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

[Lars Hupel]

> But ocamlfind semms not to provide a subcommand to invoke the
> interactive OCaml toplevel.  What am I missing?

The other way round. "ocamlfind" hooks into the toplevel.

$ isabelle ocaml_opam config exec ocaml
        OCaml version 4.05.0

# #use "topfind";;
- : unit = ()
Findlib has been successfully loaded. Additional directives:
  #require "package";;      to load a package
  #list;;                   to list the available packages
  #camlp4o;;                to load camlp4 (standard syntax)
  #camlp4r;;                to load camlp4 (revised syntax)
  #predicates "p,q,...";;   to set these predicates
  Topfind.reset();;         to force that packages will be reloaded
  #thread;;                 to enable threads

- : unit = ()
# #require "zarith";;
/home/lars/.isabelle/opam/4.05.0/lib/zarith: added to search path
/home/lars/.isabelle/opam/4.05.0/lib/zarith/zarith.cma: loaded
# Z.one;;
- : Z.t = <abstr>

Cheers
Lars