Re: [isabelle-dev] exception Size raised (line 173 of ./basis/LibrarySupport.sml)
On Thu, 21 Feb 2013, Tobias Nipkow wrote: Load attached theory in HOL/IMP. Go to line done (* exception *) and you'll see the subject line. I am on parent: 51188:9b5bf1a9a710 tip The exception means that some string value has exceeded String.maxSize, which is approx. 64 MB on the 32bit platform that we are using by default everywhere. Enabling exception trace like this ML_command Toplevel.debug := true produces the following: Code_Target.prepare_serializer(17) Code_Target.mount_serializer(9) Code_Runtime.obtain_evaluator(6) Code_Runtime.evaluation(5) Code_Preproc.dynamic_value(4) Code_Evaluation.gen_dynamic_value(1)(1)(1) Value.value_cmd(4) Toplevel.apply_tr(3)(1) Florian should know what to do here. There are often easy ways to avoid huge monolithic strings, e.g. via type Buffer.T instead of string. If it turns out complicated, one needs to think again. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] exception Size raised (line 173 of ./basis/LibrarySupport.sml)
It is a fairly huge goal state that is supposed to get printed there. With all the annotations, it may exceed the limit. But why is code generation involved at that point (done)? Tobias Am 21/02/2013 15:56, schrieb Makarius: On Thu, 21 Feb 2013, Tobias Nipkow wrote: Load attached theory in HOL/IMP. Go to line done (* exception *) and you'll see the subject line. I am on parent: 51188:9b5bf1a9a710 tip The exception means that some string value has exceeded String.maxSize, which is approx. 64 MB on the 32bit platform that we are using by default everywhere. Enabling exception trace like this ML_command Toplevel.debug := true produces the following: Code_Target.prepare_serializer(17) Code_Target.mount_serializer(9) Code_Runtime.obtain_evaluator(6) Code_Runtime.evaluation(5) Code_Preproc.dynamic_value(4) Code_Evaluation.gen_dynamic_value(1)(1)(1) Value.value_cmd(4) Toplevel.apply_tr(3)(1) Florian should know what to do here. There are often easy ways to avoid huge monolithic strings, e.g. via type Buffer.T instead of string. If it turns out complicated, one needs to think again. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] exception Size raised (line 173 of ./basis/LibrarySupport.sml)
On Thu, 21 Feb 2013, Tobias Nipkow wrote: It is a fairly huge goal state that is supposed to get printed there. With all the annotations, it may exceed the limit. But why is code generation involved at that point (done)? The exception trace has no context, so I just looked in the wrong spot -- one of the later 'value' commands in the text. So Florian can ignore this thread. Trying again in TTY mode, there is indeed a huge error message produced here. It crashes when run with full annotations in Isabelle/jEdit. The computer is a finite automaton, it will always crash at some point. You can either use x86_64 for the proof development, or try to avoid such massive goals in the first place. This is how to configure x86_64 in $ISABELLE_HOME_USER/etc/settings: ML_PLATFORM=$ISABELLE_PLATFORM64 ML_HOME=$ML_HOME/../$ML_PLATFORM Note that everything that ends up in the Isabelle or AFP repository needs to run in batch mode for x86 in 32bit mode. This is faster on Linux and Mac OS X, and on Windows/Cygwin x86_64 is unavailable. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] exception Size raised (line 173 of ./basis/LibrarySupport.sml)
Now that I know that this is a resource limitation and not an error, I'm happy again. Thanks Tobias Am 21/02/2013 16:51, schrieb Makarius: On Thu, 21 Feb 2013, Tobias Nipkow wrote: It is a fairly huge goal state that is supposed to get printed there. With all the annotations, it may exceed the limit. But why is code generation involved at that point (done)? The exception trace has no context, so I just looked in the wrong spot -- one of the later 'value' commands in the text. So Florian can ignore this thread. Trying again in TTY mode, there is indeed a huge error message produced here. It crashes when run with full annotations in Isabelle/jEdit. The computer is a finite automaton, it will always crash at some point. You can either use x86_64 for the proof development, or try to avoid such massive goals in the first place. This is how to configure x86_64 in $ISABELLE_HOME_USER/etc/settings: ML_PLATFORM=$ISABELLE_PLATFORM64 ML_HOME=$ML_HOME/../$ML_PLATFORM Note that everything that ends up in the Isabelle or AFP repository needs to run in batch mode for x86 in 32bit mode. This is faster on Linux and Mac OS X, and on Windows/Cygwin x86_64 is unavailable. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] exception Size raised (line 173 of ./basis/LibrarySupport.sml)
On Thu, 21 Feb 2013, Makarius wrote:
This is how to configure x86_64 in $ISABELLE_HOME_USER/etc/settings:
ML_PLATFORM=$ISABELLE_PLATFORM64
ML_HOME=$ML_HOME/../$ML_PLATFORM
Actually doing this reveals further resource limitations. First of all,
Oracle needs to be instructed to provide a bit more heap space like this:
JEDIT_JAVA_OPTIONS=-Xms512m -Xmx4096m -Xss8m -Dactors.corePoolSize=4
-Dactors.enableForkJoin=false
See also ~~/src/Tools/jEdit/etc/settings for some more examples.
Then the goal can be printed and digested by the front-end, but it is all
very huge and takes minutes to get through.
Here is some ML snipped to get an idea about size of output:
ML_val {*
fun pr_size st =
size (Pretty.string_of (Pretty.chunks (Proof.pretty_state 1
(Toplevel.proof_of st;
pr_size @{Isar.state}; (* with PIDE markup *)
(* 139371907 *)
Print_Mode.setmp [] pr_size @{Isar.state}; (* raw output *)
(* 15882084 *)
*}
130 MB is a bit much for the whole syntax stack and editor front-end, but
it is only factor 2 beyond the 64 MB string limit in 32bit mode.
15 MB for the raw text is also quite something. We also see that PIDE
markup is only a factor 10 larger, even though it marks all formal
entities and type information for atomic subterms. (The type information
is approx. a factor of 2, but I did not measure this here.)
We are presently in this bounded 32bit address space by default, which is
2GB .. 3.5 GB depending on the platform. I find its early failure
behaviour more convenient, than denial of service of the overall system.
For example, certain situations of non-termination produce a Interrupt
exception due to stack overflow, instead of filling up VM space
indefinitely.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle (proof assistant) - Wikipedia, the free encyclopedia
Makarius wrote: I am more concerned about this wiki here: https://isabelle.in.tum.de/community since it is provided by one of the established Isabelle sites. I would still like to see a genuine Isabelle community contributing here, and doing serious maintenance. Right now it is just a scribbling board for people who were discontent with some of the official READMEs or manuals, and even that is often pointless already due to continuous updates of the official versions. Wiki is old-fashioned these days, how about using Stack Exchange for Isabelle user communication? It would open up Isabelle knowledge contrasted to the user mailing list. Of course Isabelle is too narrow a topic for an own site, but proposing a computational logic area could be an idea, having all the provers and their fans there. Of course using the existing cstheory and cs sites are options. The logic one was closed down saying that it would draw users from the philosophy site. Here is how to suggest a site: http://area51.stackexchange.com/faq What do you think about this? - Gergely ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
