Gergely Buday (Sep 03 2026 at 11:48): Gergely Buday (Sep 03 2026 at 11:48):Building HOL by
isabelle build -vfb HOL 2>&1 | tee holbuild.log
results in
HOL: command "class" running for 29.320s (line 489 of theory "HOL.Euclidean_Rings")
/tmp/isabelle-user/bash_script13427155852201317942: line 1: 38234 Killed /home/user/Isabelle2025-2/contrib/polyml-5.9.2-2/x86_64_32-linux/poly -q --minheap 500 --gcthreads 4 --exportstats --eval \(PolyML.SaveState.loadHierarchy\ \[\"/home/user/.isabelle/Isabelle2025-2/heaps/polyml-5.9.2_x86_64_32-linux/Pure\"\]\;\ PolyML.print_depth\ 0\) --eval Options.load_default\ \(\) --eval Resources.init_session_env\ \(\) --eval Command_Line.tool\ \(fn\ \(\)\ \=\>\ \(Isabelle_Process.init_build\ \(\)\;\ ML_Heap.share_common_data\ \(\)\;\ ML_Heap.save_child\ \"/home/user/.isabelle/Isabelle2025-2/heaps/polyml-5.9.2_x86_64_32-linux/HOL\"\)\)\;
HOL FAILED (see also "isabelle build_log -H Error HOL")
What could be the problem?
Mathias Fleury (Sep 03 2026 at 16:43):Looks like a memory problem
Gergely Buday (Sep 07 2026 at 07:59):I got this on the command line, but I also get this when Isabelle/jEdit starts the build. I wonder about this as this worked on previous occasions, especially on the same laptop and with the same Isabelle version.
What setting could cure this?
Ant S. (Sep 07 2026 at 08:03):If you're on a *NIX system perhaps increasing your swap space might help?
Gergely Buday (Sep 07 2026 at 08:11):Thanks, I try it now
Ant S. (Sep 08 2026 at 09:03):Gergely Buday said:
Thanks, I try it now
Did it work?
Gergely Buday (Sep 08 2026 at 10:17):Yes, it did, although it took hours.
Last updated: Sep 15 2026 at 09:19 UTC