Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] exception Size raised (line 183 of "./basis/Li...

Email Gateway (May 15 2025 at 17:40):

From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Hi List,

an innocent print_codesetup (at the end of some sizeable development)
will fail with exception Size raised (line 183 of
"./basis/LibrarySupport.sml").

Just under Main it works fine. What is happening here? And can I still
inspect the code setup?

Example:

theory Scratch
imports Refine_Imperative_HOL.IICF (* from AFP *)
begin

print_codesetup

(exception Size raised (line 183 of "./basis/LibrarySupport.sml"))
end

--

Peter

Email Gateway (May 15 2025 at 17:54):

From: Jan van Brügge <jan@vanbruegge.de>
Hi Peter,

this error is thrown when there is not enough memory for the ML process.
By default Isabelle uses the 32-bit version of PolyML, so switching on
the option "ML_system_64" should fix that.

Cheers,
Jan

Am 15.05.25 um 18:39 schrieb Peter Lammich (via cl-isabelle-users
Mailing List):

Hi List,

an innocent print_codesetup (at the end of some sizeable development)
will fail with exception Size raised (line 183 of
"./basis/LibrarySupport.sml").

Just under Main it works fine. What is happening here? And can I still
inspect the code setup?

Example:

theory Scratch
imports Refine_Imperative_HOL.IICF (* from AFP *)
begin

print_codesetup

(exception Size raised (line 183 of "./basis/LibrarySupport.sml"))
end

--

Peter

Email Gateway (May 21 2025 at 14:03):

From: Makarius <makarius@sketis.net>
On 15/05/2025 19:39, Peter Lammich (via cl-isabelle-users Mailing List) wrote:

Hi List,

an innocent print_codesetup (at the end of some sizeable development) will
fail with exception Size raised (line 183 of "./basis/LibrarySupport.sml").

Just under Main it works fine. What is happening here? And can I still inspect
the code setup?

This problem is new in Isabelle2025, because that provides much more markup in
pretty-printed output (types, terms, theorems etc.). You can avoid it by
disabling most markup like this:

declare [[show_markup = false]]

The underlying problem is a size limit for Poly/ML strings, which is 64MB for
the default 64_32 memory model. The limit is much larger for bulky 64 bit
mode. So ML_system_64 = true in etc/preferences is an alternative approach.

In the meantime I have refined the situation in various respects. The
non-scalability of print_codesetup is addressed here:

changeset: 82586:7415414bd9d8
user: wenzelm
date: Fri Apr 25 11:22:25 2025 +0200
files: src/HOL/Library/code_lazy.ML
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/Tools/Quickcheck/find_unused_assms.ML src/HOL/Tools/inductive.ML
src/Provers/classical.ML src/Pure/General/pretty.ML src/Pure/Isar/attrib.ML
src/Pure/Isar/bundle.ML src/Pure/Isar/calculation.ML src/Pure/Isar/class.ML
src/Pure/Isar/code.ML src/Pure/Isar/context_rules.ML src/Pure/Isar/method.ML
src/Pure/Isar/outer_syntax.ML src/Pure/Isar/proof_context.ML src/Pure/Pure.thy
src/Pure/Syntax/syntax.ML src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/document_antiquotation.ML src/Tools/Code/code_preproc.ML
src/Tools/induct.ML src/Tools/subtyping.ML
description:
more scalable: discontinue odd shortcuts from 6b3739fee456, which produce
bulky strings internally;

Example:

theory Scratch
imports Refine_Imperative_HOL.IICF (* from AFP *)
begin

print_codesetup

(exception Size raised (line 183 of "./basis/LibrarySupport.sml"))
end

Just for fun, I have measured the size of the output in current
Isabelle/b5b3082c9866 + AFP/d6aa42f2ef8d:

* show_markup = true: approx. 70MB
* show_markup = false: approx. 10MB

That shows that my old saying when introducing markup in pretty-printing some
decades ago is still correct: "We don't print several GBs of text". Java
String is actually limited by 1G, but both in Isabelle/ML and Isabelle/Scala
the key types Pretty.T and XML.Tree are not limited by that. Transfer of
messages now also works via Bytes.T, which can get very large.

The remaining problems are nostalgic (and usually pointless) uses of type
string, like we have seen here.

Makarius

Last updated: May 30 2025 at 04:27 UTC