Architecture problem

[Lawrence Paulson]

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> 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)?
>