[isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20190122/90f912e1/attachment.asc>