Discussion:
[isabelle] 64 bit distro available?
(too old to reply)
Daniel Horne
2015-11-22 19:27:44 UTC
Permalink
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
Makarius
2015-11-22 19:38:24 UTC
Permalink
Post by Daniel Horne
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.
Post by Daniel Horne
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.
Post by Daniel Horne
-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
Daniel Horne
2015-11-22 20:44:45 UTC
Permalink
Post by Makarius
Post by Daniel Horne
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.
Post by Makarius
Post by Daniel Horne
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
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.
Manuel Eberl
2015-11-22 20:55:57 UTC
Permalink
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
Post by Daniel Horne
Post by Makarius
Post by Daniel Horne
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
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.
Post by Makarius
Post by Daniel Horne
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
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.
Manuel Eberl
2015-11-24 13:45:44 UTC
Permalink
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.
Post by Manuel Eberl
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
Post by Daniel Horne
Post by Makarius
Post by Daniel Horne
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
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.
Post by Makarius
Post by Daniel Horne
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
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.
Makarius
2015-11-22 21:44:52 UTC
Permalink
fun isIdentifierStartChar:: "char ⇒ bool" where
NoteThatCamelCaseIsNotUsedInIsabelleToImproveReadability.


Makarius
bnord
2015-11-23 15:43:35 UTC
Permalink
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
Post by Makarius
Post by Daniel Horne
fun isIdentifierStartChar:: "char ⇒ bool" where
NoteThatCamelCaseIsNotUsedInIsabelleToImproveReadability.
Makarius
Loading...