Arpan Agrawal (Sep 06 2022 at 00:26): Arpan Agrawal (Sep 06 2022 at 00:26):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!
Karl Palmskog (Sep 06 2022 at 06:39):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? Theplugin-tutorial repo is incompatible with any other Coq version.
Arpan Agrawal (Sep 06 2022 at 07:30):Yes, just to be sure I created a new switch and installed coq 8.14.1 in it. Still having the same issue.
Karl Palmskog (Sep 06 2022 at 08:27):I still think some other Coq version than 8.14.1 is getting pulled in. I recommend doing stuff like eval $(opam env).
Karl Palmskog (Sep 06 2022 at 08:28):the plugin parts compile for me on 8.14.1, albeit with CAMLFLAGS += -w -39 in Makefile.coq.local.
Arpan Agrawal (Oct 10 2022 at 18:12):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: Oct 13 2024 at 01:02 UTC