The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

During the Coq Coding sprint I had the pleasure of converting some Coq
plugin authors to the Merlin editor-assistant for OCaml:
  https://github.com/the-lambda-church/merlin/

Using merlin on Coq sources themselves is very easy, thanks to the
`.merlin` description file already included in the Coq sources (thanks
to Pierre Boutillier, with some help from Thomas Refis). This means
that when you are hacking the OCaml files inside the Coq sources,
Merlin can provide accurate type feedback, go to definition, find all
occurences, etc.

But if you develop your own plugin, using Coq's internal modules from
outside the Coq sources direction, you have to write a .merlin file of
your own to tell Merlin where to look for type information. The
following structure for a .merlin file seems correct:

FLG -rectypes
S $(coqc -where)/**
B $(coqc -where)/**

Note that you have to expand $(coqc -where) into the result of your
command by yourself. (This would be easier if Coq installed itself as
a findlib package, but this file works for the current Coq development
workflow.). For example, a typical .merlin plugin would look like the
following:

FLG -rectypes
S /home/gasche/.opam/4.02.2/lib/coq
B /home/gasche/.opam/4.02.2/lib/coq

(I contacted merlin devs upstream to ask whether the shell-expansion
could be done by Merlin itself:
  https://github.com/the-lambda-church/merlin/issues/411
but I think changes in Coq's install procedure may be a better
long-term way to not require hardcoding user-specific directories)


Happy OCaml hacking!