coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Plugin development in emacs with merlin

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Plugin development in emacs with merlin
Date: Sat, 21 Apr 2018 16:43:13 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f173.google.com
Ironport-phdr: 9a23:v/54WhGiPt8Vu2CMtWK/gp1GYnF86YWxBRYc798ds5kLTJ7zpsqwAkXT6L1XgUPTWs2DsrQY07GQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDSwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAvYaMuZYron9vFsOogW9BQKxGO7vzCVHhnnr0qYn1OkuCxrJ3AwhH9IVsHTbstb1OL0IXuCz1qbIyyjMY+lX2Tf89IjIfQssof6JXb1qcMrRzVMjGB/CjlWVsIHoOS6e2OoKs2ie9eVgVOSvhnY7pAF2uDivwNkjio3Nho4P1F/L6Dh5zJ4pKt2/Uk57Z8CrEJ9Uty2ALYd5XN4tQ3xutS0nybMGoYa2cDYWxJkj3RLSaPyKf5KV7h/iSeqdOyp0iXBrdb+5mh2861KvyvfmWcmxyFtKrjRKkt3Ltn0V0hzc8MmHSv9k8kah1zeDyxnf6u9ZLU02m6fXMZEhwrk3lpoctUTMADX6l1nxjK+Tbkkk++6o5Pr7Yrj+uJOQK4t5hhv9P6kugMCzHOU1PhUUU2SG++mx2qXv/UjjT7VLiv02nLPZsJffJckDvKG2GA9V0oc46xa/ETim084UkmMBLF1ffhKIkpLlO1DPIPDkAveymFuskDJxyPDHOr3tGInCLn/GkLv5Z7Zy91ZcyBYvzdBY/59bFrYBIOvqVkDtsNzYEwQ2Phevw+fnDdV9zpkRVXiOAq+fKqPSsEWH6vghI+mWN8cpv2P2LOFg7Przh1c4n0UcdO+nx8g5cne9S91sI0SCYXfvyv4HGGEG9l43Ruzrk12PUnhaYX+0U+Q95y00II2jBIbHAIuqherSj2+AApRKazUeWRi3GnDyetDcAqZeWGepOsZk1wc8e/2kQo4l2wupsVajmbViJ+vQvCYfsMC6jYQn16jojRg3sAdMIYGFyWjUFjN7m2oJQ3k926Ut+RUgmGfG6rBxhrljLfIW5/5NVV1kZ5vVzug/Gs+qHwyYIYzPR1GhTdGrRzo2S4Bpzg==

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/

[Coq-Club] Plugin development in emacs with merlin, Hans Jacob Fehrmann Rojas, 04/21/2018
- Re: [Coq-Club] Plugin development in emacs with merlin, Abhishek Anand, 04/21/2018
  - Re: [Coq-Club] Plugin development in emacs with merlin, Théo Zimmermann, 04/21/2018
    - Re: [Coq-Club] Plugin development in emacs with merlin, Hans Jacob Fehrmann Rojas, 04/21/2018