Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Isabelle2025-1-RC1] About try0

view this post on Zulip Email Gateway (Nov 13 2025 at 09:57):

From: "\"Kohlen, Bram (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

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. First it tries satx and metis, then order, presburger, linarith, algebra and argo and finally simp, auto, blast, fast, fastforce, force and meson.

I have been running into some issues where for example satx and metis block (sometimes almost trivial) proofs that can easily be solved by auto.
For example:

lemma "(λ (n,M). M n) (n,M) ⟹ M n"
   try0

First, metis or satx will block try0 for about 5 seconds while searching for a proof. After 5 seconds, presumably because of a timeout, try0 moves on to the second batch of provers (order, presburger, linarith, algebra and argo), which fail immediately and only then moves on to the third batch where it provides proofs using simp, auto, blast, fast, fastforce and force.

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.

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.

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.

Kind regards,
Bram

view this post on Zulip Email Gateway (Nov 13 2025 at 10:04):

From: Tobias Nipkow <nipkow@in.tum.de>
I would just like to add that a student of mine has the same issue.

Tobias

On 13/11/2025 10:56, "Kohlen, Bram (UT-EEMCS)" (via cl-isabelle-users Mailing
List) wrote:

Dear all,

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. First it tries satx and metis, then order, presburger, linarith,
algebra and argo and finally simp, auto, blast, fast, fastforce, force and meson.

I have been running into some issues where for example satx and metis block
(sometimes almost trivial) proofs that can easily be solved by auto.
For example:

lemma "(λ (n,M). M n) (n,M) ⟹ M n"
    try0

First, metis or satx will block try0 for about 5 seconds while searching for a
proof. After 5 seconds, presumably because of a timeout, try0 moves on to the
second batch of provers (order, presburger, linarith, algebra and argo), which
fail immediately and only then moves on to the third batch where it provides
proofs using simp, auto, blast, fast, fastforce and force.

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.

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.

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.

Kind regards,
Bram

smime.p7s

view this post on Zulip Email Gateway (Nov 13 2025 at 10:13):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
In my experience, Isabelle2025 already had the issue where "try" would sometimes completely
fail when in fact it turns out "auto" would succeed very quickly. This meant that you would
lose the time of waiting through an entire cycle of "try" and only then (because it looks
like the goal ought to be fairly simple to solve) you find that "auto" worked in the first place.

So far, it looks like Isabelle2025-1-RC1 also has this behavior. It is of course very difficult
to extract reasonable examples for bug reporting purposes.

- Gene Stark

On 11/13/25 04:56, "Kohlen, Bram (UT-EEMCS)" (via cl-isabelle-users Mailing List) wrote:

Dear all,

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. First it tries satx and metis, then order, presburger, linarith,
algebra and argo and finally simp, auto, blast, fast, fastforce, force and meson.

I have been running into some issues where for example satx and metis block (sometimes almost trivial) proofs that can
easily be solved by auto.
For example: 

lemma "(λ (n,M). M n) (n,M) ⟹ M n"
    try0

First, metis or satx will block try0 for about 5 seconds while searching for a proof. After 5 seconds, presumably
because of a timeout, try0 moves on to the second batch of provers (order, presburger, linarith, algebra and argo),
which fail immediately and only then moves on to the third batch where it provides proofs using simp, auto, blast, fast,
fastforce and force.

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.

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.

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.

Kind regards,
Bram

view this post on Zulip Email Gateway (Nov 19 2025 at 09:44):

From: martin.desharnais-schaefer@posteo.de
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_timeout and 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 with using [[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:

Regards,
Martin

view this post on Zulip Email Gateway (Nov 19 2025 at 11:19):

From: Peter <cl-isabelle-users@lists.cam.ac.uk>
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_timeout and 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 with using [[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:

Regards,
Martin

view this post on Zulip Email Gateway (Nov 19 2025 at 13:04):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
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_timeout and 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 with using [[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:

Regards,
Martin

view this post on Zulip Email Gateway (Nov 19 2025 at 13:15):

From: Martin Desharnais-Schäfer <martin.desharnais-schaefer@posteo.de>
Hi Bram,

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_timeout and 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 with using [[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.

I added the following documentation entry to NEW:

Regards,
Martin

view this post on Zulip Email Gateway (Dec 01 2025 at 17:22):

From: Makarius <makarius@sketis.net>

On 19/11/2025 12:19, 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.

Is that question settled in RC3? I've lost track of the many small changes in
that area.

Makarius

view this post on Zulip Email Gateway (Dec 01 2025 at 17:29):

From: Martin Desharnais-Schäfer <martin.desharnais-schaefer@posteo.de>

Hi Makarius,

Le 2025-12-01 à 18 h 22, Makarius a écrit :

On 19/11/2025 12:19, 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.

Is that question settled in RC3? I've lost track of the many small
changes in that area.

I changed the default schedule to run all proof methods in parallel,
which should, hopefully, settled the raised criticisms.

Regards,
Martin

Last updated: Dec 02 2025 at 16:32 UTC