Stream: Coq devs & plugin devs

Topic: merlin for gramlib


view this post on Zulip Hugo Herbelin (Oct 14 2020 at 18:16):

To get merlin working with the packed gramlib, I need to add an open Gramlib at the top of gramlib files, so that it finds e.g. the module Gramlib.Gramext. Is it expected? Should I make a PR with the added open Gramlib?

view this post on Zulip Gaëtan Gilbert (Oct 14 2020 at 18:20):

dune or non dune?

view this post on Zulip Hugo Herbelin (Oct 14 2020 at 18:20):

Not having used dune (using emacs gramlib/grammar.ml).

view this post on Zulip Hugo Herbelin (Oct 14 2020 at 18:37):

OK, apparently, make works without open Gramlib because there is an explicit -open Gramlib in target COND_GRAMFLAGS of Makefile.build. Is there a way to tell merlin to use the option -open Gramlib too?

view this post on Zulip Hugo Herbelin (Oct 14 2020 at 18:40):

OK, adding - open Gramlib in the FLG header of .merlin.in fixes merlin for gramlib files. Is that the correct fix? Do I make a PR?

view this post on Zulip Gaëtan Gilbert (Oct 14 2020 at 18:45):

probably should be in a new gramlib/.merlin.in instead of the main one (using merlin REC)

view this post on Zulip Hugo Herbelin (Oct 14 2020 at 18:52):

I tried:

FLG -open gramlib

REC

in gramlib/.merlin (or gramlib/.merlin.in) but it did work. Do I miss something?

view this post on Zulip Hugo Herbelin (Oct 14 2020 at 19:17):

With the above gramlib/.merlin, merlin fails on the first character of grammar.ml and says: Wrong file naming: /home/coq/gramlib/.pack/gramlib.cmi contains the compiled interface for Gramlib when gramlib was expected

view this post on Zulip Gaëtan Gilbert (Oct 14 2020 at 19:18):

-open Gramlib then

view this post on Zulip Hugo Herbelin (Oct 14 2020 at 19:19):

With

-open gramlib

REC

in gramlib/.merlin, it fails to find open Gramext in grammar.ml.

view this post on Zulip Hugo Herbelin (Oct 14 2020 at 19:20):

Does it work for you?

view this post on Zulip Gaëtan Gilbert (Oct 14 2020 at 19:20):

you need to capitalize Gramlib

view this post on Zulip Gaëtan Gilbert (Oct 14 2020 at 19:20):

it's a module not a directory

view this post on Zulip Gaëtan Gilbert (Oct 14 2020 at 19:21):

I'm on dune, the autogenerated dune file is

EXCLUDE_QUERY_DIR
B /home/gaetan/.opam/4.09.1/lib/ocaml
B /home/gaetan/.opam/4.09.1/lib/ocaml/threads
B ../_build/default/clib/.clib.objs/byte
B ../_build/default/config/.config.objs/byte
B ../_build/default/gramlib/.gramlib.objs/byte
B ../_build/default/lib/.lib.objs/byte
S /home/gaetan/.opam/4.09.1/lib/ocaml
S /home/gaetan/.opam/4.09.1/lib/ocaml/threads
S ../clib
S ../config
S .
S ../lib
FLG -open Gramlib -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -keep-locs -rectypes -w -9-27+40+60

Last updated: Oct 21 2021 at 20:02 UTC