coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Tej Chajed <tchajed AT mit.edu>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Issues with Ocaml Toplevel in Coq [coq-club][coqdev]
- Date: Fri, 7 Jul 2017 07:56:11 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-1.mit.edu
- Ironport-phdr: 9a23:+TDvrxe9rSiDYETStAhh/ZuolGMj4u6mDksu8pMizoh2WeGdxcu6ZR7h7PlgxGXEQZ/co6odzbGH7Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5Y75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM28m/XhMx+gqxYvRyvuQBwzpXOb42JLvdzZL/Rcc8YSGdHQ81fVzZBAoS5b4YXEeQOI+RYpJTjqlsOtxS+BxejC/7ywTJPmn/5wa063P4jEQ7YwQMtBNcOsHXIrNnvKqgdTP21wbDOwD7ebP1WwS/w5JXLfxw7pfyAR6x8fMrLxUUyCQ/JlkucpZDhMj+P1ekAs3KX4/d+We+skWIrtgN8riWpy8wxkIfGnJgVxUrB9ShhwIY6O9m4SEljbNG5FZtRtjiWN45sTcMjR2Foozg1xaEftZ6gYCcF0pInxxjBZPydaoSE/wjvVOOQITdknn5qZq+whwuq/UihzO3zSNW03U5XoidGiNXBsmoB2wLT58SdV/dx4F+t2TOV2ADS7uFEL1o0la3eK5M53r4/ipoTvl7BHiDohUr7l6qWdkQ4+uSy9evof6jmqoeGN4BokgH+LrgumsunDOskNQgORnGX9vi41L3+5kL0W65Kj/0zkqnBqp/WP8UbpqijAw9UyIkv8Ri/Dy31mOgfyHIANRdOfA+Nx9ziPEiLK/TlB9++hU6tmXFl3aaVEKfmB8DxI3qLu7fof7txoxpAwwo6z91Tz5dVFvcMLO+lCRy5j8DREhJsa1/8+O3gEtgojo4=
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!
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ł
- [Coq-Club] Issues with Ocaml Toplevel in Coq [coq-club][coqdev], Paul Sacawa, 07/07/2017
- Re: [Coq-Club] Issues with Ocaml Toplevel in Coq [coq-club][coqdev], Tej Chajed, 07/07/2017
- Re: [Coq-Club] Issues with Ocaml Toplevel in Coq [coq-club][coqdev], Paul Sacawa, 07/07/2017
- Re: [Coq-Club] Issues with Ocaml Toplevel in Coq [coq-club][coqdev], Tej Chajed, 07/07/2017
Archive powered by MHonArc 2.6.18.