Stream: Coq users

Topic: Coming back from `Drop.` on Coq 8.11.0


view this post on Zulip 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 ?

view this post on Zulip 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?

view this post on Zulip Vincent Siles (Sep 11 2020 at 13:46):

From https://coq.inria.fr/refman/practical-tools/coq-commands.html

view this post on Zulip 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 !

view this post on Zulip 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.

view this post on Zulip 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 *)

view this post on Zulip Michael Soegtrop (Sep 11 2020 at 14:19):

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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 29 2023 at 06:02 UTC