(boot) assumes that the Prelude is
Coq.Init.Prelude. It would be great if we could configure this.
@Emilio Jesús Gallego Arias do you want to add anything more?
Thanks @Ali Caglayan , when
(boot) is added to a library
Foo it does indeed do a bit more:
-boot[which disables the automatic binding of the
Coqprefix] and adding the extra dependency
Foo.Init.Preludeas it implicit and
coqdepwon't add it.
This model may not be flexible enough for those looking to replace Coq's stdlib, in particular HoTT and likely stdlib2, so the question is, what should we add to
(boot ...) so it better fits these devs.
-boot [which disables the loading of prelude]
Do you mean -noinit? AFAIK -boot still loads Prelude.vo
Sorry, I meant
-boot but I got the description wrong, fixed, thanks
Having dune compile
Foo.Init.* with those flags doesn't seem robust to me. Would a better option be putting a dune file in the
Init folder? Then we can mark everything in that folder to be compiled with
Or better yet, have a mode for dune so that there is no
At least for the stdlib it is more subtle than just modifying some flags, as outlined above [extra implicit deps appear, only when boot lib is in scope]
@Emilio Jesús Gallego Arias Any progress with this?
@Ali Caglayan , nope, but I'd be happy to schedule a room in the CUDW to work on that together if you want, it shouldn't take long.
@Emilio Jesús Gallego Arias That sounds good, what time is suitable for you?
I'd say most times free in the CUDW should work, we tend to organize quite organically
Where can I find the free times in the CUDW?
See the program https://github.com/coq/coq/wiki/Coq-Users-and-Developers-Workshop-2020#program
OK, I am available at 13:00 tomorrow is that good for you? I haven't quite understood what you mean by scheduling a room though.
The ongoing CUDW (see the corresponding Zulip stream) has a main visio room and 8 breakout rooms. People self-organize around a topic by chatting in Zulip, finding a suitable time to talk live and a free breakout room to join together.
13:00 Paris time sounds good to me. Indeed, join the workshop BBB visio system and you will see the breakout rooms
@Emilio Jesús Gallego Arias I am in BBB now
Hi @Ali Caglayan , thanks! I need a few more minutes sorry, running late today
Ok I'm good, sorry for the dealy
Last updated: Oct 16 2021 at 07:02 UTC