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?
I think I solved this. I hadn't installed dune in my new opam switch so dune
was actually the system-wide dune binary.
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
And maybe update some dune files to newer (lang coq 0.2)
Last updated: Dec 05 2023 at 12:01 UTC