Email Gateway (Aug 22 2022 at 11:48): Email Gateway (Aug 22 2022 at 11:48):From: Daniel Horne <d.horne@danielhorne.co.uk>
On 22/11/2015 19:36, Makarius wrote:
On Sun, 22 Nov 2015, Daniel Horne wrote:
I'm running into situations where the polyml executable is running
out of memory and being killed when it uses ~4Gb of memory.It is relatively rare that Isabelle applications run out of ML heap
memory. It might indicate an abnormal situation, e.g. a
non-terminating tool that allocates data structures indefinitely.
Well, this is with the 2015 distribution on either windows 7 or gentoo
linux x86_64. I'm trying to model the subset of c++ I use (mostly for
learning purposes), and I'm trying to create a set of functions that
correspond to a simple parser - namely in this case classifying whether
a particular char is valid as part of an identifier. So I created this:
fun isIdentifierStartChar:: "char ⇒ bool" where
"isIdentifierStartChar CHR ''_'' = True" |
"isIdentifierStartChar CHR ''a'' = True" |
"isIdentifierStartChar CHR ''b'' = True" |
"isIdentifierStartChar CHR ''c'' = True" |
"isIdentifierStartChar CHR ''d'' = True" |
"isIdentifierStartChar CHR ''e'' = True" |
"isIdentifierStartChar CHR ''f'' = True" |
"isIdentifierStartChar CHR ''g'' = True" |
"isIdentifierStartChar CHR ''h'' = True" |
"isIdentifierStartChar CHR ''i'' = True" |
"isIdentifierStartChar CHR ''j'' = True" |
"isIdentifierStartChar CHR ''k'' = True" |
"isIdentifierStartChar CHR ''l'' = True" |
"isIdentifierStartChar CHR ''m'' = True" |
"isIdentifierStartChar CHR ''n'' = True" |
"isIdentifierStartChar CHR ''o'' = True" |
"isIdentifierStartChar CHR ''p'' = True" |
"isIdentifierStartChar CHR ''q'' = True" |
"isIdentifierStartChar CHR ''r'' = True" |
"isIdentifierStartChar CHR ''s'' = True" |
"isIdentifierStartChar CHR ''t'' = True" |
"isIdentifierStartChar CHR ''u'' = True" |
"isIdentifierStartChar CHR ''v'' = True" |
"isIdentifierStartChar CHR ''w'' = True" |
"isIdentifierStartChar CHR ''x'' = True" |
"isIdentifierStartChar CHR ''y'' = True" |
"isIdentifierStartChar CHR ''z'' = True" |
"isIdentifierStartChar CHR ''A'' = True" |
"isIdentifierStartChar CHR ''B'' = True" |
"isIdentifierStartChar CHR ''C'' = True" |
"isIdentifierStartChar CHR ''D'' = True" |
"isIdentifierStartChar CHR ''E'' = True" |
"isIdentifierStartChar CHR ''F'' = True" |
"isIdentifierStartChar CHR ''G'' = True" |
"isIdentifierStartChar CHR ''H'' = True" |
"isIdentifierStartChar CHR ''I'' = True" |
"isIdentifierStartChar CHR ''J'' = True" |
"isIdentifierStartChar CHR ''K'' = True" |
"isIdentifierStartChar CHR ''L'' = True" |
"isIdentifierStartChar CHR ''M'' = True" |
"isIdentifierStartChar CHR ''N'' = True" |
"isIdentifierStartChar CHR ''O'' = True" |
"isIdentifierStartChar CHR ''P'' = True" |
"isIdentifierStartChar CHR ''Q'' = True" |
"isIdentifierStartChar CHR ''R'' = True" |
"isIdentifierStartChar CHR ''S'' = True" |
"isIdentifierStartChar CHR ''T'' = True" |
"isIdentifierStartChar CHR ''U'' = True" |
"isIdentifierStartChar CHR ''V'' = True" |
"isIdentifierStartChar CHR ''W'' = True" |
"isIdentifierStartChar CHR ''X'' = True" |
"isIdentifierStartChar CHR ''Y'' = True" |
"isIdentifierStartChar CHR ''Z'' = True" |
"isIdentifierStartChar a = False"
..and isabelle crashes after several minutes of it being purpled-out. I
guess it's the sheer number of terms here that's causing the problem.
The machine I'm working on has 12Gb of ram, so I thought I might
attack this problem by using a 64-bit version of the relevant programs.In order to switch the ML system into x86_64 mode, you can edit
$ISABELLE_HOME_USER/etc/settings like this:ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$ML_HOME/../$ML_PLATFORM"Isabelle/jEdit supports symbolic file names with $ literally as
written above.
Great - I'll try that, thanks.
Email Gateway (Aug 22 2022 at 11:48):From: Manuel Eberl <eberlm@in.tum.de>
I very much recommend that you define your function differently, e.g.
definition "isIdentifierStartChar c ⟷
c ∈ set ''_abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ''"
Or you can import "~~/src/HOL/Library/Char_ord" and do
definition "isIdentifierStartChar c ⟷
c ∈ set ''_abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ''"
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 11:48):From: Makarius <makarius@sketis.net>
NoteThatCamelCaseIsNotUsedInIsabelleToImproveReadability.
Makarius
Email Gateway (Aug 22 2022 at 11:48):From: bnord <bnord01@gmail.com>
When I think about, how hard it is to convince students to find the
courage to post their questions on this mailing list, comments like
these can't be overrated!
Benedikt
Email Gateway (Aug 22 2022 at 11:49):From: Manuel Eberl <eberlm@in.tum.de>
The second part should, of course read:
Or you can import "~~/src/HOL/Library/Char_ord" and do
definition "isIdentifierStartChar c ⟷
c = CHR ''_'' ∨ (c ≥ CHR ''A'' ∧ c ≤ CHR ''Z'') ∨ (c ≥ CHR ''a'' ∧ c ≤ CHR ''z'')
For code generation, this is probably the most efficient way to state it.
Email Gateway (Aug 22 2022 at 11:59):From: Daniel Horne <d.horne@danielhorne.co.uk>
Hi..
I'm running into situations where the polyml executable is running out
of memory and being killed when it uses ~4Gb of memory. The machine I'm
working on has 12Gb of ram, so I thought I might attack this problem by
using a 64-bit version of the relevant programs.
-Are there any pre-built 64-bit versions available for either windows or
linux?
-Is there an official isabelle "maintainer" for gentoo linux? I notice
that there are some builds in the portage tree, but none newer than
isabelle-2013
Thanks,
Daniel Horne
Email Gateway (Aug 22 2022 at 11:59):From: Makarius <makarius@sketis.net>
On Sun, 22 Nov 2015, Daniel Horne wrote:
I'm running into situations where the polyml executable is running out
of memory and being killed when it uses ~4Gb of memory.
It is relatively rare that Isabelle applications run out of ML heap
memory. It might indicate an abnormal situation, e.g. a non-terminating
tool that allocates data structures indefinitely.
The machine I'm working on has 12Gb of ram, so I thought I might attack
this problem by using a 64-bit version of the relevant programs.
In order to switch the ML system into x86_64 mode, you can edit
$ISABELLE_HOME_USER/etc/settings like this:
ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$ML_HOME/../$ML_PLATFORM"
Isabelle/jEdit supports symbolic file names with $ literally as written
above.
This only works on Linux and Mac OS X. For Windows, native x86-windows
and x86_64-windows support will come with the next release (at the start
of 2016). In that release, switching to 64bit will be also easier, via
a single system option.
-Are there any pre-built 64-bit versions available for either windows or
linux?
The official Isabelle application bundles are "pre-built" concerning
everything except heap images. These are built as required on demand.
Makarius
Last updated: Apr 25 2024 at 08:20 UTC