Stream: jsCoq

Topic: Addons and Dune


view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Jun 08 2022 at 14:08):

Hi! Did you end up doing that? do you need any help?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 03 2022 at 18:20):

@Shachar Itzhaky beware of the two modes

view this post on Zulip Emilio Jesús Gallego Arias (Jul 03 2022 at 18:20):

what's on Loader.v

view this post on Zulip Emilio Jesús Gallego Arias (Jul 03 2022 at 18:20):

?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 03 2022 at 18:21):

Do you have a link to the actual tree?

view this post on Zulip Shachar Itzhaky (Jul 03 2022 at 19:33):

my bad @Théo Zimmermann


Last updated: Jan 31 2023 at 10:01 UTC