Email Gateway (Jul 08 2025 at 17:27): Email Gateway (Jul 08 2025 at 17:27):From: Lawrence Paulson <lp15@cam.ac.uk>
Hello all, the following email from John Harrison may be of interest.
Begin forwarded message:
From: John R Harrison <jrh013@gmail.com>
Subject: Datatype definition efficiency
Date: 8 July 2025 at 01:29:22 BST
To: Larry Paulson <Larry.Paulson@cl.cam.ac.uk>This is a real example in HOL Light from the domain mentioned,
of CPU ISA specification. It's currently at 79 constructors and
growing but not otherwise very interesting or challenging; it's not
actually recursive, for example.https://github.com/awslabs/s2n-bignum/blob/main/x86/proofs/instruction.ml#L234-L317
I did some tests of the following in HOL Light, defining simple
enumeration types with 2^n constructors:let test n =
let s = String.make 1 (Char.chr (Char.code 'A' + n)) in
let cnames = map (fun i -> s^string_of_int i) (0--(1 lsl n - 1)) in
let comstr = end_itlist (fun s t -> s ^ " | " ^ t) cnames in
time define_type ("Type_"^s^" = " ^ comstr);;do_list test (1--8);;
and the performance is worse than quadratic, looking suspiciously as
if something in there is cubic:constructors | CPU time in seconds
2 | 0.033
4 | 0.039
8 | 0.061
16 | 0.133
32 | 0.333
64 | 1.104
128 | 5.225
256 | 33.499
512 | 258.794My recollection is that when first writing this code (sharing an
office with Makarius in Munich!) I initially made an effort to keep
things subquadratic but at some point decided not to bother with the
extra complications since it was OK in most practical cases.
Email Gateway (Jul 08 2025 at 20:13):From: Makarius <makarius@sketis.net>
Hi Larry,
it is good to collect more specimens from the greater HOL family. I will go
through some of the examples soon, although I am not directly responsible for
the actual datatype construction --- Dmitriy is.
Nonetheless, we can expect some improvements in the underlying infrastructure.
I am half-through with some significant changes on the claset, after so many
decades of a certain status-quo that I never quite understood (due to
accumulated adhoc changes).
Makarius
On 08/07/2025 19:27, Lawrence Paulson wrote:
Hello all, the following email from John Harrison may be of interest.
Begin forwarded message:
From: John R Harrison <jrh013@gmail.com>
Subject: Datatype definition efficiency
Date: 8 July 2025 at 01:29:22 BST
To: Larry Paulson <Larry.Paulson@cl.cam.ac.uk>This is a real example in HOL Light from the domain mentioned,
of CPU ISA specification. It's currently at 79 constructors and
growing but not otherwise very interesting or challenging; it's not
actually recursive, for example.https://github.com/awslabs/s2n-bignum/blob/main/x86/proofs/instruction.ml#L234-L317
I did some tests of the following in HOL Light, defining simple
enumeration types with 2^n constructors:let test n =
let s = String.make 1 (Char.chr (Char.code 'A' + n)) in
let cnames = map (fun i -> s^string_of_int i) (0--(1 lsl n - 1)) in
let comstr = end_itlist (fun s t -> s ^ " | " ^ t) cnames in
time define_type ("Type_"^s^" = " ^ comstr);;do_list test (1--8);;
and the performance is worse than quadratic, looking suspiciously as
if something in there is cubic:constructors | CPU time in seconds
2 | 0.033
4 | 0.039
8 | 0.061
16 | 0.133
32 | 0.333
64 | 1.104
128 | 5.225
256 | 33.499
512 | 258.794My recollection is that when first writing this code (sharing an
office with Makarius in Munich!) I initially made an effort to keep
things subquadratic but at some point decided not to bother with the
extra complications since it was OK in most practical cases.
Email Gateway (Jul 08 2025 at 20:23):From: Lawrence Paulson <lp15@cam.ac.uk>
Indeed the real question is why the merging of clasets is slower than the merging of simpsets, when they use the same data structure.
Dmitriy reminds me that the unwanted rules can just be deleted using [iff del].
On 8 Jul 2025, at 21:12, Makarius <makarius@sketis.net> wrote:
Nonetheless, we can expect some improvements in the underlying infrastructure. I am half-through with some significant changes on the claset, after so many decades of a certain status-quo that I never quite understood (due to accumulated adhoc changes).
Email Gateway (Jul 08 2025 at 22:19):From: Makarius <makarius@sketis.net>
On 08/07/2025 22:23, Lawrence Paulson wrote:
Indeed the real question is why the merging of clasets is slower than the merging of simpsets, when they use the same data structure.
At the very bottom there is type Net.net for both, but the claset has a lot of
extra complexity piled up on top of it. When I am through in reading/rewriting
it carefully, it should be all apparent: written in proper Isabelle/ML of
2025, not Cambridge SML from 1995.
Makarius
Email Gateway (Jul 09 2025 at 09:38):From: Lawrence Paulson <lp15@cam.ac.uk>
Looking forward to this. As I may have mentioned already, one of Isabelle's distinct advantages over "certain other trendy systems" is its ability to scale. That is something we should push to its limit.
Larry
On 8 Jul 2025, at 23:18, Makarius <makarius@sketis.net> wrote:
At the very bottom there is type Net.net for both, but the claset has a lot of extra complexity piled up on top of it. When I am through in reading/rewriting it carefully, it should be all apparent: written in proper Isabelle/ML of 2025, not Cambridge SML from 1995.
Email Gateway (Jul 09 2025 at 09:40):From: Makarius <makarius@sketis.net>
On 09/07/2025 11:38, Lawrence Paulson wrote:
Looking forward to this. As I may have mentioned already, one of Isabelle's distinct advantages over "certain other trendy systems" is its ability to scale. That is something we should push to its limit.
"Push to its limits" is not conformant with decades of Isabelle culture. We
usually work more diligently. Isabelle is a non-violent system.
Makarius
Email Gateway (Jul 09 2025 at 09:52):From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>
Thank you for looking into this, Makarius.
In addition to potential claset efficiency improvements: Can the datatype package be adjusted to allow the user to choose between the auto-generation of (in)equality lemmas (unmodified default) and alternative means such as a simproc? The package already has a plugin mechanism -- can it be extended to allow for this customization?
Hanno
On 09/07/2025, 10:41, "cl-isabelle-users-request@lists.cam.ac.uk <mailto:cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Makarius" <cl-isabelle-users-request@lists.cam.ac.uk <mailto:cl-isabelle-users-request@lists.cam.ac.uk> on behalf of makarius@sketis.net <mailto:makarius@sketis.net>> wrote:
CAUTION: This email originated from outside of the organization. Do not click links or open attachments unless you can confirm the sender and know the content is safe.
On 09/07/2025 11:38, Lawrence Paulson wrote:
Looking forward to this. As I may have mentioned already, one of Isabelle's distinct advantages over "certain other trendy systems" is its ability to scale. That is something we should push to its limit.
"Push to its limits" is not conformant with decades of Isabelle culture. We
usually work more diligently. Isabelle is a non-violent system.
Makarius
Email Gateway (Jul 09 2025 at 10:56):From: Makarius <makarius@sketis.net>
On 09/07/2025 11:51, Becker, Hanno wrote:
In addition to potential claset efficiency improvements: Can the datatype package be adjusted to allow the user to choose between the auto-generation of (in)equality lemmas (unmodified default) and alternative means such as a simproc? The package already has a plugin mechanism -- can it be extended to allow for this customization?
That particular question is for Dmitriy.
Merely a reminder: any performance improvements of Isabelle need to be based
on concrete applications and/or benchmarks. This is required to provide
repeatable measurements, before and after attempts of improvements, and also
for future tests (sometimes years later).
Otherwise, we would be flying blind, and nobody could say if something is
really better, or could be done differently later on.
Makarius
Email Gateway (Jul 11 2025 at 17:43):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
Sorry, I have been delaying the response to this thread due to being occupied otherwise.
First, thanks to Larry and John for sharing the HOL Light benchmark. It inspired me to make my own measurements (not to compare to HOL Light but to get some understanding of whether there might be a problem). I paste the Isabelle snippet below. It produces the following results:
No plugins:
#Constructors 2: 83 ms
#Constructors 4: 113 ms
#Constructors 8: 164 ms
#Constructors 16: 373 ms
#Constructors 32: 1568 ms
#Constructors 64: 11088 ms
#Constructors 128: 109744 ms
All standard plugins:
#Constructors 2: 260 ms
#Constructors 4: 345 ms
#Constructors 8: 729 ms
#Constructors 16: 1154 ms
#Constructors 32: 5061 ms
#Constructors 64: 41187 ms
#Constructors 128: 692897 ms
Some notes about these numbers:
1) I consider myself primarily responsible for the runtime of datatypes with all plugins disabled. (Even there, frankly speaking, this is a shared responsibility between me and Jasmin, but at least in the past, we were both happy to look into each other's code.)
2) The standard plugins add about a factor 4–6 to the runtime. I don’t know how this breaks down between the different plugins precisely, and need to investigate this further. Some of the plugins are somewhat essential for proper (i.e., recursive) datatypes, such as the size plugin that defines the size function; others are relevant for all datatypes, such as the code generation plugin that e.g., instantiates the equal type class (another quadratic theorem BTW). Others again are more exotic, such as the lifting and transfer plugins. Ultimately, it depends on the application whether one needs a particular plugin. The default in Isabelle is to have all plugins enabled. Perhaps we can discuss if this should be reconsidered.
3) The measurements are taken with parallelism turned off. This is not representative of the average user experience. With parallelism, it is hard to get precise timings. For example, the no-plugins 128 constructors test reports 13107 ms (instead of 109774 ms), and the processing of the commands below that declaration proceeds after that time. However, the internal datatype proofs are forked, and PolyML is working hard on them in the background so that the system’s responsiveness is lowered for about a minute.
4) The examples of the form T1 = A1 | … | A128 are very artificial. Here, I agree with Makarius that we lack real-world evidence of specific Isabelle examples that are too slow. I’ll reply to some of the pointers in the other thread. The original issue with the claset in the other thread has to my knowledge been resolved by adding a T.distinct[iff del] declaration for the offending type T.
5) While it would be nice to bring the numbers (or even better the growth factor) down, I don’t think we are in a state that prohibits us from using large datatypes.
Coming back to Hanno’s question: The plugins are already in users’ hands. So yes, you can add attributes like [simp del] or [iff del] to any theorem associated with (co)datatypes, e.g., if they have more than 100 constructors. However, not generating the properties in the first place is more difficult: distinctness is part of the standard interface of (co)datatypes and is already used by other tools for their internal work (I know of primcorec as one example, but there may be others too).
Best wishes,
Dmitriy
ML ‹Multithreading.parallel_proofs := 0›
local_setup ‹ fn lthy =>
let
open BNF_FP_Def_Sugar;
open BNF_FP_Util;
open BNF_LFP;
open BNF_Util;
open BNF_Def;
val time = time (Config.put bnf_timing true lthy);
fun test filter b n lthy =
let
val timer = time (Timer.startRealTimer ());
val ctr_specs = map (fn i =>
(((Binding.empty, Binding.suffix_name (string_of_int i) @{binding A}), []), NoSyn)) (0 upto Integer.pow n 2);
val spec = ((((([], Binding.suffix_name (string_of_int n) b), NoSyn), ctr_specs),
(Binding.empty, Binding.empty, Binding.empty)), []);
val lthy = co_datatypes Least_FP construct_lfp ((filter, false), [spec]) lthy
val timer = time (timer ("#Constructors " ^ string_of_int (Integer.pow n 2)));
in
lthy
end;
in
lthy
|> (fn lthy => K lthy (warning "No plugins:"))
|> fold (test (Plugin_Name.make_filter lthy (K (K false))) @{binding T}) (1 upto 7)
|> (fn lthy => K lthy (warning "All standard plugins:"))
|> fold (test Plugin_Name.default_filter @{binding U}) (1 upto 7)
end
›
On 9 Jul 2025, at 12.56, Makarius <makarius@sketis.net> wrote:
On 09/07/2025 11:51, Becker, Hanno wrote:
In addition to potential claset efficiency improvements: Can the datatype package be adjusted to allow the user to choose between the auto-generation of (in)equality lemmas (unmodified default) and alternative means such as a simproc? The package already has a plugin mechanism -- can it be extended to allow for this customization?
That particular question is for Dmitriy.
Merely a reminder: any performance improvements of Isabelle need to be based on concrete applications and/or benchmarks. This is required to provide repeatable measurements, before and after attempts of improvements, and also for future tests (sometimes years later).
Otherwise, we would be flying blind, and nobody could say if something is really better, or could be done differently later on.
Makarius
Last updated: Jul 26 2025 at 12:43 UTC