Email Gateway (Aug 22 2022 at 12:39): Email Gateway (Aug 22 2022 at 12:39):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
I'm trying to start RC3 jEdit with Collections pre-loaded. I'm using
afp-devel 138306721319. I also tried it with a less recent version
which worked on RC2.
For a fresh start, I deleted my .isabelle/Isabelle-2016-RC3 directory.
I started Isabelle from the afp-devel toplevel with
~/Downloads/Isabelle2016-RC3/bin/isabelle jedit -d thys/ -l Collections
It starts building everything, starting from session HOL in the jEdit window.
At some point (Collections), the build just fails. These are the last
parts of the output:
...
Collections: theory Refine_Monadic_Userguide
Collections FAILED
(see also /home/diekmann/.isabelle/Isabelle2016-RC3/heaps/polyml-5.6_x86-linux/log/Collections)
Int_of_integer 3072, (),
Branch
(B, Branch (..., ...), Int_of_integer 3584, ...))),
Int_of_integer 4096, (),
Branch
(B, Branch
(B, Branch
(B, Branch (..., ...), Int_of_integer 4608, ...),
Int_of_integer 5120, (),
Branch (B, Branch (..., ...), Int_of_integer 5632, ...)),
Int_of_integer 6144, (),
Branch
(B, Branch (B, Branch (..., ...), Int_of_integer 6656, ...),
Int_of_integer 7168, (),
Branch (B, Branch (..., ...), Int_of_integer 7680, ...))))
):
(Isabelle1955749.Generated_Code.inta, unit)
Isabelle1955749.Generated_Code.rbt
val it = (): unit
ML> Exception- Fail "Insufficient memory" raised
Unfinished session(s): Collections
Return code: 1
Session build failed -- prover process remains inactive!
When the build is at "Collections: theory Refine_Monadic_Userguide",
at most 5.8GB RAM of 7.8GB RAM are used on my system (tested three
times).
However, when I cd to thys and start isabelle with
~/Downloads/Isabelle2016-RC3/bin/isabelle jedit -d . -l Collections
it works fine.
I could reproduce this several times (3 tests each, always the same
behavior). It does not look like a _random_ memory shortage to me. The
whole thing worked fine with the previous RCs.
This behavior does not occur with the command line build. I.e.
~/Downloads/Isabelle2016-RC3/bin/isabelle build -d thys -v Collections
works fine.
My system has 8GB of RAM, 2 physical cores + hyperthreading, Linux
ubuntu 14.04, unity.
Best Regards,
Cornelius
Email Gateway (Aug 22 2022 at 12:44):From: Peter Lammich <lammich@in.tum.de>
This error is strange, and we should be careful not to rule out building
big sessions without really big machines. Btw Collections is of moderate
size, compared to, eg, JinjaThreads.
Is there any way to measure how "close" a build comes to an
out-of-memory error, to figure out whether something serious happened
between RC2 and RC3, or whether on RC2 the build ran at 99% of available
memory, on on RC3 it happens to be 101%.
Email Gateway (Aug 22 2022 at 12:44):From: "C. Diekmann" <diekmann@in.tum.de>
2016-02-02 18:45 GMT+01:00 Peter Lammich <lammich@in.tum.de>:
This error is strange, and we should be careful not to rule out building
big sessions without really big machines.
I agree. My office laptop has 8GB of RAM. It would be really hard if
this is not enough for Isabelle. Students often have laptops with less
RAM.
This thread should be called: Isabelle2016 uses too much RAM.
For the way I (personally) use Isabelle, this would be release-critical.
<off topic>
I started buying big machines after I got familiar with Isabelle. I
was a happy intel atom 1GM RAM user before that. But Isabelle was
working okay in 2012 on that device. I understand that these times are
long gone. But requiring more that a common, up-to-date, medium-class,
off-the-shelf laptop to run Isabelle will make it really hard to get
new users or to use Isabelle in a lecture.
</off topic>
Btw Collections is of moderate
size, compared to, eg, JinjaThreads.
<more off topic>
If Collections is medium-sized, does this mean this theory can
determine the minimum amount of RAM necessary to do something useful
with Isabelle? Should this information be on the website?
</more off topic>
Is there any way to measure how "close" a build comes to an
out-of-memory error, to figure out whether something serious happened
between RC2 and RC3, or whether on RC2 the build ran at 99% of available
memory, on on RC3 it happens to be 101%.
I booted my machine with only 6BG of ram (kernel option) and now the
build also fails at the same position with RC2.
Isabelle 2015 (with my 2015 snapshot of the afp, which makes the whole
measurement not comparable) can build Collection on 6GB RAM. But there
was a moment where it "felt like" I almost ran out of RAM.
Cornelius
On Di, 2016-02-02 at 18:26 +0100, C. Diekmann wrote:
Thanks.
If I build it with "isabelle build -d . -b Collections", I also get
the "Insufficient memory" error.With RC2, the same works fine. I can run the following without any problems:
$ISABELLE build -d $AFP -v -b Collections
$ISABELLE jedit -d $AFP -l CollectionsIt should be possible to build Collections with only 8GB of RAM,
right? I know that a student used this entry in 2015 with a 4GB RAM
laptop. Something seems to eat up the RAM in RC3 when finalizing* the
session image.*) I'm just guessing that it happens at finalizing because the
out-of-memory occurs at the last theory and does not occur if I omit
the "-b" option.Best Regards,
Cornelius2016-02-02 17:04 GMT+01:00 Makarius <makarius@sketis.net>:
On Tue, 2 Feb 2016, C. Diekmann wrote:
Now I also get the error when I build from the current directory.
~/Downloads/Isabelle2016-RC3/bin/isabelle jedit -d . -l CollectionsIf I build Collections first on the command line
~/Downloads/Isabelle2016-RC3/bin/isabelle build -d . -v Collections
the build works.
If I try to load it in jEdit (previous command), it is building
Collections again, but not its dependencies. Shouldn't it load
Collections now without building? The jEdit build fails with the
previously mentioned error.You need to build a session image using "isabelle build -b".
That also makes a difference in resource requirements.
Makarius
Email Gateway (Aug 22 2022 at 12:45):From: Peter Lammich <lammich@in.tum.de>
Have you used 64bit poly? What happens on 32bit poly?
\-------- Originalnachricht --------
Email Gateway (Aug 22 2022 at 12:45):From: Makarius <makarius@sketis.net>
The NEWS file says again that resource requirements have been reduced.
Interestingly that has been a theme of all releases of the last years.
Whenever the resource requirements of the systems are reduced,
applications fill up the free space again.
I don't complain about that, it is just how things work. You merely need
to be slightly above average in hardware capacities to cope with that.
8 GB is below that average. Further below are small mobile devices, not
proper computers.
Makarius
Email Gateway (Aug 22 2022 at 12:45):From: Makarius <makarius@sketis.net>
Using Poly/ML with x86_64 is actually a common mistake -- it is the
default on most Linux installations, but the Isabelle installation
instructions say explicitly that 32bit libraries should be installed.
We are back to the question how much documentation people want to use.
Anybody with higher-than average requirements should peek at advanced
texts occasionally.
What also helps under tight ML heap conditions to is vary the ML_OPTIONS a
bit, concerning the initial heap size. This changes the way how Poly/ML
grows and shrinks the heap, and sometimes it makes a difference.
Makarius
Email Gateway (Aug 22 2022 at 12:45):From: Lawrence Paulson <lp15@cam.ac.uk>
I’ve used an 8 GB laptop (Macbook Pro) for years, generally with success. Of course things are better with a bigger machine, but it’s not essential.
Larry
Email Gateway (Aug 22 2022 at 12:45):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
On 03/02/16 09:35, Makarius wrote:
On Tue, 2 Feb 2016, Peter Lammich wrote:
Have you used 64bit poly? What happens on 32bit poly?
Using Poly/ML with x86_64 is actually a common mistake -- it is the default on most Linux installations, but the
Isabelle installation instructions say explicitly that 32bit libraries should be installed.
Maybe I'm missing some context for this statement, but why is using 64-bit Poly/ML a mistake? This is what I use and, as
far as I'm aware, is the default configuration in the l4.verified proofs setup [0]. I don't have a deep knowledge of the
Poly/ML implementation but my understanding is that, while the 64-bit version uses more memory to accomplish the same
thing, you must use it if you want to use more than N bytes of RAM (for some N; 4GB?). If this is not the case, I
would love to be enlightened as to how to better configure my system.
[0]: https://github.com/seL4/l4v/blob/master/misc/etc/settings#L19
We are back to the question how much documentation people want to use. Anybody with higher-than average requirements
should peek at advanced texts occasionally.What also helps under tight ML heap conditions to is vary the ML_OPTIONS a bit, concerning the initial heap size. This
changes the way how Poly/ML grows and shrinks the heap, and sometimes it makes a difference.Makarius
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 12:45):From: "C. Diekmann" <diekmann@in.tum.de>
2016-02-02 23:35 GMT+01:00 Makarius <makarius@sketis.net>:
On Tue, 2 Feb 2016, Peter Lammich wrote:
Have you used 64bit poly? What happens on 32bit poly?
Using Poly/ML with x86_64 is actually a common mistake -- it is the default
on most Linux installations, but the Isabelle installation instructions say
explicitly that 32bit libraries should be installed.
I'm not getting the "bulky 64bit version" warning when i start jEdit
or build, so I guess that I'm using the 32bit library.
We are back to the question how much documentation people want to use.
Anybody with higher-than average requirements should peek at advanced texts
occasionally.
Is Isabelle2016 still issuing a warning on startup if the 64bit
libraries are used?
Cornelius
Email Gateway (Aug 22 2022 at 12:46):From: David Matthews <dm@prolingua.co.uk>
Actually, that used to be the case. At one time the initial heap size
was also used to calculate the increment if the heap needed to be
expanded. Since Poly/ML 5.5 the heap sizing is adjusted depending on
the GC load. The heap size is only adjusted after a major GC so if you
know you're going to need a large heap it may help to set the minimum
size before you start.
David
Email Gateway (Aug 22 2022 at 12:47):From: Makarius <makarius@sketis.net>
For more than 3 years big Isabelle applications are usually run in
constant space of approx. 3.5 GB, i.e. the maximum on 32bit. This applies
to all of Isabelle + AFP, and is usually the most efficient way on small
and big machines.
Applications that really need more GBs -- presumably l4.verified is the
only one on the planet -- there is no other way than to move on to bigger
machines and the 64bit model.
What kind of hardware do l4.verified people use for that?
Makarius
Email Gateway (Aug 22 2022 at 12:47):From: Makarius <makarius@sketis.net>
Not any longer. This warning usually showed up in unexpected situations,
and did not show up when the standard Isabelle application wrapper was
used.
There were various changes in the auto-configuration of 32bit vs. 64bit
platforms, both for the ML system and the JVM. You now get this
information in the title of the build dialog on the first startup, but it
is possible to overlook it. (And sometimes people think that 64bit is
always better than 32bit.)
I was thinking of an additional warning dialog for a situation where the
option ML_system_64 is not set (i.e. the default of Isabelle), but the
result forced to x86_64-linux due to lack of 32bit g++ libraries (i.e. the
default of most Linux installations). I did not do it, because it may
cause puzzlement to new users or casual users, e.g. of introductory
Isabelle tutorials. The difference is only relevant to really big
applications.
Isabelle power users, especially on Linux, need to do some more
fine-tuning to get various side-conditions right. The details are listed
here: http://isabelle.in.tum.de/website-Isabelle2016-RC3/installation.html
Makarius
Email Gateway (Aug 22 2022 at 12:47):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Raf Kolanski can probably provide details about our server, but for my own desktop machine I have an Intel i7 with 32GB
RAM. On my current proofs I regularly exceed 20GB.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 12:47):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
The standard desktop setup is 32GB RAM with a higher-end quadcore i7. This allow you to run 2 sessions in parallel without too much trouble. Without memory pressure it’ll take about 20GB, but with GC it should fit into 16GB (it’s very close to that 16GB limit, sometimes over sometimes under, depending on changes in proofs, Isabelle, polyml, Linux or Mac, etc).
Server side we’re currently running an 8-core i7 with 128GB, but it’s getting a bit old and is in need of a refresh.
Most of the proofs do actually run fine on a 8GB laptop. It’s only the later stages and C-level proofs that need that much memory.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 12:47):From: Christian Sternagel <c.sternagel@gmail.com>
Make this at least 2. IsaFoR already fails to build its session HOL-AFP
(which just brings together all the necessary theories from the AFP) in
32bit mode.
We are using the following hardware (our "build server", a workstation
especially for people in my lab working on IsaFoR):
cpu: i7 (12 Cores a la 3.5 Ghz)
mem: 32 GB
In principle it is also possible to build IsaFoR on my "laptop" (due to
its weight you might argue that it classifies as such):
cpu: i7 (4 Cores a la 2.4 Ghz)
mem: 16 GB
However, this makes my laptop completely unusable for about 1h and thus
I usually prefer to build heap images on the "build server" and then
rsync them over onto my laptop.
cheers
chris
PS: HOL-AFP pulls in the following theories
Building HOL-AFP ...
HOL-AFP: theory AssocList
HOL-AFP: theory Bit
HOL-AFP: theory Bits
HOL-AFP: theory Boolean_Algebra
HOL-AFP: theory Comparator
HOL-AFP: theory Derive_Manager
HOL-AFP: theory Equal
HOL-AFP: theory Divmod_Int
HOL-AFP: theory Error_Syntax
HOL-AFP: theory Extend_Partial_Order
HOL-AFP: theory Foldi
HOL-AFP: theory Missing_Ring
HOL-AFP: theory Closure_Set
HOL-AFP: theory FunctionLemmas
HOL-AFP: theory Generator_Aux
HOL-AFP: theory IArray
HOL-AFP: theory ICF_Tools
HOL-AFP: theory Infinite_Sequences
HOL-AFP: theory Omega_Words_Fun
HOL-AFP: theory Least_Enum
HOL-AFP: theory List_Fusion
HOL-AFP: theory Misc_Numeric
HOL-AFP: theory Misc_Typedef
HOL-AFP: theory Bit_Representation
HOL-AFP: theory Containers_Auxiliary
HOL-AFP: theory Error_Monad
HOL-AFP: theory Efficient_Sort
HOL-AFP: theory Bits_Bit
HOL-AFP: theory Equality_Generator
HOL-AFP: theory List_More
HOL-AFP: theory Compare
HOL-AFP: theory Comparator_Generator
HOL-AFP: theory IArray_Addenda
HOL-AFP: theory Missing_Multiset
HOL-AFP: theory Quicksort
HOL-AFP: theory IArray_Haskell
HOL-AFP: theory Nat_Bijection
HOL-AFP: theory Old_Datatype
HOL-AFP: theory Option_ord
HOL-AFP: theory Equality_Instances
HOL-AFP: theory Ord_Code_Preproc
HOL-AFP: theory Bits_Int
HOL-AFP: theory Partial_Function_MR
HOL-AFP: theory Numeral_Type
HOL-AFP: theory Locale_Code
HOL-AFP: theory Containers_Generator
HOL-AFP: theory Improved_Code_Equations
HOL-AFP: theory Check_Monad
HOL-AFP: theory Strict_Sum
HOL-AFP: theory Collection_Enum
HOL-AFP: theory Collection_Eq
HOL-AFP: theory Lexicographic_Order
HOL-AFP: theory Missing_Polynomial
HOL-AFP: theory Compare_Generator
HOL-AFP: theory Neville_Aitken_Interpolation
HOL-AFP: theory Set_Linorder
HOL-AFP: theory Compare_Instances
HOL-AFP: theory Compare_Rat
HOL-AFP: theory Compare_Real
HOL-AFP: theory Type_Length
HOL-AFP: theory DList_Set
HOL-AFP: theory Prio_List
HOL-AFP: theory Lagrange_Interpolation
HOL-AFP: theory Product_Lexorder
HOL-AFP: theory RBT_Comparator_Impl
HOL-AFP: theory Bool_List_Representation
HOL-AFP: theory RBT_Compare_Order_Impl
HOL-AFP: theory RBT_ext
HOL-AFP: theory Record_Intf
HOL-AFP: theory Refine_Chapter
HOL-AFP: theory Compare_Order_Instances
HOL-AFP: theory Misc
HOL-AFP: theory Countable
HOL-AFP: theory Refine_Util
HOL-AFP: theory Anti_Unification
HOL-AFP: theory Attr_Comb
HOL-AFP: theory Autoref_Data
HOL-AFP: theory Mk_Term_Antiquot
HOL-AFP: theory Missing_Permutations
HOL-AFP: theory Mpat_Antiquot
HOL-AFP: theory Named_Sorted_Thms
HOL-AFP: theory Tagged_Solver
HOL-AFP: theory Regular_Set
HOL-AFP: theory Restricted_Predicates
HOL-AFP: theory Indep_Vars
HOL-AFP: theory More_Bits_Int
HOL-AFP: theory Mk_Record_Simp
HOL-AFP: theory RingModuleFacts
HOL-AFP: theory Select_Solve
HOL-AFP: theory Seq
HOL-AFP: theory Show
HOL-AFP: theory Countable_Generator
HOL-AFP: theory Minimal_Elements
HOL-AFP: theory Regular_Exp
HOL-AFP: theory Multiset_Extension
HOL-AFP: theory Sublist
HOL-AFP: theory Poly_Deriv
HOL-AFP: theory Conjugate
HOL-AFP: theory Missing_Unsorted
HOL-AFP: theory CauchysMeanTheorem
HOL-AFP: theory Parser_Monad
HOL-AFP: theory MonoidSums
HOL-AFP: theory Show_Instances
HOL-AFP: theory Show_Real
HOL-AFP: theory Bits_Integer
HOL-AFP: theory Misc_Polynomial
HOL-AFP: theory Show_Complex
HOL-AFP: theory LinearCombinations
HOL-AFP: theory Sqrt_Babylonian_Auxiliary
HOL-AFP: theory Sturm_Library
HOL-AFP: theory Sturm_Theorem
HOL-AFP: theory Xml
HOL-AFP: theory Transitive_Closure_Impl
HOL-AFP: theory Utility
HOL-AFP: theory Order_Polynomial
HOL-AFP: theory Is_Rat_To_Rat
HOL-AFP: theory Prime_Field
HOL-AFP: theory Show_Poly
HOL-AFP: theory NthRoot_Impl
HOL-AFP: theory NDerivative
HOL-AFP: theory Relation_Interpretation
HOL-AFP: theory Transitive_Closure_List_Impl
HOL-AFP: theory Missing_List
HOL-AFP: theory Word_Miscellaneous
HOL-AFP: theory Ring_Hom
HOL-AFP: theory Prime_Factorization
HOL-AFP: theory Polynomial_Field
HOL-AFP: theory Matrix
HOL-AFP: theory Missing_Fraction_Field
HOL-AFP: theory Word
HOL-AFP: theory Sqrt_Babylonian
HOL-AFP: theory Ring_Hom_Poly
HOL-AFP: theory Explicit_Roots
HOL-AFP: theory SetIterator
HOL-AFP: theory Digraph_Basic
HOL-AFP: theory Bivariate_Polynomials
HOL-AFP: theory Xmlt
HOL-AFP: theory Complex_Roots_Real_Poly
HOL-AFP: theory Dvd_Int_Poly
HOL-AFP: theory Gauss_Lemma
HOL-AFP: theory Refine_Lib
HOL-AFP: theory Newton_Interpolation
HOL-AFP: theory SetIteratorOperations
HOL-AFP: theory Unique_Factorization_Domain
HOL-AFP: theory Autoref_Phases
HOL-AFP: theory Autoref_Tagging
HOL-AFP: theory Refine_Mono_Prover
HOL-AFP: theory Relators
HOL-AFP: theory Equivalence_Checking
HOL-AFP: theory Code_Target_Bits_Int
HOL-AFP: theory Rational_Root_Test
HOL-AFP: theory Code_Target_ICF
HOL-AFP: theory Regexp_Method
HOL-AFP: theory Gauss_Jordan
HOL-AFP: theory Show_Matrix
HOL-AFP: theory Ring_Hom_Matrix
HOL-AFP: theory Param_Tool
HOL-AFP: theory Abstract_Rewriting
HOL-AFP: theory Almost_Full
HOL-AFP: theory Param_HOL
HOL-AFP: theory Collection_Order
HOL-AFP: theory RTrancl
HOL-AFP: theory Minimal_Bad_Sequences
HOL-AFP: theory Parametricity
HOL-AFP: theory Proper_Iterator
HOL-AFP: theory Autoref_Id_Ops
HOL-AFP: theory SetIteratorGA
HOL-AFP: theory Almost_Full_Relations
HOL-AFP: theory Polynomial_Interpolation
HOL-AFP: theory Column_Operations
HOL-AFP: theory It_to_It
HOL-AFP: theory Well_Quasi_Orders
HOL-AFP: theory Gauss_Jordan_Field
HOL-AFP: theory Polynomial_Divisibility
HOL-AFP: theory Autoref_Fix_Rel
HOL-AFP: theory Derivation_Bound
HOL-AFP: theory Relative_Rewriting
HOL-AFP: theory RBT_Mapping2
HOL-AFP: theory SN_Orders
HOL-AFP: theory Decreasing_Diagrams_II_Aux
HOL-AFP: theory Kruskal
HOL-AFP: theory Word_Misc
HOL-AFP: theory Determinant
HOL-AFP: theory Square_Free_Factorization
HOL-AFP: theory Unique_Factorization_Poly
HOL-AFP: theory Autoref_Translate
HOL-AFP: theory Autoref_Relator_Interface
HOL-AFP: theory Autoref_Gen_Algo
HOL-AFP: theory Decreasing_Diagrams_II
HOL-AFP: theory Autoref_Tool
HOL-AFP: theory Uint32
HOL-AFP: theory SumSpaces
HOL-AFP: theory RBT_Set2
HOL-AFP: theory Autoref_Bindings_HOL
HOL-AFP: theory Char_Poly
HOL-AFP: theory Determinant_Impl
HOL-AFP: theory Ordered_Semiring
HOL-AFP: theory Polynomials
HOL-AFP: theory SN_Order_Carrier
HOL-AFP: theory VectorSpace
HOL-AFP: theory HashCode
HOL-AFP: theory Berlekamp_Hensel_Factorization
HOL-AFP: theory Precomputation
HOL-AFP: theory Set_Impl
HOL-AFP: theory Matrix_Comparison
HOL-AFP: theory Jordan_Normal_Form
HOL-AFP: theory Hash_Generator
HOL-AFP: theory Kronecker_Factorization
HOL-AFP: theory Hash_Instances
HOL-AFP: theory Derive
HOL-AFP: theory Automatic_Refinement
HOL-AFP: theory Idx_Iterator
HOL-AFP: theory Refine_Misc
HOL-AFP: theory RefineG_Domain
HOL-AFP: theory RefineG_Transfer
HOL-AFP: theory Show_Arctic
HOL-AFP: theory Complexity_Carrier
HOL-AFP: theory RefineG_Assert
HOL-AFP: theory RefineG_Recursion
HOL-AFP: theory Refine_Basic
HOL-AFP: theory RefineG_While
HOL-AFP: theory Rational_Factorization
HOL-AFP: theory Refine_Det
HOL-AFP: theory Matrix_Complexity
HOL-AFP: theory Refine_Heuristics
HOL-AFP: theory Refine_Leof
HOL-AFP: theory Refine_Pfun
HOL-AFP: theory Refine_While
HOL-AFP: theory Algebraic_Numbers_Prelim
HOL-AFP: theory Refine_Transfer
HOL-AFP: theory Autoref_Monadic
HOL-AFP: theory Refine_Automation
HOL-AFP: theory Refine_Foreach
HOL-AFP: theory Missing_VectorSpace
HOL-AFP: theory VS_Connect
HOL-AFP: theory Sturm_Rat
HOL-AFP: theory Refine_Monadic
HOL-AFP: theory Gen_Iterator
HOL-AFP: theory Iterator
HOL-AFP: theory ICF_Spec_Base
HOL-AFP: theory RBT_add
HOL-AFP: theory Gram_Schmidt
HOL-AFP: theory Matrix_Kernel
HOL-AFP: theory MapSpec
HOL-AFP: theory SetSpec
HOL-AFP: theory Mapping_Impl
HOL-AFP: theory Compare_Complex
HOL-AFP: theory Matrix_IArray_Impl
HOL-AFP: theory Schur_Decomposition
HOL-AFP: theory Jordan_Normal_Form_Uniqueness
HOL-AFP: theory Map_To_Mapping
HOL-AFP: theory Resultant
HOL-AFP: theory Containers
HOL-AFP: theory Compatibility_Containers_Regular_Sets
HOL-AFP: theory SetIteratorCollectionsGA
HOL-AFP: theory MapGA
HOL-AFP: theory SetGA
HOL-AFP: theory Jordan_Normal_Form_Existence
HOL-AFP: theory RBTMapImpl
HOL-AFP: theory Algebraic_Numbers
HOL-AFP: theory Real_Algebraic_Numbers
HOL-AFP: theory SetByMap
HOL-AFP: theory RBTSetImpl
HOL-AFP: theory Matrix_Impl
HOL-AFP: theory RBT_Map_Set_Extension
HOL-AFP: theory Transitive_Closure_RBT_Impl
HOL-AFP: theory Real_Roots
HOL-AFP: theory Show_Real_Alg
HOL-AFP: theory Show_Real_Precise
HOL-AFP: theory Complex_Algebraic_Numbers
Timing HOL-AFP (12 threads, 231.218s elapsed time, 2018.896s cpu time,
437.292s GC time, factor 8.73)
HOL-AFP FAILED
Email Gateway (Aug 22 2022 at 12:48):From: "C. Diekmann" <diekmann@in.tum.de>
2016-02-03 21:54 GMT+01:00 Makarius <makarius@sketis.net>:
On Wed, 3 Feb 2016, C. Diekmann wrote:
I'm not getting the "bulky 64bit version" warning when i start jEdit or
build, so I guess that I'm using the 32bit library.Is Isabelle2016 still issuing a warning on startup if the 64bit libraries
are used?Not any longer. This warning usually showed up in unexpected situations,
and did not show up when the standard Isabelle application wrapper was used.There were various changes in the auto-configuration of 32bit vs. 64bit
platforms, both for the ML system and the JVM. You now get this information
in the title of the build dialog on the first startup, but it is possible to
overlook it. (And sometimes people think that 64bit is always better than
32bit.)
Is there a way to check my setup after the first startup?
I was thinking of an additional warning dialog for a situation where the
option ML_system_64 is not set (i.e. the default of Isabelle), but the
result forced to x86_64-linux due to lack of 32bit g++ libraries (i.e. the
default of most Linux installations). I did not do it, because it may cause
puzzlement to new users or casual users, e.g. of introductory Isabelle
tutorials. The difference is only relevant to really big applications.Isabelle power users, especially on Linux, need to do some more fine-tuning
to get various side-conditions right. The details are listed here:
http://isabelle.in.tum.de/website-Isabelle2016-RC3/installation.html
Where can I find the documentation how I can set the ML settings such
that I can build Collections again?
For more than 3 years big Isabelle applications are usually run in constant space of approx. 3.5 GB, i.e. the maximum on 32bit.
If the build of a session image fails with an out of memory error, is
it possible to do the build again with only one core/process to limit
the memory usage to 3.5GB?
Cheers,
Cornelius
Email Gateway (Aug 22 2022 at 12:48):From: Makarius <makarius@sketis.net>
On Thu, 4 Feb 2016, C. Diekmann wrote:
Is there a way to check my setup after the first startup?
E.g. like this:
ML "open ML_System"
Where can I find the documentation how I can set the ML settings such
that I can build Collections again?
http://isabelle.in.tum.de/installation.html / Linux / Requirements:
32-bit C/C++ standard libraries on 64-bit Linux (optional, for improved performance of Poly/ML)
The details depend on the Linux distribution. On Ubuntu it is probably
just the "g++-multilib" package.
If the build of a session image fails with an out of memory error, is it
possible to do the build again with only one core/process to limit the
memory usage to 3.5GB?
You need to provide the 32-bit C/C++ standard libraries first, and then
restart the whole application. This allows to use the 32-bit version of
Poly/ML, which is separate from the 64-bit version.
Afterwards you can switch back to 64-bit via Plugin Options / Isabelle /
General / ML System 64, although that is practically irrelevant on only
8GB.
Makarius
Email Gateway (Aug 22 2022 at 12:48):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
I think Cornelius was asking for a way to limit parallelism while still using 64-bit Poly/ML in order to reduce the
maximum amount of memory required over the course of a build. If so, then yes:
isabelle build -o threads=1 ...
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 12:49):From: Makarius <makarius@sketis.net>
I have experimented with this a bit in the vicinity of Isabelle2016-RC.
The precise versions are as follows:
IsaFoR: 61d9e42449c2
Isabelle: dfb70abaa3f0
AFP: 522c6c87f51e
HOL-AFP still works with x86-linux, leading to a heap image of 577M. Here
are more details:
ML_PLATFORM="x86-linux"
ML_OPTIONS="-H 1500 --gcthreads 12"
isabelle build -b -o threads=12
Finished HOL-AFP (0:06:21 elapsed time, 0:47:49 cpu time, factor 7.53)
ML_PLATFORM="x86-linux"
ML_OPTIONS="-H 1500 --gcthreads 6"
isabelle build -b -o threads=6
Finished HOL-AFP (0:07:34 elapsed time, 0:37:10 cpu time, factor 4.91)
Trying "make all" of IsaFoR produces this result:
Building QTRS ...
Finished QTRS (0:02:02 elapsed time, 0:07:36 cpu time, factor 3.73)
Building Check-NT ...
Finished Check-NT (0:05:17 elapsed time, 0:22:26 cpu time, factor 4.24)
Building Processors ...
Processors FAILED
ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised
Proof-Checker CANCELLED
CeTA CANCELLED
Code CANCELLED
Makarius
Email Gateway (Aug 22 2022 at 12:50):From: Makarius <makarius@sketis.net>
Here are the results of further experiments. For Isabelle2016, I've
introduced certain "trim_context" operations that are mentioned in the
NEWS as follows:
For HOL-AFP this yields on x86-linux:
Finished HOL (0:02:58 elapsed time, 0:10:58 cpu time, factor 3.69) 218M
Finished HOL-Lib (0:01:24 elapsed time, 0:05:45 cpu time, factor 4.10) 281M
Finished HOL-AFP (0:07:37 elapsed time, 0:37:15 cpu time, factor 4.89) 577M
Disabling the mechanism here
https://bitbucket.org/isabelle_project/isabelle-release/src/f4baefee57768cf00b1a9e003770c7573b5d7378/src/Pure/thm.ML?at=default&fileviewer=file-view-default#thm.ML-410
yields the following:
Finished HOL (0:03:06 elapsed time, 0:11:21 cpu time, factor 3.66) 245M
Finished HOL-Lib (0:01:26 elapsed time, 0:05:54 cpu time, factor 4.11) 315M
Finished HOL-AFP (0:08:30 elapsed time, 0:39:52 cpu time, factor 4.69) 643M
Interestingly, the main HOL image has the same size of 218M in
Isabelle2015. So the extra space provided by the system has been exactly
consumed by the application -- this is a perfectly normal situation in
Isabelle development.
I guess that on average bigger applications did not grow that much. For
HOL-AFP, though, there seems to be a substantial increase in imports
compared to Isabelle2015, but I did not check this systematically.
Makarius
Email Gateway (Aug 22 2022 at 12:51):From: "C. Diekmann" <diekmann@in.tum.de>
I'm happy to tell that Collections builds again with RC4 on my 8GB RAM
laptop. Is this just a coincidence or did you fine-tune something?
Best,
Cornelius
Email Gateway (Aug 22 2022 at 12:51):From: Makarius <makarius@sketis.net>
I did not change anything.
It was working all the time in all my tests during this discussion.
Makarius
Last updated: Apr 26 2024 at 16:20 UTC