Ali Caglayan (Aug 25 2020 at 17:11): Ali Caglayan (Aug 25 2020 at 17:11):Currently (boot) assumes that the Prelude is Coq.Init.Prelude. It would be great if we could configure this.
Ali Caglayan (Aug 25 2020 at 17:11):@Emilio Jesús Gallego Arias do you want to add anything more?
Emilio Jesús Gallego Arias (Aug 25 2020 at 17:20):Thanks @Ali Caglayan , when (boot) is added to a library Foo it does indeed do a bit more:
Foo.Init.* with -boot -noinit-boot [which disables the automatic binding of the Coq prefix] and adding the extra dependency Foo.Init.Prelude as it implicit and coqdep won'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.
Gaëtan Gilbert (Aug 25 2020 at 17:27):-boot [which disables the loading of prelude]
Do you mean -noinit? AFAIK -boot still loads Prelude.vo
Emilio Jesús Gallego Arias (Aug 25 2020 at 17:29):Sorry, I meant -boot but I got the description wrong, fixed, thanks
Ali Caglayan (Aug 27 2020 at 11:00):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 -boot and -noinit.
Ali Caglayan (Aug 27 2020 at 11:01):Or better yet, have a mode for dune so that there is no Init library.
Emilio Jesús Gallego Arias (Aug 27 2020 at 14:09):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]
Ali Caglayan (Dec 01 2020 at 14:57):@Emilio Jesús Gallego Arias Any progress with this?
Emilio Jesús Gallego Arias (Dec 01 2020 at 15:30):@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.
Ali Caglayan (Dec 01 2020 at 15:43):@Emilio Jesús Gallego Arias That sounds good, what time is suitable for you?
Emilio Jesús Gallego Arias (Dec 01 2020 at 15:48):I'd say most times free in the CUDW should work, we tend to organize quite organically
Ali Caglayan (Dec 01 2020 at 15:57):Where can I find the free times in the CUDW?
Emilio Jesús Gallego Arias (Dec 01 2020 at 16:02):See the program https://github.com/coq/coq/wiki/Coq-Users-and-Developers-Workshop-2020#program
Ali Caglayan (Dec 01 2020 at 16:07):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.
Théo Zimmermann (Dec 01 2020 at 16:42):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.
Emilio Jesús Gallego Arias (Dec 01 2020 at 17:31):13:00 Paris time sounds good to me. Indeed, join the workshop BBB visio system and you will see the breakout rooms
Ali Caglayan (Dec 02 2020 at 11:59):@Emilio Jesús Gallego Arias I am in BBB now
Emilio Jesús Gallego Arias (Dec 02 2020 at 12:05):Hi @Ali Caglayan , thanks! I need a few more minutes sorry, running late today
Emilio Jesús Gallego Arias (Dec 02 2020 at 12:18):Ok I'm good, sorry for the dealy
Emilio Jesús Gallego Arias (Dec 02 2020 at 12:18):joining
Last updated: Oct 13 2024 at 01:02 UTC