Architecture problem

[Jasmin Blanchette]

Hi Hanna,

Thanks for the update. I wish you good luck with the last steps! The icing on the cake of any programming project is of course when it gets integrated upstream. Let me know if there's anything I can do to help (but I suspect the combined expertise of you and your coauthors is more than enough to succeed).

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html


> On 23. Oct 2025, at 02:13, Hanna Elif Lachnitt <lachnitt at stanford.edu> wrote:
> 
> Hi everyone,
> 
> unfortunately we don't think that we can have it ready for the RC1 in two weeks. We strive to put it in the official repo as soon as possible.
> 
> We made extensive changes and additions to the code as cvc5's proofs are far more detailed than veriT's. We also want to optimize good performance before users start using it. Since parsing is slow, having more steps can be detrimental, so we are investigating how to improve the size of cvc5 proofs.
> 
> 
> Best,
> Hanna
> 
> From: Lawrence Paulson <lp15 at cam.ac.uk <mailto:lp15 at cam.ac.uk>>
> Sent: Wednesday, October 22, 2025 03:32
> To: Jasmin Blanchette <jasmin.blanchette at ifi.lmu.de <mailto:jasmin.blanchette at ifi.lmu.de>>; Hanna Elif Lachnitt <lachnitt at stanford.edu <mailto:lachnitt at stanford.edu>>
> Cc: DEV Isabelle Mailinglist <isabelle-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>>
> Subject: Re: Architecture problem
>  
> I'm pretty sure Hanna said that this would be in the next release. Hanna, can you offer any more details?
> 
> Larry
> 
> > On 22 Oct 2025, at 08:00, Jasmin Blanchette <jasmin.blanchette at ifi.lmu.de <mailto:jasmin.blanchette at ifi.lmu.de>> wrote:
> >
> > Now, I just tried this example with Isabelle/a356fd7ca1c4:
> >
> > lemma "a = b ⟹ f a = f b"
> >   using [[smt_trace]]
> >   by (smt (cvc5))
> >
> > and it doesn't work. I get the error "Error in option parsing: proof-format=alethe is experimental in this version. If you know what you are doing, you can try --proof-alethe-experimental". So it doesn't look to me as if we can use cvc5 for reconstruction quite yet, which also postpones the work of the "task force".
> >
> > Could one of the multiple authors of Lachnitt et al. (ITP 2025) comment on the status of their project (hoping at least one of them is on this mailing list)?
> >

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251023/7be47b93/attachment.htm>