Stream: Coq devs & plugin devs

Topic: ✔ .mlg files in vscode


view this post on Zulip Arpan Agrawal (Oct 10 2022 at 16:00):

Is there any editor support for mlg files in vscode? When I try to treat mlg files as just ordinary ocaml files in vscode (with the ocaml platform extension and ocaml-lsp-server installed), I get a "Unbound constructor DECLARE" error on the first line itself.

For context, I'm going through the plugin tutorial in the coq repo at https://github.com/coq/coq/tree/v8.16/doc/plugin_tutorial
Using coq 8.16.0 installed via opam

view this post on Zulip Gaëtan Gilbert (Oct 10 2022 at 16:03):

do you get syntax colors? I don't think any editor supports mlg beyond that, and even that is by just pretending it's ocaml and ignoring the errors

view this post on Zulip Karl Palmskog (Oct 10 2022 at 16:04):

maybe .mlg highlighting and support could be added VsCoq? VsCoq is not really part of Coq proper, though. Could be reported as a feature request: https://github.com/coq-community/vscoq/issues

view this post on Zulip Arpan Agrawal (Oct 10 2022 at 16:13):

Yes, there is syntax highlighting

view this post on Zulip Karl Palmskog (Oct 10 2022 at 16:14):

you mean, it uses OCaml syntax highlighting? But probably no mlg specific keywords are highlighted?

view this post on Zulip Arpan Agrawal (Oct 10 2022 at 16:15):

Yes, and it runs into the mentioned error on the first line

view this post on Zulip Gaëtan Gilbert (Oct 10 2022 at 16:17):

in emacs it looks like this
tac2.png

view this post on Zulip Arpan Agrawal (Oct 10 2022 at 16:30):

Does navigation from within the file still work? Can you jump to Prim from here?

view this post on Zulip Gaëtan Gilbert (Oct 10 2022 at 16:33):

no

view this post on Zulip Arpan Agrawal (Oct 10 2022 at 16:34):

Okay, thanks! Seems like emacs is better at handling mlg files, but not by much

view this post on Zulip Gaëtan Gilbert (Oct 10 2022 at 16:35):

if you have syntax highlighting it sounds equivalent not better

view this post on Zulip Arpan Agrawal (Oct 10 2022 at 16:38):

Vscode has syntax highlighting but also shows errors, which emacs seems to hide

view this post on Zulip Gaëtan Gilbert (Oct 10 2022 at 16:41):

emacs shows a couple errors at the top of the file
I guess merlin gives up after that
err.png

view this post on Zulip Pierre-Marie Pédrot (Oct 10 2022 at 16:44):

A good practice is to have the smallest possible mlg files, and one reason for that is the lack of editor support.

view this post on Zulip Pierre-Marie Pédrot (Oct 10 2022 at 16:45):

I don't think it makes much sense to implement such a support in any mainstream editor, to be honest.

view this post on Zulip Notification Bot (Oct 10 2022 at 18:12):

Arpan Agrawal has marked this topic as resolved.

view this post on Zulip Théo Zimmermann (Oct 11 2022 at 06:58):

I tend to do without the highlighting. The thing I miss most is the jump to definition feature.

view this post on Zulip Ali Caglayan (Oct 11 2022 at 09:03):

FTR merlin/ocaml-lisp doesn't even support ocamllex files which has been a wish for a wile I believe.


Last updated: Oct 13 2024 at 01:02 UTC