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
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
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
Yes, there is syntax highlighting
you mean, it uses OCaml syntax highlighting? But probably no mlg
specific keywords are highlighted?
Yes, and it runs into the mentioned error on the first line
in emacs it looks like this
tac2.png
Does navigation from within the file still work? Can you jump to Prim from here?
no
Okay, thanks! Seems like emacs is better at handling mlg files, but not by much
if you have syntax highlighting it sounds equivalent not better
Vscode has syntax highlighting but also shows errors, which emacs seems to hide
emacs shows a couple errors at the top of the file
I guess merlin gives up after that
err.png
A good practice is to have the smallest possible mlg files, and one reason for that is the lack of editor support.
I don't think it makes much sense to implement such a support in any mainstream editor, to be honest.
Arpan Agrawal has marked this topic as resolved.
I tend to do without the highlighting. The thing I miss most is the jump to definition feature.
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