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