search

NixOS / nixpkgs

Nix Packages collection & NixOS
MIT License
18.08k stars 14.13k forks source link

Can't build HOL in Isabelle #154249

Closed sledgehammervampire closed 2 years ago

sledgehammervampire commented 2 years ago

Describe the bug

When I open Isabelle for the first time, I can't proceed because Isabelle needs to build HOL.

Here is the error I get from the "Isabelle build" window:

Build started for Isabelle/HOL ...
Building HOL ...
HOL: theory Tools.Code_Generator
HOL: theory HOL.HOL
HOL: theory HOL.Ctr_Sugar
HOL: theory HOL.Orderings
HOL: theory HOL.Argo
HOL: theory HOL.Groups
HOL: theory HOL.SAT
HOL: theory HOL.Lattices
HOL: theory HOL.Boolean_Algebras
HOL: theory HOL.Set
HOL: theory HOL.Fun
HOL: theory HOL.Typedef
HOL: theory HOL.Rings
HOL: theory HOL.Complete_Lattices
HOL: theory HOL.Inductive
HOL: theory HOL.Product_Type
HOL: theory HOL.Sum_Type
HOL: theory HOL.Complete_Partial_Order
HOL: theory HOL.Nat
HOL: theory HOL.Fields
HOL: theory HOL.Meson
HOL: theory HOL.ATP
HOL: theory HOL.Metis
HOL: theory HOL.Finite_Set
HOL: theory HOL.Relation
HOL: theory HOL.Transitive_Closure
HOL: theory HOL.Wellfounded
HOL: theory HOL.Fun_Def_Base
HOL: theory HOL.Hilbert_Choice
HOL: theory HOL.Wfrec
HOL: theory HOL.Order_Relation
HOL: theory HOL.BNF_Wellorder_Relation
HOL: theory HOL.Zorn
HOL: theory HOL.BNF_Wellorder_Embedding
HOL: theory HOL.BNF_Wellorder_Constructions
HOL: theory HOL.BNF_Cardinal_Order_Relation
HOL: theory HOL.BNF_Cardinal_Arithmetic
HOL: theory HOL.BNF_Def
HOL: theory HOL.BNF_Composition
HOL: theory HOL.Basic_BNFs
HOL: theory HOL.BNF_Fixpoint_Base
HOL: theory HOL.BNF_Least_Fixpoint
HOL: theory HOL.Basic_BNF_LFPs
HOL: theory HOL.Transfer
HOL: theory HOL.Num
HOL: theory HOL.Power
HOL: theory HOL.Groups_Big
HOL: theory HOL.Equiv_Relations
HOL: theory HOL.Lifting
HOL: theory HOL.Lifting_Set
HOL: theory HOL.Option
HOL: theory HOL.Quotient
HOL: theory HOL.Extraction
HOL: theory HOL.Lattices_Big
HOL: theory HOL.Partial_Function
HOL: theory HOL.Fun_Def
HOL: theory HOL.Int
HOL: theory HOL.Euclidean_Division
HOL: theory HOL.Parity
HOL: theory HOL.Divides
HOL: theory HOL.Set_Interval
HOL: theory HOL.Numeral_Simprocs
HOL: theory HOL.Semiring_Normalization
HOL: theory HOL.SMT
HOL: theory HOL.Groebner_Basis
HOL: theory HOL.Conditionally_Complete_Lattices
HOL: theory HOL.Filter
HOL: theory HOL.Presburger
HOL: theory HOL.Sledgehammer
HOL: theory HOL.List
HOL: theory HOL.Groups_List
HOL: theory HOL.Map
HOL: theory HOL.Bit_Operations
HOL: theory HOL.Factorial
HOL: theory HOL.Enum
HOL: theory HOL.Binomial
HOL: theory HOL.Code_Numeral
HOL: theory HOL.GCD
HOL: theory HOL.String
HOL: theory HOL.Random
HOL: theory HOL.BNF_Greatest_Fixpoint
HOL: theory HOL.Predicate
HOL: theory HOL.Typerep
HOL: theory HOL.Lazy_Sequence
HOL: theory HOL.Limited_Sequence
HOL: theory HOL.Code_Evaluation
HOL: theory HOL.Quickcheck_Random
HOL: theory HOL.Quickcheck_Exhaustive
HOL: theory HOL.Quickcheck_Narrowing
HOL: theory HOL.Random_Pred
HOL: theory HOL.Random_Sequence
HOL: theory HOL.Record
HOL: theory HOL.Predicate_Compile
HOL: theory HOL.Nitpick
HOL: theory HOL.Mirabelle
HOL: theory HOL.Nunchaku
HOL: theory Main
HOL: theory HOL.Archimedean_Field
HOL: theory HOL.Hull
HOL: theory HOL.Modules
HOL: theory HOL.Topological_Spaces
HOL: theory HOL.Vector_Spaces
HOL: theory HOL.Rat
/tmp/isabelle-rdp/bash_script11507550249421458447: line 1: 1830458 Killed                  "$ML_HOME/poly" -q --minheap 1000 --gcthreads 0 --exportstats --eval \(PolyML.SaveState.loadHierarchy\ \[\"/home/rdp/.isabelle/Isabelle2021-1/heaps/polyml-5.9_x86_64-linux/Pure\"\]\;\ PolyML.print_depth\ 0\)\ handle\ exn\ \=\>\ \(TextIO.output\ \(TextIO.stdErr,\ General.exnMessage\ exn\ \^\ \":\ Pure\\n\"\)\;\ OS.Process.exit\ OS.Process.failure\) --eval Options.load_default\ \(\) --eval Command_Line.tool\ \(fn\ \(\)\ \=\>\ \(Isabelle_Process.init_build\ \(\)\;\ ML_Heap.share_common_data\ \(\)\;\ ML_Heap.save_child\ \"/home/rdp/.isabelle/Isabelle2021-1/heaps/polyml-5.9_x86_64-linux/HOL\"\)\)\;
HOL FAILED
(see also /home/rdp/.isabelle/Isabelle2021-1/heaps/polyml-5.9_x86_64-linux/log/HOL)
### Loading </nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so> failed: /nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
### Loading </nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so> failed: /nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
### Loading </nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so> failed: /nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
### Loading </nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so> failed: /nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
### Loading </nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so> failed: /nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
### Loading </nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so> failed: /nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
### Loading </nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so> failed: /nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
### Loading </nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so> failed: /nix/store/ljvsn7y9d0790hpqf42a70q250ypjs42-polyml-5.9/bin/libsha1.so: cannot open shared object file: No such file or directory
### Using slow ML implementation of SHA1.digest
Unfinished session(s): HOL
Return code: 137 (KILL SIGNAL)

Session build failed -- prover process remains inactive!

Steps To Reproduce

Steps to reproduce the behavior:

  1. Install Isabelle.
  2. Open Isabelle.

Expected behavior

Isabelle builds HOL.

Notify maintainers

@jwiegley @jvanbruegge @gebner

sledgehammervampire commented 2 years ago

It looks like I OOM'd.

jvanbruegge commented 2 years ago

I've opened #154272 to prevent others from OOMing for the HOL session