Stream: Coq devs & plugin devs

Topic: Porting plugins to dune


view this post on Zulip Janno (Jul 11 2020 at 13:00):

In an attempt to (eventually) work around https://github.com/coq/coq/issues/12067 I've been trying to use dune to build Unicoq. However, I get the following error and I don't know what to do about it:

Error: The following libraries are missing in the default context:
- coq.plugins.ltac
Hint: try: opam install coq

The problem is that I already did install coq via opam (and it works fine, too):

$ opam list
[...]
coq            8.11.2         Formal proof management system
[...]

What am I missing?

view this post on Zulip Janno (Jul 11 2020 at 13:34):

I think I solved this. I hadn't installed dune in my new opam switch so dune was actually the system-wide dune binary.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2020 at 15:06):

Yup you gotta be careful with system-wide ocaml stuff. unicoq + mtac2 do work fine with dune, except that you will have to manually Declare ML unicoq

view this post on Zulip Emilio Jesús Gallego Arias (Jul 11 2020 at 15:06):

And maybe update some dune files to newer (lang coq 0.2)


Last updated: Oct 21 2021 at 21:03 UTC