Stream: Dune devs & users

Topic: Make (boot) stable


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

view this post on Zulip Ali Caglayan (Aug 25 2020 at 17:11):

@Emilio Jesús Gallego Arias do you want to add anything more?

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

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.

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

view this post on Zulip Emilio Jesús Gallego Arias (Aug 25 2020 at 17:29):

Sorry, I meant -boot but I got the description wrong, fixed, thanks

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

view this post on Zulip Ali Caglayan (Aug 27 2020 at 11:01):

Or better yet, have a mode for dune so that there is no Init library.

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

view this post on Zulip Ali Caglayan (Dec 01 2020 at 14:57):

@Emilio Jesús Gallego Arias Any progress with this?

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

view this post on Zulip Ali Caglayan (Dec 01 2020 at 15:43):

@Emilio Jesús Gallego Arias That sounds good, what time is suitable for you?

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

view this post on Zulip Ali Caglayan (Dec 01 2020 at 15:57):

Where can I find the free times in the CUDW?

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

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

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

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

view this post on Zulip Ali Caglayan (Dec 02 2020 at 11:59):

@Emilio Jesús Gallego Arias I am in BBB now

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2020 at 12:18):

Ok I'm good, sorry for the dealy

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2020 at 12:18):

joining


Last updated: Oct 16 2021 at 07:02 UTC