coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Issues with Ocaml Toplevel in Coq [coq-club][coqdev]

From: "Paul Sacawa" <psacawa AT math.toronto.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Issues with Ocaml Toplevel in Coq [coq-club][coqdev]
Date: Thu, 6 Jul 2017 18:36:46 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=psacawa AT math.toronto.edu; spf=Pass smtp.mailfrom=psacawa AT math.toronto.edu; spf=None smtp.helo=postmaster AT mail.math.toronto.edu
Importance: Normal
Ironport-phdr: 9a23:i23MyhwWFV2rdhnXCy+O+j09IxM/srCxBDY+r6Qd1O4WIJqq85mqBkHD//Il1AaPBtSEraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pnRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRH1iCkJKTA2/27LhcJ/lqxUowmspwB8zoLIfI2ZKOdwfrjbcNgHRWRBRMFRVylZD4+ydYUAFfcBPeJFpIfgvVQBsQGxBAe2C+/h1zRFgWf23bYg3Os9Cw7H0hYvEskLsHvOsNX1NL0eUfyyzKnSyjXDae9W2TDn5IfWbx8hvOiBULRtesTS0UkiDx7JgkuTpID/Ij+ZyvgBv3Ka4udjT+6iim0qpxlsrjWhxcogkInEip8PxlzZ6Cl0w5w5KNykREN9fNWqCoFftzuAOItzWs4iQ39nuCI9yrAevJ60ZikKyJA9yx7acfOHb4iI7gj/VOaWOzd4g3RleK64hxqo70ev1/D8WtG10FZMsCVFjsHBum0T2xHQ8MSLV+dx8lu71TuO1A3f8OBJLEMsmareMZEhw7owlpQJsUTEGy/7gF32jLSMeUo44Oep5f7ob67jppCGK490ihvyMrgpmsylBuQ4NBQOX2+B9euiybLj4FX1QK9Wgf0ujqnZrJfaKNwHqa6+Gg9Zy5os6xKiDzi9y9kYhnkGLFddeB2dlYTpOlfOIOr5DfilmVisni1rlLj6OejqBYyIJXzemp/ge6x84ghS0lkd19dasthsA6wFaMn6UUbuvZaQWgciOge93O/PDdxh1sUCXniIBLOedq7erAnbtaoUP+CQadpN637GIP8/6qu2gA==

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