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