The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

I don’t know much about the OCaml top-level, but it does work for me.

I’m working directly from the Coq sources; I’m not sure about the binary releases. Here’s what I did:

make world coqbyte pluginsbyte
./bin/coqtop.byte

This brings up the Coq toplevel. Now run Drop. to get to an OCaml top-level.

You first have to run #use "include";; (there’s also #use "base_include";;, documented in the text file dev/doc/debugging.txt, which does not load the pretty printers). The reference manual mentions this, but isn’t clear that this is actually required to use go(). We could probably also reference some documentation upon running Drop.

This command prints a bunch of functions that are now defined. These include go (to exit) and a bunch of conveniences like parse_constr and parse_tac to easily construct terms, for example:

# let nat = parse_constr "nat";;
val nat : API.Constrexpr.constr_expr =
  {CAst.v = API.Constrexpr.CRef (API.Prelude.Ident (Some (0,3), nat), None);
   loc = Some (0,3)}

# let repeat_subst = parse_tac "repeat subst";;
val repeat_subst : Tacexpr.raw_tactic_expr =
  Tacexpr.TacRepeat
   (Tacexpr.TacAlias (Some (7,12), (Coq.Init.Notations.subst_4C69D532, [])))

Hope that helps!

​

On Thu, Jul 6, 2017 at 11:36 PM, Paul Sacawa <psacawa AT math.toronto.edu> wrote:

Hello,
I'm an amateur in Ocaml and Coq trying to conduct some experiments to
extend the functionality of the former. To get a handle on the classes
used I've tried using Coq's "Drop" Vernac command (6.8.2 in reference
manual) to enter Ocaml shell, and experiment. Some issues:

1. "go();;" does not work to go back from ocaml toplevel to coq. How to
make it work?
2. I'm unable to access any coq objects through the shell, either
directly, or via #load_rec (*.cmo files and coqtop.byte disagree on module
interfaces). How can I most directly interface with the basic coq kernel
modules,  like Term?
3. Is there any documentation I should read to understand how to get a
grip on this?

Regards,
Paweł