Hi all, I plan to go some steps to use zarith for integer arithmetic for code generated in OCaml, and at the moment I am surrounded by tapestry.
As of, 331ef175a112, I issue the following steps:
$ isabelle ocaml_setup
--> fine
$ isabelle ocaml_opam install zarith
--> fine
$ echo 'let foo = 42;;' | isabelle env bash -c '"${ISABELLE_OCAML}"'
--> fine
Then I have no clue how to include the installed zarith properly.
https://opam.ocaml.org/doc/FAQ.html mentions subcommands »exec« and
»env« for opam, which the installed version available through »isabelle
ocaml_opam« does not provide.
A manual plumbing attempt fails either
$ echo 'let foo = Z.one;;' | isabelle env bash -c '"${ISABELLE_OCAML}"
"${ISABELLE_OPAM_ROOT}/4.05.0/lib/zarith/zarith.cma"'
--> »Error: Unbound module Z«
Has anybody advice how to go from here?
Thanks a lot,
Florian
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
