Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021-1-RC1: Download for Linux (ARM64)


view this post on Zulip Email Gateway (Nov 01 2021 at 21:56):

From: Makarius <makarius@sketis.net>
There is now also a Download for Linux (ARM64).

I've had considerable problems building the HOL heap image on my Raspberry Pi
4 (4 cores, 8 GB). It worked much better with the MacMini M1 (8 cores, 16 GB)
and native Docker for ARM.
The result basically works, but I've seen it crash already (maybe severe
resource problems).

Further omissions in this release:

- cvc4
- nunchaku / smbc
- z3
- GHC stack
- OCaml opam

Everything else is already available for arm64-linux (and arm64-darwin).

Makarius

view this post on Zulip Email Gateway (Nov 04 2021 at 10:23):

From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
Hello,

I installed Isabelle2021-1-RC1 for arm64 in a Docker container on an M1 Mac.
It works fine, but there is an error each time I invoke sledgehammer.

More precisely, sledgehammer works (it calls provers and returns proofs) but at the end, I get the following error (which pops up in an error dialog):

Welcome to Isabelle/HOL (Isabelle2021-1-RC1)
message_output terminated
/tmp/isabelle-root/bash_script4312713774210683116: line 1: 1202 Segmentation fault "$ML_HOME/poly" -q --minheap 500 --gcthreads 0 --exportstats --eval \(PolyML.SaveState.loadHierarchy\ \[\"/root/Isabelle2021-1-RC1/heaps/polyml-5.9_arm64-linux/Pure\",\ \"/root/Isabelle2021-1-RC1/heaps/polyml-5.9_arm64-linux/HOL\"\]\;\ PolyML.print_depth\ 0\)\ handle\ exn\ \=\>\ \(TextIO.output\ \(TextIO.stdErr,\ General.exnMessage\ exn\ \^\ \":\ HOL\\n\"\)\;\ OS.Process.exit\ OS.Process.failure\) --eval Options.load_default\ \(\) --eval Isabelle_Process.init\ \(\)

standard_output terminated
standard_error terminated
process terminated
command_input terminated
process_manager terminated
Return code: 139 (SEGMENTATION VIOLATION)

I then have to quit Isabelle because nothing works any longer as expected.

Frédéric

Frédéric Boulanger
CentraleSupélec - Département Informatique Laboratoire Méthodes Formelles (LMF)
3 rue Joliot-Curie, 91192 Gif-sur-Yvette cedex Bât. 650 - 1 rue Raimond Castaing, 91190 Gif-sur-Yvette
+33 [0]1 69 85 14 84
Capture d’écran 2021-11-04 à 10.54.12.png


Last updated: Jul 15 2022 at 23:21 UTC