[Coq-Club] Plugin development in emacs with merlin

[Hans Jacob Fehrmann Rojas]

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 Anand]

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 <

Post by Hans Jacob Fehrmann Rojas
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.

[Théo Zimmermann]

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.

Post by Abhishek Anand
There's probably a better way to do this, but here's what I do for plugin
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
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 <

Post by Hans Jacob Fehrmann Rojas
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/

[Hans Jacob Fehrmann Rojas]

Thanks. This was the solution.

Hans.

Post by Théo Zimmermann
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 <

Post by Abhishek Anand
There's probably a better way to do this, but here's what I do for plugin
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
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 <

Post by Hans Jacob Fehrmann Rojas
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 Anand]

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 <

Post by Hans Jacob Fehrmann Rojas
Thanks. This was the solution.
Hans.

Post by Théo Zimmermann
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 <

Post by Abhishek Anand
There's probably a better way to do this, but here's what I do for
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
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 <

Post by Hans Jacob Fehrmann Rojas
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/

[Gaëtan Gilbert]

make install-merlin looks related

Gaëtan Gilbert

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
Thanks. This was the solution.
Hans.
On Sat, Apr 21, 2018 at 1:58 PM, Théo Zimmermann
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
There's probably a better way to do this, but here's what I
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
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
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/>

[Gaëtan Gilbert]

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

Gaëtan Gilbert

Post by Gaëtan Gilbert
make install-merlin looks related
Gaëtan Gilbert

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
    Thanks. This was the solution.
    Hans.
    On Sat, Apr 21, 2018 at 1:58 PM, Théo Zimmermann
        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
            There's probably a better way to do this, but here's what I
            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
            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
                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/>