Isabelle 2018 from nixos-19.09 fails to build HOL when the first startup of $isabelle jedit.
The build log is as follows:
Build started for Isabelle/HOL ...
Building Pure ...
Pure: theory Pure
Pure: theory ML_Bootstrap
Pure: theory Pure.Sessions
Finished Pure (0:00:15 elapsed time, 0:00:14 cpu time, factor 0.96)
Building HOL ...
HOL: theory HOL.Code_Generator
HOL: theory HOL.HOL
HOL: theory HOL.Argo
HOL: theory HOL.Ctr_Sugar
HOL: theory HOL.Orderings
HOL: theory HOL.SAT
HOL: theory HOL.Groups
HOL: theory HOL.Lattices
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.BNF_Wellorder_Embedding
HOL: theory HOL.Zorn
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 FAILED
(see also /home/pan/.isabelle/Isabelle2018/heaps/polyml-5.7.1_x86_64-linux/log/HOL)
"division_segment_mod":
"\<And>b a.
\<lbrakk>b \<noteq> (0::'a); \<not> b dvd a\<rbrakk>
\<Longrightarrow> division_segment (a mod b) = division_segment b"
assumes
"div_bounded":
"\<And>b r q.
\<lbrakk>b \<noteq> (0::'a);
division_segment r = division_segment b;
euclidean_size r < euclidean_size b\<rbrakk>
\<Longrightarrow> (q * b + r) div b = q"
instantiation
nat :: normalization_semidom
normalize_nat == normalize :: nat \<Rightarrow> nat
unit_factor_nat == unit_factor :: nat \<Rightarrow> nat
divide_nat == divide :: nat \<Rightarrow> nat \<Rightarrow> nat
instantiation
nat :: unique_euclidean_semiring
division_segment_nat == division_segment :: nat \<Rightarrow> nat
euclidean_size_nat == euclidean_size :: nat \<Rightarrow> nat
modulo_nat == modulo :: nat \<Rightarrow> nat \<Rightarrow> nat
structure Cancel_Div_Mod_Nat: CANCEL_DIV_MOD
### Rule already declared as elimination (elim)
### \<lbrakk>?b dvd ?a; \<And>k. ?a = ?b * k \<Longrightarrow> ?P\<rbrakk>
### \<Longrightarrow> ?P
instantiation
int :: normalization_semidom
normalize_int == normalize :: int \<Rightarrow> int
unit_factor_int == unit_factor :: int \<Rightarrow> int
divide_int == divide :: int \<Rightarrow> int \<Rightarrow> int
instantiation
int :: idom_modulo
modulo_int == modulo :: int \<Rightarrow> int \<Rightarrow> int
instantiation
int :: unique_euclidean_ring
division_segment_int == division_segment :: int \<Rightarrow> int
euclidean_size_int == euclidean_size :: int \<Rightarrow> nat
### theory "HOL.Euclidean_Division"
### 21.065s elapsed time, 56.271s cpu time, 49.818s GC time
Loading theory "HOL.Parity" (required by "Main" via "HOL.Predicate_Compile" via "HOL.Random_Sequence" via "HOL.Random_Pred" via "HOL.Quickcheck_Random" via "HOL.Random" via "HOL.List" via "HOL.Sledgehammer" via "HOL.Presburger" via "HOL.Groebner_Basis" via "HOL.Semiring_Normalization" via "HOL.Numeral_Simprocs" via "HOL.Divides")
Unfinished session(s): HOL
Return code: 139
Session build failed -- prover process remains inactive!
Do you have any experience of running Isabelle in NixOS successfully?