Email Gateway (Aug 19 2022 at 08:41): Email Gateway (Aug 19 2022 at 08:41):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I tried to build a heap image with "isabelle usedir", and the programme
completed - apparently successfully - but the heap image was nowhere to
be found. I then looked at the log file in the ~/.isabelle/ directory
and it turns out PolyML threw an "Insufficient Memory" exception and died.
Would it be possible to have Isabelle display an error message in these
cases so that the user knows something went wrong?
Also, if I load all these theories by hand by importing them in a theory
and loading that theory in Proof General, everything seems to work, but
when I do "isabelle usedir" with an appropriate ROOT.ML file, I get this
insufficient memory exception. The reason for that is that, apparently,
"Isabelle usedir" uses up to 6.5 GiB of memory (tested on a 64 bit
system), but the computer with which I normally work runs a 32 bit
system, so I only have 4 GiB per process.
What is the reason for this huge memory usage compared to the more
moderate requirements of loading the theories with Proof General? Is
there some workaround to build this heap image on a 32 bit system?
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 08:42):From: Makarius <makarius@sketis.net>
On Fri, 28 Sep 2012, Manuel Eberl wrote:
Also, if I load all these theories by hand by importing them in a theory
and loading that theory in Proof General, everything seems to work, but
when I do "isabelle usedir" with an appropriate ROOT.ML file, I get this
insufficient memory exception.
Traditionally, Proof General runs things with slightly different options,
such as quick_and_dirty and reduced parallel proof checking, so there can
be easily a difference to batch mode.
I am trying hard not to repeat these mistakes and consequent confusion in
the current interactive document model, the one that is used for
Isabelle/jEdit. So after a few more rounds of refinements, and when Proof
General is forgotten, such issues should no longer occur.
The reason for that is that, apparently, "Isabelle usedir" uses up to
6.5 GiB of memory (tested on a 64 bit system), but the computer with
which I normally work runs a 32 bit system, so I only have 4 GiB per
process.
You need to find out where the resources are going, i.e. which part of
your application burns them. You may try this in plain "isabelle tty"
which is a bit closer to batch mode than the Proof General interaction
mode.
Alternatively, you can ignore the problem and use current polyml-5.5.0
from here: http://isabelle.in.tum.de/components/polyml-5.5.0.tar.gz
This is the brand-new Poly/ML release, with greatly improved heap
management (parallel garbage collection and online sharing of values).
It is able to run much larger Isabelle applications even in 32bit mode.
To use the above polyml-5.5.0 component in Isabelle2012, add something
like this to your $ISABELLE_HOME_USER/etc/settings:
ML_SYSTEM=polyml-5.5.0
ML_PLATFORM="$ISABELLE_PLATFORM"
ML_HOME="/some/where/polyml-5.5.0/$ML_PLATFORM"
ML_OPTIONS="-H 500"
ML_SOURCES="$ML_HOME/../src"
Then rebuild the required images as usual via Isabelle2012/build.
Makarius
Email Gateway (Aug 19 2022 at 08:42):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
thanks for the quick reply, I should probably give the new PolyML a try
then.
However, I do not quite understand what you mean with this:
Email Gateway (Aug 19 2022 at 08:42):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
I think Makarius just means that it's generally a bad idea to have two modes, because it's more likely that at least one of them will break.
I don't know for the other options, but "quick and dirty" is certainly not a good idea in general, as illustrated recently on this mailing list by Brian Huffman, who derived "False" by exploiting a bug in the "datatype" package. Then you're thankful that your command-line-based nightly tests have it disabled.
Jasmin
Email Gateway (Aug 19 2022 at 08:42):From: Manuel Eberl <eberlm@in.tum.de>
Brilliant, worked like a charm. Thanks a lot!
Email Gateway (Aug 19 2022 at 08:52):From: Tobias Nipkow <nipkow@in.tum.de>
Am 28/09/2012 17:26, schrieb Jasmin Blanchette:
Am 28.09.2012 um 16:54 schrieb Manuel Eberl:
In my case, loading everything in Proof General works, loading
everything in batch mode does not work. Based on that, I would argue
that whatever options Proof General does run things with are a good
idea, not a mistake. Therefore, I cannot quite follow your reasoning here.I think Makarius just means that it's generally a bad idea to have two modes, because it's more likely that at least one of them will break.
I don't know for the other options, but "quick and dirty" is certainly not a good idea in general, as illustrated recently on this mailing list by Brian Huffman, who derived "False" by exploiting a bug in the "datatype" package.
I beg to differ. It has saved users countless hours waiting for packages to
perform long routine proofs. So it certainly was of great benefit at the time.
And if you think green IT...
Then you're thankful that your command-line-based nightly tests have it disabled.
Anything else would be throwing the baby out with the bath water.
Tobias
Jasmin
Email Gateway (Aug 19 2022 at 08:56):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Am 01.10.2012 um 05:33 schrieb Tobias Nipkow:
Am 28/09/2012 17:26, schrieb Jasmin Blanchette:
I don't know for the other options, but "quick and dirty" is certainly not a good idea in general, as illustrated recently on this mailing list by Brian Huffman, who derived "False" by exploiting a bug in the "datatype" package.
I beg to differ. It has saved users countless hours waiting for packages to
perform long routine proofs. So it certainly was of great benefit at the time.
And if you think green IT...
By "in general", I meant "as the default for both interactive and noninteractive". (Remember: Manuel was suggesting making the PG defaults the defaults for command-line.) I'm a big fan of quick-and-dirty for the interactive mode myself, as can be seen from the source code of the new (co)datatype package (grep quick_and_dirty ~/isabelle/src/HOL/BNF/Tools/*ML).
When it comes to having one vs. two modes, my comment was meant as a general programming guideline, not an actual opinion of mine on this specific case:
I think Makarius just means that it's generally a bad idea to have two modes, because it's more likely that at least one of them will break.
It's just one of many usually conflicting criteria that must be considered when developing software.
Jasmin
Email Gateway (Aug 19 2022 at 08:58):From: Tobias Nipkow <nipkow@in.tum.de>
Am 01/10/2012 10:25, schrieb Jasmin Blanchette:
Am 01.10.2012 um 05:33 schrieb Tobias Nipkow:
Am 28/09/2012 17:26, schrieb Jasmin Blanchette:
I don't know for the other options, but "quick and dirty" is certainly not a good idea in general, as illustrated recently on this mailing list by Brian Huffman, who derived "False" by exploiting a bug in the "datatype" package.
I beg to differ. It has saved users countless hours waiting for packages to
perform long routine proofs. So it certainly was of great benefit at the time.
And if you think green IT...By "in general", I meant "as the default for both interactive and noninteractive". (Remember: Manuel was suggesting making the PG defaults the defaults for command-line.) I'm a big fan of quick-and-dirty for the interactive mode myself, as can be seen from the source code of the new (co)datatype package (grep quick_and_dirty ~/isabelle/src/HOL/BNF/Tools/*ML).
Sorry, I misunderstood you. Then we are in violent agreement ;-)
Tobias
When it comes to having one vs. two modes, my comment was meant as a general programming guideline, not an actual opinion of mine on this specific case:
I think Makarius just means that it's generally a bad idea to have two modes, because it's more likely that at least one of them will break.
It's just one of many usually conflicting criteria that must be considered when developing software.
Jasmin
Email Gateway (Aug 19 2022 at 08:59):From: Makarius <makarius@sketis.net>
Having "modes", i.e. opportunities for slightly changed behaviour is
indeed evil in its own right. In the end the possibilities of every
system component that might change its behaviour are multiplied, so you
get an exponential number of oddities in the worst case.
The traditional "interactive mode" vs. "batch mode" has accumulated quite
a few such oddities over time, and it will take a few more years to chop
off most of the heads of the hydra.
Quick and dirty mode is a well-known special case of this principle, and
Proof General has depended on it a lot, and will continue to do so,
because it is not moving anymore.
These things need to be understood from their historic context and
technical side-condutions. In the next Isabelle release, the regular
Isabelle/jEdit interaction mode will already work smoothly without quick
and dirty, because proofs are parallel by default, and not so expensive
after all in the overall bilance.
At some later stage the competiting "skip_proofs" feature should be
somehow integrated into the parallel interaction model, lets say as forked
proofs that are deferred for much longer, or indefinitely.
Makarius
Last updated: Apr 24 2024 at 20:16 UTC