Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] export code checking OCaml: zarith not found

Email Gateway (Apr 06 2021 at 11:49):

From: Peter Lammich <lammich@in.tum.de>
Hi,

I'm trying to use the checking OCaml mode of export_code, but it fails
with

ocamlfind: Package `zarith' not found
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w pu
-package zarith -linkpkg ROOT.ml </dev/null

I have installed opam and ocamlfind, and added the path to ocamlfind
and an eval $(opam env) to my ~/.isabelle/Isabelle2021/etc/settings
file:

peter@peterXps:~$ cat ~/.isabelle/Isabelle2021/etc/settings
ISABELLE_OCAMLFIND=/usr/bin/ocamlfind
ISABELLE_GHC=/usr/bin/ghc

eval $(opam env)

running with isabelle env works as expected

peter@peterXps:~$ isabelle env ocamlfind query zarith
/home/peter/.opam/default/lib/zarith

but, even after restarting isabelle, export_code keeps complaining.
What am I missing? How to troubleshoot?

Email Gateway (Apr 06 2021 at 12:08):

From: Makarius <makarius@sketis.net>
In principle it is meant to work via "isabelle ocaml_setup", which takes care
of opam by itself.

But opam is not very robust and has implicit dependencies that need to be
satisfied separately. E.g. on Ubuntu 20.04 LTS, I have something like
libzarith-ocaml, libgmp-dev, m4 --- maybe more that I have forgotten.

Makarius

Email Gateway (Apr 06 2021 at 14:09):

From: Peter Lammich <lammich@in.tum.de>

In principle it is meant to work via "isabelle ocaml_setup", which
takes care
of opam by itself.

But opam is not very robust and has implicit dependencies that need
to be
satisfied separately. E.g. on Ubuntu 20.04 LTS, I have something like
libzarith-ocaml, libgmp-dev, m4

Last updated: Jan 04 2025 at 20:18 UTC