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



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


Le 1 nov. 2021 à 22:55, Makarius <makarius at sketis.net> a écrit :

On 01/11/2021 20:35, Makarius wrote:

The current release candidate is
https://isabelle.sketis.net/website-Isabelle2021-1-RC1

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





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