Hi all, I'm just trying to setup vscoq to work on a Coq plugin. While trying to follow this tutorial (https://github.com/tlringer/plugin-tutorial), I get the error "Unbound module Evd" in my mli files.
For some more context:
I have coq installed through opam (I also tried building from sources).
Using vscode via WSL2 on Windows.
Can someone please help me with this? Thanks!
it looks like the repo will only work with Coq 8.14. Did you install version 8.14.0 or 8.14.1 of Coq via opam? The
plugin-tutorial repo is incompatible with any other Coq version.
Yes, just to be sure I created a new switch and installed coq 8.14.1 in it. Still having the same issue.
I still think some other Coq version than 8.14.1 is getting pulled in. I recommend doing stuff like
eval $(opam env).
the plugin parts compile for me on 8.14.1, albeit with
CAMLFLAGS += -w -39 in
Still having this issue, even after double checking the Coq version. Now I am thinking this might be an editor issue, since the plugin functionality works, but vscode throws the above mentioned error in mli files. I am running vscode from the folder that has the _CoqProject file
Last updated: Dec 06 2023 at 14:01 UTC