Janno (Jul 11 2020 at 13:00): 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?
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.
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
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: Dec 05 2023 at 12:01 UTC