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

2019-01-23 Thread 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 = 

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2019-01-22 Thread Florian Haftmann 
Hi Lars,

Am 22.01.19 um 22:34 schrieb Lars Hupel:
> It is admittedly a complicated incantation, but here you go:
> 
> $ cat test.ml
> let x = Z.one;;
> let _ = print_endline (Z.to_string x);;
> 
> $ isabelle ocaml_opam config exec ocamlfind -- ocamlopt -package zarith
> -linkpkg test.ml
> 
> $ ./a.out
> 1
> 
> You need "ocamlfind" to tell the OCaml compiler ("ocamlopt") where to
> look for packages.

thanks for that hint.

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

Cheers,
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

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

2019-01-22 Thread Lars Hupel 
It is admittedly a complicated incantation, but here you go:

$ cat test.ml
let x = Z.one;;
let _ = print_endline (Z.to_string x);;

$ isabelle ocaml_opam config exec ocamlfind -- ocamlopt -package zarith
-linkpkg test.ml

$ ./a.out
1

You need "ocamlfind" to tell the OCaml compiler ("ocamlopt") where to
look for packages.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2019-01-22 Thread Makarius 
On 22/01/2019 22:02, Florian Haftmann wrote:
> 
> 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.

That documentation is for Opam 2.0, but we are still on 1.2.2 because
that is the latest version I've found for Windows (based on MinGW); the
same 1.2.2 is part of Cygwin.

I can update Isabelle/Opam when there is a proper Windows version for
2.0 -- maybe it has already arrived in the meantime, somewhere in some
dark corner.


Apart from that, I've recently seen Coq experts worry about the
status-quo of Opam: it is not as well-developed as Stack for Haskell,
and Coq already critically depends on it.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev