Re: [isabelle] Isabelle2016-RC3 -- jEdit build fails when session loaded from different directory



On 02/03/2016 09:40 PM, Makarius wrote:

> 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.

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.