Email Gateway (Nov 10 2025 at 18:35): Email Gateway (Nov 10 2025 at 18:35):From: "\"Kohlen, Bram (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear mailing list,
we have successfully ported Isabelle_LLVM (minus some of the latest functionality, which Peter will port later) to the latest release candidate. We did not find any big problems but we would like to address the following minor things:
*
Quite a large part of tactic.ML was moved to bires.ML, but this was not documented. We found it out by scanning the Isabelle files, but maybe this could be placed in the news as well.
*
Pretty.writeln_chunks was separated into Pretty.writeln and Pretty.chunks, but not documented.
*
Actually, I quite quickly found out many parts of Pure were renamed, but these were easy enough to port so I stopped making notes. Documentation is still appreciated though :slight_smile:
*
Several proofs broke due to "take_update" being in the simp set. Removing it fixed these proofs. While take_update was in the simp set in the 2025 version already, it seems to cause trouble only now, maybe due to another change to the simp set?
Thanks to the developers for the latest release candidate. I still have to get used to the updated GUI in jedit, but the user experience generally seems to be much better to me!
Kind regards,
Bram
Email Gateway (Nov 10 2025 at 18:53):From: Lawrence Paulson <lp15@cam.ac.uk>
Very likely because list_update_beyond is no longer in the simpset. It is not obvious that take_update is a sensible simprule, because it could be oriented either way.
Larry
On 10 Nov 2025, at 18:35, Kohlen, Bram (UT-EEMCS) <cl-isabelle-users@lists.cam.ac.uk> wrote:
• Several proofs broke due to "take_update" being in the simp set. Removing it fixed these proofs. While take_update was in the simp set in the 2025 version already, it seems to cause trouble only now, maybe due to another change to the simp set?
Email Gateway (Nov 10 2025 at 19:30):From: Manuel Eberl <manuel@pruvisto.org>
Okay, I changed the integration contour to what the Malaysian people
use. The adjustment was surprisingly easy. I did not have to touch the
main proof at all; I only had to prove that the two z1 and z2 that do
not follow the usual pattern (i.e. the endpoints of the very last arc)
satisfy the same properties as the other ones. That's a bit of
straightforward algebra.
So I managed to get a sorry-free proof of the theorem. It's not quite
the same form as Apostol and the Malaysians and the remaining literature
have because I haven't integrated the closed-form expression for the
Bessel function yet. But I do have that (and much more on Bessel
functions), so morally it's there. The constants in the error bound may
also be different from what one might find in the literature (that said,
Apostol doesn't even give a constant, just a "Big-O" estimate).
So to conclude, what we have shows that the infinite sum formula works.
And we could also easily derive the asymptotic estimate for p(n).
I did however find that the constant one gets out of the proof is
really, really bad, since it's exponential in n. So according to our
bound, you need 2^O(n) terms of the sum to compute p(n), which is quite
absurd. The true number is much lower. Not sure how much work is
required to prove that. But neither Apostol nor the Malaysians care
about that.
Manuel
On 11/10/25 19:53, Lawrence Paulson wrote:
Very likely because list_update_beyond is no longer in the simpset. It is not obvious that take_update is a sensible simprule, because it could be oriented either way.
Larry
On 10 Nov 2025, at 18:35, Kohlen, Bram (UT-EEMCS) <cl-isabelle-users@lists.cam.ac.uk> wrote:
• Several proofs broke due to "take_update" being in the simp set. Removing it fixed these proofs. While take_update was in the simp set in the 2025 version already, it seems to cause trouble only now, maybe due to another change to the simp set?
Email Gateway (Nov 10 2025 at 19:31):From: Manuel Eberl <manuel@pruvisto.org>
Oops, sorry! That was not supposed to go on the mailing list.
Manuel
On 11/10/25 20:29, Manuel Eberl wrote:
Okay, I changed the integration contour to what the Malaysian people
use. The adjustment was surprisingly easy. I did not have to touch the
main proof at all; I only had to prove that the two z1 and z2 that do
not follow the usual pattern (i.e. the endpoints of the very last arc)
satisfy the same properties as the other ones. That's a bit of
straightforward algebra.So I managed to get a sorry-free proof of the theorem. It's not quite
the same form as Apostol and the Malaysians and the remaining
literature have because I haven't integrated the closed-form
expression for the Bessel function yet. But I do have that (and much
more on Bessel functions), so morally it's there. The constants in the
error bound may also be different from what one might find in the
literature (that said, Apostol doesn't even give a constant, just a
"Big-O" estimate).So to conclude, what we have shows that the infinite sum formula
works. And we could also easily derive the asymptotic estimate for p(n).I did however find that the constant one gets out of the proof is
really, really bad, since it's exponential in n. So according to our
bound, you need 2^O(n) terms of the sum to compute p(n), which is
quite absurd. The true number is much lower. Not sure how much work is
required to prove that. But neither Apostol nor the Malaysians care
about that.Manuel
On 11/10/25 19:53, Lawrence Paulson wrote:
Very likely because list_update_beyond is no longer in the simpset.
It is not obvious that take_update is a sensible simprule, because it
could be oriented either way.Larry
On 10 Nov 2025, at 18:35, Kohlen, Bram (UT-EEMCS)
<cl-isabelle-users@lists.cam.ac.uk> wrote:• Several proofs broke due to "take_update" being in the simp
set. Removing it fixed these proofs. While take_update was in the
simp set in the 2025 version already, it seems to cause trouble only
now, maybe due to another change to the simp set?
Email Gateway (Nov 11 2025 at 12:44):From: Tobias Nipkow <nipkow@in.tum.de>
Larry,
I am a little surprised that you "Removed simp status from list_update_beyond"
(log entry).
lemma list_update_beyond: "length xs <= i ==> xs[i:=x] = xs"
It seems a useful rule to me (and I probably added it in the distant past). The
function is defined like this on purpose to avoids undefinedness. Figuring out
that the rule is applicable is not always onbious because of the precondition.
Thus I would be in favour of turning [simp] back on here.
Tobias
On 10/11/2025 19:53, Lawrence Paulson wrote:
Very likely because list_update_beyond is no longer in the simpset. It is not obvious that take_update is a sensible simprule, because it could be oriented either way.
Larry
On 10 Nov 2025, at 18:35, Kohlen, Bram (UT-EEMCS) <cl-isabelle-users@lists.cam.ac.uk> wrote:
• Several proofs broke due to "take_update" being in the simp set. Removing it fixed these proofs. While take_update was in the simp set in the 2025 version already, it seems to cause trouble only now, maybe due to another change to the simp set?
Email Gateway (Nov 12 2025 at 11:21):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
The dependent projects lrat_isa and bernoulli-numbers where ported
easily, with only minor changes required.
--
Peter
cf.
https://github.com/lammich/lrat_isa/tree/2025-1
https://github.com/pruvisto/bernmm/tree/2025-1
On 10/11/2025 19:35, "Kohlen, Bram (UT-EEMCS)" (via cl-isabelle-users
Mailing List) wrote:
Dear mailing list,
we have successfully ported Isabelle_LLVM (minus some of the latest
functionality, which Peter will port later) to the latest release
candidate. We did not find any big problems but we would like to
address the following minor things:*
Quite a large part of tactic.ML was moved to bires.ML, but this
was not documented. We found it out by scanning the Isabelle
files, but maybe this could be placed in the news as well.
*
Pretty.writeln_chunks was separated into Pretty.writeln and
Pretty.chunks, but not documented.
o
Actually, I quite quickly found out many parts of Pure were
renamed, but these were easy enough to port so I stopped
making notes. Documentation is still appreciated though :slight_smile:
*
Several proofs broke due to "take_update" being in the simp set.
Removing it fixed these proofs. While take_update was in the simp
set in the 2025 version already, it seems to cause trouble only
now, maybe due to another change to the simp set?Thanks to the developers for the latest release candidate. I still
have to get used to the updated GUI in jedit, but the user experience
generally seems to be much better to me!Kind regards,
Bram
Email Gateway (Nov 17 2025 at 15:06):From: Makarius <makarius@sketis.net>
On 10/11/2025 19:35, "Kohlen, Bram (UT-EEMCS)" (via cl-isabelle-users Mailing
List) wrote:
*
Quite a large part of tactic.ML was moved to bires.ML, but this was not
documented. We found it out by scanning the Isabelle files, but maybe this
could be placed in the news as well.
*
Pretty.writeln_chunks was separated into Pretty.writeln and Pretty.chunks,
but not documented.
o
Actually, I quite quickly found out many parts of Pure were renamed,
but these were easy enough to port so I stopped making notes.
Documentation is still appreciated though :slight_smile:
I will see what needs to be added to NEWS on Isabelle/ML.
I still have to get
used to the updated GUI in jedit, but the user experience generally seems to
be much better to me!
Is there anything specific that needs to get used to? Many minor details have
been brushed up, but there could be also new drop-outs that were not intended.
Makarius
Email Gateway (Nov 19 2025 at 09:04):From: "\"Kohlen, Bram (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hello Makarius,
after using the new version for a couple of days I feel no features I use are missing. With the help of the mailing list I have now created a different try0 schedule for myself, so that has been resolved, thanks to everyone for the answers!
The only thing I noticed is that sledgehammer seems to abort much earlier now (in about half the time).
The standard timeout for sledgehammer is 30 seconds, but I found sledgehammer to stop already after just under 15 seconds. If I increase the timeout to 60 seconds, it stops at just under 30 seconds.
And I am sure that it does not abort due to the lack of a proof, as I have at least one example where sledgehammer does not find a proof with 30 seconds timeout, in which case it terminates after about 15 seconds without a proof. However, with 60 seconds timeout, a proof is found after about 20 seconds.
Typically I would provide a small example of said case, but I have failed to produce one of reasonable size so far. I do get this behaviour in my own formalization. However, it is easy to check that sledgehammer stops early on any lemma for which sledgehammer does not find a proof.
Apart from that, I have not noticed anything strange so far.
Kind regards,
Bram
From: Makarius <makarius@sketis.net>
Sent: Monday, November 17, 2025 4:05 PM
To: Kohlen, Bram (UT-EEMCS) <b.kohlen@utwente.nl>; isabelle-users <isabelle-users@cl.cam.ac.uk>
Subject: Re: [isabelle] [Isabelle2025-1-RC1] Porting Isabelle_LLVM
On 10/11/2025 19:35, "Kohlen, Bram (UT-EEMCS)" (via cl-isabelle-users Mailing
List) wrote:
*
Quite a large part of tactic.ML was moved to bires.ML, but this was not
documented. We found it out by scanning the Isabelle files, but maybe this
could be placed in the news as well.
*
Pretty.writeln_chunks was separated into Pretty.writeln and Pretty.chunks,
but not documented.
o
Actually, I quite quickly found out many parts of Pure were renamed,
but these were easy enough to port so I stopped making notes.
Documentation is still appreciated though :slight_smile:
I will see what needs to be added to NEWS on Isabelle/ML.
I still have to get
used to the updated GUI in jedit, but the user experience generally seems to
be much better to me!
Is there anything specific that needs to get used to? Many minor details have
been brushed up, but there could be also new drop-outs that were not intended.
Makarius
Email Gateway (Nov 19 2025 at 09:15):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
On 19-Nov-25 10:03 AM, "Kohlen, Bram (UT-EEMCS)" (via cl-isabelle-users
Mailing List) wrote:
With the help of the mailing list I have now created a different try0
schedule for myself, so that has been resolved, thanks to everyone for
the answers!
Can you describe your solution here? I think this is of a general
interest (the current default behavior of try0 feels strange to me), and
I do not see immediately the answer in the mailing list.
Thanks.
Stepan
Email Gateway (Nov 19 2025 at 09:22):From: "\"Kohlen, Bram (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hello Stepan,
I simply moved satx and metis to the last batch.
declare [[try0_schedule = "
order presburger linarith algebra argo | simp auto blast fast fastforce force meson satx metis
"]]
It seems to work well, but I am also considering moving everything into the same batch again (removing the pipe | ), as I do not notice an improvement from this setup compared to try0 in Isabelle2025. Maybe I am using it the wrong way though. Does anyone have any insights on this?
Kind regards,
Bram
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: Wednesday, November 19, 2025 10:15 AM
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] [Isabelle2025-1-RC1] Porting Isabelle_LLVM
On 19-Nov-25 10:03 AM, "Kohlen, Bram (UT-EEMCS)" (via cl-isabelle-users
Mailing List) wrote:
With the help of the mailing list I have now created a different try0
schedule for myself, so that has been resolved, thanks to everyone for
the answers!
Can you describe your solution here? I think this is of a general
interest (the current default behavior of try0 feels strange to me), and
I do not see immediately the answer in the mailing list.
Thanks.
Stepan
Email Gateway (Nov 19 2025 at 09:22):From: "\"Lammich, Peter (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
I'd prefer the old behaviour as standard, as it seems to be more likely to find proofs quickly. This is in particular important for auto-try0.
What was the motivation behind the change?
Peter
On 19 Nov 2025 10:15, Stepan Holub <cl-isabelle-users@lists.cam.ac.uk> wrote:
On 19-Nov-25 10:03 AM, "Kohlen, Bram (UT-EEMCS)" (via cl-isabelle-users
Mailing List) wrote:
With the help of the mailing list I have now created a different try0
schedule for myself, so that has been resolved, thanks to everyone for
the answers!
Can you describe your solution here? I think this is of a general
interest (the current default behavior of try0 feels strange to me), and
I do not see immediately the answer in the mailing list.
Thanks.
Stepan
Email Gateway (Nov 19 2025 at 10:12):From: Manuel Eberl <manuel@pruvisto.org>
I also experienced problems with this. My impression was that try0
inexplicable only tried satx and metis and never tried any of the
others, but I didn't care enough to investigate further. It did not
occur to me that I ought to simply wait longer – in any case I would
have had to wait significantly longer than my patience allows when using
"try0", which I (in my usual workflow) expect to give an answer within 5
seconds or so at most.
So my impression is that the issue is mainly that one of "satx" and
"metis" sometimes does not terminate within a reasonable amount of time
and is also not killed within a reasonable amount of time, and then the
others are not even tried.
Manuel
On 19/11/2025 10:22, "Lammich, Peter (UT-EEMCS)" (via cl-isabelle-users
Mailing List) wrote:
I'd prefer the old behaviour as standard, as it seems to be more
likely to find proofs quickly. This is in particular important for
auto-try0.What was the motivation behind the change?
Peter
On 19 Nov 2025 10:15, Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
wrote:On 19-Nov-25 10:03 AM, "Kohlen, Bram (UT-EEMCS)" (via cl-isabelle-users
Mailing List) wrote:With the help of the mailing list I have now created a different try0
schedule for myself, so that has been resolved, thanks to everyone for
the answers!
Can you describe your solution here? I think this is of a general
interest (the current default behavior of try0 feels strange to me), and
I do not see immediately the answer in the mailing list.Thanks.
Stepan
Last updated: Dec 02 2025 at 16:32 UTC