Email Gateway (Aug 22 2022 at 20:32): Email Gateway (Aug 22 2022 at 20:32):From: Walther Neuper <walther.neuper@jku.at>
Building our project by "isabelle jedit" leads to
exception Size raised (line 171 of "./basis/LibrarySupport.sml")
at several places for some time already. But "isabelle build" works fine
over all code without exceptions, so we didn't care so far. We use the
standard etc/setting
ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0 -Djdk.gtk.version=2.2"
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss16m"
for this operating system and hardware:
Ubuntu 16.04 LTS
Memory: 15,3 GiB
Processor: ntel® Core™ i7-4810MQ CPU @ 2.80GHz × 8
Since update to Isabelle2019, however, the same exception is raised
several times within our test-suite (which uses series of "ML_file
*.sml" [1]) and we have to out-comment parts of tests (which we don't
like at all). So the question:
Is there a way to bypass limitations of Java buffers and run a
test-suite using a kind of "isabelle build" ?
Many thanks in advance,
Walther
[1] https://hg.risc.uni-linz.ac.at/wneuper/isa/file/5c4230e32124/test/Tools/isac/Test_Isac.thy
Email Gateway (Aug 22 2022 at 20:32):From: Makarius <makarius@sketis.net>
This is a limitation of Poly/ML in 32bit address mode: that is always
used by default in Isabelle2019, because of the great new x86_64_32 mode
of Poly/ML 5.8.
The limitation is approx. 64MB for single items on the heap, e.g.
strings. So there must be something rather big in your application, e.g.
a huge XML tree printed in YXML.
It would be better to figure out where this happens, but it should work
as before if you add this to $ISABELLE_HOME_USER/etc/preferences:
ML_system_64 = "true"
Makarius
Email Gateway (Aug 22 2022 at 20:32):From: Walther Neuper <walther.neuper@jku.at>
thank you for the quick answer.
Our quick trial with ML_system_64 = "true" did not help, so we shall
find tools to figure out in detail, what is going on here.
Walther
This is a limitation of Poly/ML in 32bit address mode: that is always
used by default in Isabelle2019, because of the great new x86_64_32 mode
of Poly/ML 5.8.
The limitation is approx. 64MB for single items on the heap, e.g.
strings. So there must be something rather big in your application, e.g.
a huge XML tree printed in YXML.
It would be better to figure out where this happens, but it should work
as before if you add this to $ISABELLE_HOME_USER/etc/preferences:
ML_system_64 = "true"
Makarius
Email Gateway (Aug 22 2022 at 20:33):From: Makarius <makarius@sketis.net>
It is unlikely that you get a Size exception in full x86_64 mode.
Do you really have this enabled? You can check within the running
Isabelle session as follows:
ML ‹open ML_System›
Makarius
Email Gateway (Aug 22 2022 at 20:33):From: Walther Neuper <walther.neuper@jku.at>
This gives
val platform_is_windows = false: bool
val platform = "x86_64_32-linux": string
val standard_path = fn: string -> string
val name = "polyml-5.8": string
val platform_is_64 = false: bool
val platform_path = fn: string -> string
in spite of
~/.isabelle$ cat etc/preferences
(* generated by Isabelle Sat Dec 05 14:56:44 CET 2015 *)
ML_system_64 = "true"
Might these preferences be overridden somehow?
Walther
Email Gateway (Aug 22 2022 at 20:33):From: Makarius <makarius@sketis.net>
You need to use the proper ISABELLE_HOME_USER directory. The
command-line "isabelle getenv ISABELLE_HOME_USE" will tell you where it is.
Makarius
Email Gateway (Aug 22 2022 at 20:34):From: Walther Neuper <walther.neuper@jku.at>
right, sorry for inattention.
But now I struggle with an unexpected reset of the preferences:
Updating in ISABELLE_HOME to
isabisacREP$ cat etc/preferences
(* generated by Isabelle 14-Sep-2019 12:34:51 +0200 *)
(* avoid exception Size raised (line 171 of "./basis/LibrarySupport.sml") *)
ML_system_64 = "true"
and in ISABELLE_HOME_USER to
~/.isabelle$ cat isabisacREP/etc/preferences
(* generated by Isabelle 14-Sep-2019 12:34:51 +0200 *)
(* avoid exception Size raised (line 171 of "./basis/LibrarySupport.sml") *)
ML_system_64 = "true"
causes running Isabelle
isabisacREP$ ./bin/isabelle jedit &
?!?--------- to reset ---------?!? in ISABELLE_HOME_USER to
~/.isabelle$ cat isabisacREP/etc/preferences
(* generated by Isabelle 14-Sep-2019 13:12:44 +0200 *)
Scanning system.pdf seems not to explain this kind of reset of
preferences, the system behaviour (exn Size) didn't change and from
isabisacREP$ ./bin/isabelle jedit &
:
ML ‹open ML_System›
:
we still get
val platform_is_windows = false: bool
val platform = "x86_64_32-linux": string
val standard_path = fn: string -> string
val name = "polyml-5.8": string
val platform_is_64 = false: bool <<<==========================
val platform_path = fn: string -> string
What would inhibit the reset, or how/where must <ML_system_64 = "true">
be applied in order to make an effect ?
Walther
PS:
(1) switching to shell format
# avoid exception Size raised (line 171 of "./basis/LibrarySupport.sml")
doesn't change anything.
(2) The Isabelle installation used above is described here
https://isac.miraheze.org/wiki/Fix_kernel_installation
Email Gateway (Aug 22 2022 at 20:34):From: Makarius <makarius@sketis.net>
This "lost update" is to be expected: when you have "isabelle jedit"
still running, it will re-generate the preferences file on shutdown. See
also section 1.2.3 in the Isabelle/jEdit manual.
Inside Isabelle/jEdit you can actually use the plugin options panel to
edit this option.
Makarius
Last updated: Apr 30 2024 at 16:19 UTC