Email Gateway (Apr 27 2021 at 09:26): Email Gateway (Apr 27 2021 at 09:26):From: Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
Hello,
When I try to do isabelle jedit -R Some_Session_with_code_generation
Isabelle fails to do the heap build and throws the following error:
Some_Session_with_code_generation FAILED
(see also
/Users/user/.isabelle/Isabelle2021/heaps/polyml-5.8.2_x86_64_32-darwin/log/Some_Session_with_code_generation)
*** Failed to load theory "Some_Session_with_code_generation.Examples"
(unresolved "Some_Session_with_code_generation.Theory_with_Code")
*** Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu
-package zarith -linkpkg ROOT.ml </dev/null
*** At command "export_code" (line 42 of
"~/.../thys/Some_Session_with_code_generation/Theory_with_Code.thy")
Some_Session_with_code_generation_requirements(Some_Session_with_code_generation)
CANCELLED
Unfinished session(s):
Some_Session_with_code_generation_requirements(Some_Session_with_code_generation)
Return code: 1 (ERROR)
Things that I have tried to not have the error:
isabelle ocaml_setup before isabelle jedit -R ...Changing manually ISABELLE_OCAMLFIND as suggested here:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2019-March/016793.html
Changing manually ISABELLE_OCAML_VERSION to the latest ocaml as the ocaml
people suggest an upgrade to the ocaml compiler (
https://github.com/ocaml/opam-repository/issues/18586)
As an average user, I'd appreciate any specific set of instructions to
remove the error (my computer specifications appear in the github link).
Best wishes,
Email Gateway (Apr 27 2021 at 10:57):From: Fabian Huch <huch@in.tum.de>
You might be missing some system packages, see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-April/msg00007.html
I had the same issue after a major system update (with the packages
installed), and it turned out that opam was broken -- removing the
~/.opam folder and re-running ocaml_setup solved that for me.
Fabian
Email Gateway (Apr 27 2021 at 22:42):From: Makarius <makarius@sketis.net>
Your system is macOS Big Sur on Apple Silicon (ARM64), and the problem is
ultimately to build OCaml (with zlib) on it, with or without opam.
Some years ago, I provided the "isabelle ocaml_setup" tool to simplify that
process, but now I am unsure if that was actually a good idea: opam has too
many implicit dependencies on the operating system and easily breaks.
I've briefly tried it on my Apple M1 test machine and failed on missing
libgmp: so maybe it actually works after more tinkering. When doing the
Isabelle2021 release some months ago, native OCaml was still not visible on
the horizon.
If you do manage to build OCaml on arm64-darwin, I will take the result into
account of the next Isabelle release --- presumably Nov/Dec-2021.
Makarius
Email Gateway (Apr 27 2021 at 22:45):From: Makarius <makarius@sketis.net>
With "zarith", not "zlib".
Makarius
Email Gateway (Apr 28 2021 at 08:02):From: Florian Märkl <isabelle-users@florianmaerkl.de>
What works quite well on arm64 macOS is ocaml from MacPorts:
https://ports.macports.org/port/ocaml
https://ports.macports.org/port/ocaml-zarith
https://ports.macports.org/port/opam
I can recommend setting "buildfromsource always“ in /opt/local/etc/macports/macports.conf to force it to always build from source natively instead of trying to possibly fetch x86 binaries.
Their build scripts can also be used as a reference for building outside of MacPorts, for example:
https://github.com/macports/macports-ports/blob/master/lang/ocaml/Portfile
Though in this case it looks quite straightforward.
Florian
Last updated: Jul 15 2022 at 23:21 UTC