The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

While installing Coq using opam, is there a way to ask that the .cmt files for Coq's OCaml sources be generated and installed at the appropriate place? 

Is there any significant downside to doing that by default?

On Sat, Apr 21, 2018 at 5:09 PM Hans Jacob Fehrmann Rojas <hans.jfehrmann AT gmail.com> wrote:

Thanks. This was the solution.

Hans.

On Sat, Apr 21, 2018 at 1:58 PM, Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

Note that with Coq master -debug is on by default and -annotate is now -bin-annot.

Also, there is a Merlin file in the Coq sources.

Le sam. 21 avr. 2018 à 18:44, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :

There's probably a better way to do this, but here's what I do for plugin work:

I manually build coq (the same version as that of the coq binaries) from sources, say in a directory X.

While building Coq, I pass the following options to ./configure: -debug -annotate

Then, in ~/.merlin, I add the following:

FLG -rectypes

B X/config

B X/lib

B X/intf

B X/kernel

B X/kernel/byterun

B X/library

B X/engine

B X/pretyping

B X/interp

B X/proofs

B X/tactics

B X/printing

B X/parsing

B X/toplevel

B X/tools

B X/tools/coqdoc

B X/dev

B X/stm

B X/plugins/ltac

B X/vernac

Then, in vscode, I am able to jump (to definition) around in Coq sources and see types of items that are in Coq sources.

On Sat, Apr 21, 2018 at 11:33 AM Hans Jacob Fehrmann Rojas <hans.jfehrmann AT gmail.com> wrote:

I am developing a plugin in emacs with merlin. Today I changed my pc and now I am not able to locate the function on the coq modules. The problem seems to be some cmt files missing. How can this be fixed?

Best,

Hans.

--

-- Abhishek

http://www.cs.cornell.edu/~aa755/

--

-- Abhishek

http://www.cs.cornell.edu/~aa755/