Fortunately Ali and Rudi took over the implementation of inter-scope composition of
(coq.theories ...) for Dune and a PR we can use exists at https://github.com/ocaml/dune/pull/5784 ; this should help to build all the addons better.
Still I'd like to add support for a
coq-pkg rule (which is very easy!) and compilation of the .js files
Hi! Did you end up doing that? do you need any help?
Not yet as we are testing the PR and https://github.com/ejgallego/coq-universe but surely I can open a PR soon
actually I am perplexed. Even when the
META.coq-equations is there, running
coqdep fails with
*** Error: in file Loader.v, could not find META.coq-equations.. Still, compiling with -j1 succeeds while compiling multiprocess fails.
I see that coqdep needs to be invoked with
-m META. What makes Dune pass this flag?
@Shachar Itzhaky It looks like you had posted to the wrong topic. I have moved your messages to what seemed to me like the most likely relevant topic, but I'm not too sure.
@Shachar Itzhaky beware of the two modes
Do you have a link to the actual tree?
my bad @Théo Zimmermann
Last updated: May 31 2023 at 02:31 UTC