Emilio Jesús Gallego Arias (Jun 01 2022 at 18:11): Emilio Jesús Gallego Arias (Jun 01 2022 at 18:11):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
Shachar Itzhaky (Jun 08 2022 at 14:08):Hi! Did you end up doing that? do you need any help?
Emilio Jesús Gallego Arias (Jun 08 2022 at 20:59):Not yet as we are testing the PR and https://github.com/ejgallego/coq-universe but surely I can open a PR soon
Shachar Itzhaky (Jul 03 2022 at 17:57):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.
Shachar Itzhaky (Jul 03 2022 at 18:09):I see that coqdep needs to be invoked with -m META. What makes Dune pass this flag?
Théo Zimmermann (Jul 03 2022 at 18:14):@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.
Emilio Jesús Gallego Arias (Jul 03 2022 at 18:20):@Shachar Itzhaky beware of the two modes
Emilio Jesús Gallego Arias (Jul 03 2022 at 18:20):what's on Loader.v
Emilio Jesús Gallego Arias (Jul 03 2022 at 18:20):?
Emilio Jesús Gallego Arias (Jul 03 2022 at 18:21):Do you have a link to the actual tree?
Shachar Itzhaky (Jul 03 2022 at 19:33):my bad @Théo Zimmermann
Last updated: Apr 20 2024 at 01:41 UTC