Email Gateway (Oct 13 2025 at 16:10): Email Gateway (Oct 13 2025 at 16:10):From: Lawrence Paulson <lp15@cam.ac.uk>
I experienced a failure of code generation using this pre-release, and have been able to isolate it to the following example:
definition "test ≡ ∀w::16 word ∈ {0..31}. (w AND 63) = (w AND 31)"
export_code test
The error message is
*** Type 16 word not of sort discrete_linordered_semidom_with_range
*** No type arity word ::
*** discrete_linordered_semidom_with_range
This example works in Isabelle2025. Thoughts?
Larry
Email Gateway (Oct 13 2025 at 17:09):From: Makarius <makarius@sketis.net>
On 13/10/2025 18:10, Lawrence Paulson wrote:
I experienced a failure of code generation using this pre-release, and have
been able to isolate it to the following example:definition "test ≡ ∀w::16 word ∈ {0..31}. (w AND 63) = (w AND 31)"
export_code test
The error message is
*** Type 16 word not of sort discrete_linordered_semidom_with_range
*** No type arity word ::
*** discrete_linordered_semidom_with_rangeThis example works in Isabelle2025. Thoughts?
Florian Haftmann has made many changes in the codegen setup recently.
You might help him by making induction over the history, using "hg bisect".
Makarius
Email Gateway (Oct 14 2025 at 13:02):From: Lawrence Paulson <lp15@cam.ac.uk>
The error goes away if I invoke
declare discrete_linordered_semidom_with_range_class.atLeastAtMost_eq_range [code del]
The code it generates for Standard ML takes up 22K. For Isabelle 2025, the same example generates 25K of code. There is very little overlap between the two. I did not try running them.
From: Lawrence Paulson <lp15@cam.ac.uk>
Sent: 13 October 2025 17:10
To: cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Subject: Isabelle2025-1_RC0 code generation regression
I experienced a failure of code generation using this pre-release, and have been able to isolate it to the following example:
definition "test ≡ ∀w::16 word ∈ {0..31}. (w AND 63) = (w AND 31)"
export_code test
The error message is
*** Type 16 word not of sort discrete_linordered_semidom_with_range
*** No type arity word ::
*** discrete_linordered_semidom_with_range
This example works in Isabelle2025. Thoughts?
Larry
Email Gateway (Oct 16 2025 at 09:16):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Things like
definition "test ≡ ∀w::16 word ∈ {0..31}. (w AND 63) = (w AND 31)"
work in Isabelle2025 but the code is very inefficient.
I am currently testing a practically functioning code setup for ranges
on words as candidate for Isabelle2025-1.
Doing that range stuff properly will require one further iteration.
Florian
Am 14.10.25 um 15:02 schrieb Lawrence Paulson:
The error goes away if I invoke
declare discrete_linordered_semidom_with_range_class.atLeastAtMost_eq_range [code del]
The code it generates for Standard ML takes up 22K. For Isabelle 2025, the same example generates 25K of code. There is very little overlap between the two. I did not try running them.
From: Lawrence Paulson <lp15@cam.ac.uk>
Sent: 13 October 2025 17:10
To: cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Subject: Isabelle2025-1_RC0 code generation regressionI experienced a failure of code generation using this pre-release, and have been able to isolate it to the following example:
definition "test ≡ ∀w::16 word ∈ {0..31}. (w AND 63) = (w AND 31)"
export_code test
The error message is
*** Type 16 word not of sort discrete_linordered_semidom_with_range
*** No type arity word ::
*** discrete_linordered_semidom_with_rangeThis example works in Isabelle2025. Thoughts?
Larry
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Oct 16 2025 at 11:23):From: Florian Haftmann <florian.haftmann@cit.tum.de>
See now https://isabelle.in.tum.de/repos/isabelle/rev/0bd014c32479
(The additional material should be easily usable stand-alone on top of RC0)
Florian
Am 16.10.25 um 11:10 schrieb Florian Haftmann:
Things like
definition "test ≡ ∀w::16 word ∈ {0..31}. (w AND 63) = (w AND 31)"
work in Isabelle2025 but the code is very inefficient.
I am currently testing a practically functioning code setup for ranges
on words as candidate for Isabelle2025-1.Doing that range stuff properly will require one further iteration.
Florian
Am 14.10.25 um 15:02 schrieb Lawrence Paulson:
The error goes away if I invoke
declare
discrete_linordered_semidom_with_range_class.atLeastAtMost_eq_range
[code del]The code it generates for Standard ML takes up 22K. For Isabelle 2025,
the same example generates 25K of code. There is very little overlap
between the two. I did not try running them.
From: Lawrence Paulson <lp15@cam.ac.uk>
Sent: 13 October 2025 17:10
To: cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Subject: Isabelle2025-1_RC0 code generation regressionI experienced a failure of code generation using this pre-release, and
have been able to isolate it to the following example:definition "test ≡ ∀w::16 word ∈ {0..31}. (w AND 63) = (w AND 31)"
export_code test
The error message is
*** Type 16 word not of sort discrete_linordered_semidom_with_range
*** No type arity word ::
*** discrete_linordered_semidom_with_rangeThis example works in Isabelle2025. Thoughts?
Larry
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Oct 17 2025 at 10:46):From: Lawrence Paulson <lp15@cam.ac.uk>
This looks great. In the examples, I changed the upper bound for the quantifiers from 31 to 32767 and the two tests still ran in well under a second.
Larry
On 16 Oct 2025 at 12:14 +0100, Florian Haftmann <florian.haftmann@cit.tum.de>, wrote:
(The additional material should be easily usable stand-alone on top of RC0)
Last updated: Oct 20 2025 at 16:27 UTC