Vincent Siles (Sep 11 2020 at 13:00): Vincent Siles (Sep 11 2020 at 13:00):Hi ! I'd like to toy around with Drop. and the underlying ocaml runtime, but the doc says:
come back to the Coq toplevel with the command Coqloop.loop();;.
When I try that, the runtime is complaining:
# Coqloop.loop;;
- : opts:Coqargs.t -> state:Vernac.State.t -> unit = <fun>
# Coqloop.loop();;
Error: The function applied to this argument has type
opts:Coqargs.t -> state:Vernac.State.t -> unit
This argument cannot be applied without label
What arguments should I pass to get back to the Coq toplevel ?
Michael Soegtrop (Sep 11 2020 at 13:20):Please check the 8.11 reference manual:
(https://coq.github.io/doc/v8.11/refman/proof-engine/vernacular-commands.html#coq:cmd.drop)
I always used go();; and this worked for me.
Where does the Coqloop.loop();;advice come from?
Vincent Siles (Sep 11 2020 at 13:46):From https://coq.inria.fr/refman/practical-tools/coq-commands.html
Vincent Siles (Sep 11 2020 at 13:49):I'm getting Unbound Value with go();; but I think I need the source and include some things to make it work. I'll read the v8.11 doc for that. Thanks !
Vincent Siles (Sep 11 2020 at 14:07):@Michael Soegtrop did you compile Coq from source or are you using opam ? I'm trying to do that from a Coq installed via opam.
Emilio Jesús Gallego Arias (Sep 11 2020 at 14:19):@Vincent Siles right invocation for 8.12 installed with OPAM is:
$ coqtop.byte
> Drop.
# #directory "$coq_source/dev";;
# #use "base_include";;
# ...
# go () (* to return *)
As far as I can tell you don't need to compile it from sources, but you must have the corresponding sources available. The version of Coq in opam and of the sources must match. Then go into the dev folder in the sources, start coqtop.byte, Drop to OCaml and do #use"include";;. As far as I know this loads the pretty printers, but OCaml loads these as sources, not as binaries. But the pretty printers must obviously match the data structures in your coq binary.
I should say that I am not an OCaml expert - what I wrote above are my conclusions from observations what works and what not.
I just tested this with opam installed Coq 8.11.2 and a clean 8.11.2 source tree. Setting trace points and the like with proper pretty printing does work.
Emilio Jesús Gallego Arias (Sep 11 2020 at 14:20):you will need a copy of the coq sources matching your opam version, as the dev files are not installed
Vincent Siles (Sep 11 2020 at 14:22):Great, thank you both. I was missing the fact that I needed to be in the dev/ sub directory
Emilio Jesús Gallego Arias (Sep 11 2020 at 14:23):You could open a ticket so these files are installed and things work out of the box for OPAM
Michael Soegtrop (Sep 11 2020 at 14:23):Great, thank you both. I was missing the fact that I needed to be in the dev/ sub directory
Or add it to the search path with #directory "$coq_source/dev";; as Emilio wrote.
Michael Soegtrop (Sep 11 2020 at 14:26):Btw. afaik - Emilio please correct me - the difference between base_include and include is that the latter loads fancier printers, e.g. using user defined notations and the like.
Michael Soegtrop (Sep 11 2020 at 14:27):And please also file an issue for the manual - I think go();; is the recommended way - anyway the manual should be consistent in this.
Vincent Siles (Sep 11 2020 at 14:29):I would have to test with 8.12 first, see if things changed. I'm on 8.11 at the moment.
Last updated: Oct 01 2023 at 19:01 UTC