Email Gateway (Nov 19 2025 at 21:50): Email Gateway (Nov 19 2025 at 21:50):From: Jørgen Villadsen <cl-isabelle-users@lists.cam.ac.uk>
I completely agree, please call it try1 and keep the old try0. The new try0 is useless for me and my students.
Regards, Jørgen
From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Sent: 19 November 2025 14:03
To: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] [Isabelle2025-1-RC1] About try0
Perhaps, the new default, whatever reason there is for it, could be try1 ...
Stepan
On 11/19/2025 12:19 PM, Peter (via cl-isabelle-users Mailing List) wrote:
That sounds like a nice change (provided the default makes sense and
is usable).However, it is not modular: A theory cannot simply add another method
to try0 without reverting all existing settings. So in the current
form, it looks like this makes sense mostly in every private user's
settings, which is great!But forcing a new, incompatible, and less performing default setting
is critical: this will only limit the use and usefulness of try0.
Moreover, we'll probably see a lot of theories starting with
some declare [[try0_schedule = "..."]] magic, exporting it to all
dependent theories.--
Peter
On 19/11/2025 10:44, martin.desharnais-schaefer@posteo.de wrote:
Hi Bram,
reposting as my original email did not reach the mailing list.
I have been using the new Isabelle2025-1-RC1 version for a couple of
days now. I see that try0 has gotten a bit of an overhaul where
certain provers are tried before others...This bothers me, because I feel like I should not have to wait five
seconds for this very simple proof. Especially because, in
Isabelle2025, these proofs show up immediately with try0.Thank you for testing Isabelle2025-1-RC1 and pointing out your issue
caused by this undocumented change.My first question is: Can I somehow change or disable this ordering?
Or can this be added? I looked around for about 15 minutes but could
not find any new settings. I do want to play around a bit to see if I
can find an ordering works for me, but the current one makes try0 feel
a bit sluggish in my opinion.Yes, you can configure the default timeout with the option
try0_default_timeoutand the schedule with the option
try0_schedule. The default schedule is the following:declare [[try0_schedule = "
satx metis |
order presburger linarith algebra argo |
simp auto blast fast fastforce force meson
"]]See the new documentation further down. In a nutshell, you can change
the ordering by moving the names around or use full parallel
execution by removing the vertical bars.I changed the default timeout from 5 to 2 seconds; it can still be
increased or decreased on a case-by-case basis withusing [[try0_default_timeout = <integer>]].My second question is: Could these changes be added to the news?
Currently it states nothing about changes to try0 while this one is
quite large in my opinion.Yes, I added the following documentation entry to NEW:
- try0:
- Proof methods can now be dynamically added with the function
Try0.register_proof_method and retrieved (e.g., to call them from
Isabelle/ML) with the function Try0.get_proof_method.- Added the option "try0_schedule" to control which proof methods get
tried in which order. It accepts a list of proof method names
separated by either a space, meaning parallel evaluation, or
vertical lines, meaning sequential evaluation. The schedule is
interpreted as list of groups executed in sequence; in each group,
the proof methods are executed in parallel. INCOMPATIBILITY.- Added the option "try0_default_timeout" to control the default
timeout (in seconds).- Changed the default timeout from 5 to 2 seconds.
Minor INCOMPATIBILITY.Regards,
Martin
Email Gateway (Nov 19 2025 at 21:55):From: Lawrence Paulson <lp15@cam.ac.uk>
It’s impossible not to be reminded of the Theranos slogan, from Yoda in Star Wars: “Do or do not. There is no try.”
Larry
On 19 Nov 2025, at 21:50, Jørgen Villadsen <cl-isabelle-users@lists.cam.ac.uk> wrote:
I completely agree, please call it try1 and keep the old try0. The new try0 is useless for me and my students.
Email Gateway (Nov 19 2025 at 22:00):From: Makarius <makarius@sketis.net>
On 19/11/2025 22:54, Lawrence Paulson wrote:
It’s impossible not to be reminded of the Theranos slogan, from Yoda in Star Wars: “Do or do not. There is no try.”
Not Yoda am I, but the Isabelle release manager.
It is up to Martin to figure out the truth from various reports on RC1/RC2,
and come up with suitable changes in the next 1-2 weeks. It is mainly about
converging to something that works most of the time, without going back and
forth several times.
Makarius
Email Gateway (Nov 20 2025 at 06:50):From: Martin Desharnais-Schäfer <martin.desharnais-schaefer@posteo.de>
Hi all,
Le 2025-11-19 à 23 h 00, Makarius a écrit :
It is up to Martin to figure out the truth from various reports on
RC1/ RC2, and come up with suitable changes in the next 1-2 weeks.
It is mainly about converging to something that works most of the
time, without going back and forth several times.
Yesterday, I changed the default schedule to run everything in parallel
but, sadly, this commit did not make it into RC2: It will be in RC3.
A schedule can still be defined manually with the "try0_schedule"
option. However, note that I also changed the character used in the
schedule to mark sequencing from a vertical bar to a semicolon; some
anonymous person pointed out that a vertical bar could suggest
parallelism and suggested the semicolon as an alternative already use in
many programming languages to mark sequencing.
The documentation in NEWS and the reduced timeout did make it into RC2,
so all proof methods get be executed in about six seconds, slightly more
than five.
Regards,
Martin
Last updated: Dec 02 2025 at 16:32 UTC