terru (Nov 18 2025 at 16:35): terru (Nov 18 2025 at 16:35):Another question about the upcoming release: on RC1, try0 now only tries only metis and satx first, and the others only if those didn't find a proof. Since I use try0 quite often as my default option for "obvious" goals and rarely specify any of the non-interactive methods by hand, now my proofs end up with a lot more "by metis" instead of "by fastforce"/"by blast", or even "by simp". Of course this is fine, but I was a bit surprised — although I also have no good reason for wanting to avoid metis except habit ..
Max Lang (Nov 18 2025 at 22:15):Interesting. For me blast is also documentation that the goal was rather "simple", and I do prefer to have that compared to a metis, but I also don't have a good enough understanding of the various proof methods to know whether that's really justified.
Fabian Huch (Nov 19 2025 at 08:56):Can you please report such findings to the mailing list? This is important feedback about the release candidate and zulip is not the place to discuss it.
Manuel Eberl (Nov 19 2025 at 12:59):This issue is already being discussed on the mailing list (in the Isabelle/LLVM thread, I think).
Last updated: Jan 16 2026 at 08:33 UTC