The Coq mailing list

["Paul Sacawa" <psacawa AT math.toronto.edu>]

Thanks for the help. I had some issues with installation that caused
#use "include"
to not function correctly. I thought I was expected to run
#cd "checker";;
first. Thanks again.

> 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ł
>>
>