Stream: Coq devs & plugin devs

Topic: Unbound module Evd


view this post on Zulip 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. Can someone please help me with this? Thanks!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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: Feb 06 2023 at 19:03 UTC