The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

I personally like isend-mode for allowing any subprocess to be associable with a buffer. You can then iteratively send your script fragments to the toplevel, and work out all changes in a buffer that you can then save! It's like SLIME, if you've ever heard or seen that.

On Wed, Jun 24, 2015 at 10:59 AM, Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

Hi coq-club,

During the Coq Coding Sprint, Thomas Sibut-Pinote asked for a way to
start an ocaml toplevel (from the Emacs buffer showing OCaml code of a
Coq plugin) that would already know about Coq library and internal
modules.

You probably already know that you can get an OCaml-able toplevel from
coqtop using the "Drop." command,

$ coqtop.byte
Welcome to Coq 8.4pl5 (November 2014)

Coq < Drop.
        OCaml version 4.02.2

    Camlp5 parsing version 6.13

# #use "include";;

The point of this mail is to let know this from Emacs (using caml-mode
or tuareg-mode):

- use whatever command your emacs-ocaml-mode uses to launch a toplevel
(Tuareg: C-x C-e)
- ask for "coqtop.byte" as a toplevel name
- run the command "Drop. Drop. ;;"
- then #use "include";; as usual

(Yes, you need two commands instead of just Drop., and you need the
two semicolons; this is the trick, found by Jacques-Henri Jourdan.)