The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Nevermind I don't know how to get it to run from opam

Gaëtan Gilbert

On 20/07/2018 13:03, Gaëtan Gilbert wrote:
> make install-merlin looks related
>
> Gaëtan Gilbert
>
> On 20/07/2018 13:01, Abhishek Anand wrote:
> > 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 <mailto: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
> >  
> > <mailto: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
> >         
> > <mailto: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
> >  
> > <mailto: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/
> >             <http://www.cs.cornell.edu/%7Eaa755/>
> >
> >
> > --
> > -- Abhishek
> > http://www.cs.cornell.edu/~aa755/ <http://www.cs.cornell.edu/%7Eaa755/>