Stream: Dune devs & users

Topic: Boot library


view this post on Zulip Rudi Grinberg (May 27 2022 at 15:59):

What was the story with the boot library again? Can we eliminate the special casing of it in dune if we introduce per_file flags?

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 16:02):

Likely, boot is a bit like ocaml stdlib

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 16:03):

there are two cases:

Second case is harder to handle

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 16:03):

What's the problem with the boot library?

view this post on Zulip Rudi Grinberg (May 27 2022 at 17:28):

  1. So I suppose this bit is the one that is solved by the per_file flags
  2. Right, this will need to remain.

It's a bit tougher to handle some sanity checks when the boot library is composed. One must make sure there's only a single boot library in every single compilation closure.

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 17:29):

Yes, it is the same tho that having two conflict public libs

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 17:30):

with the same name

view this post on Zulip Rudi Grinberg (May 28 2022 at 02:05):

Alright, it wasn't a huge problem after all to make it work with composition

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 10:07):

Boot is quite useful as it allow us to compose with Coq itself

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 10:08):

and we have plans to run the CI incrementally, where the full CI is composed, tho we need to solve vendoring better, but we can do a lot

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:26):

What do you think about compiling everything in coq with -noinit and making people depend on the boot library explicitly? I wish we had that in OCaml at least

view this post on Zulip Karl Palmskog (May 28 2022 at 15:27):

do you mean people would have to opt in to use the prelude? If we want wide adoption of Dune for building Coq projects, that's in my view a no-go (the support issues would be huge)

view this post on Zulip Karl Palmskog (May 28 2022 at 15:28):

I think a lot of people want the option to get Coq with -noinit via Dune, though (e.g., UniMath, HoTT)

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:28):

Why would the support issues be huge?

view this post on Zulip Karl Palmskog (May 28 2022 at 15:29):

because regular users would not be able to figure out what they need to do to add the prelude, they have no idea what the prelude even is

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:30):

A regular user is someone that will use dune but will have no idea that coq consists of libraries?

view this post on Zulip Karl Palmskog (May 28 2022 at 15:30):

the regular Coq user may be able to distinguish between Coq's stdlib and something like MathComp, but not more fine-grained than that

view this post on Zulip Karl Palmskog (May 28 2022 at 15:32):

there is a still minority of users that actually need -noinit, like UniMath users, but since they are the minority by far, better to get prelude by default in Dune

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:32):

How does a regular user not know to add the prelude but know to add the Stdlib or mathcomp?

view this post on Zulip Karl Palmskog (May 28 2022 at 15:33):

a regular user has a vague idea what stdlib is, and will be annoyed and get stuck when they can't use it (due to prelude not being loaded)

view this post on Zulip Karl Palmskog (May 28 2022 at 15:34):

they may know they have to add some extra magic Require Import command to get some MathComp. But even that will not work without the prelude.

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:35):

I don’t see it. The regular user is informed enough to use dune and external libraries, but just barely not informed enough to ask for the Stdlib explicitly. Sounds like too fine of a distinction.

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:35):

If they know how to pull mathcomp, and mathcomp pulls the prelude, they don’t need to pull it explicitly

view this post on Zulip Karl Palmskog (May 28 2022 at 15:36):

they (may) know the Coq-level incantation for libraries like MathComp, since people put this in tutorials

view this post on Zulip Karl Palmskog (May 28 2022 at 15:37):

but even getting people to the point of a multi-file Coq project can be a struggle

view this post on Zulip Karl Palmskog (May 28 2022 at 15:38):

I can say that I would personally never recommend using Dune to a beginner if -no-init is the default.

view this post on Zulip Karl Palmskog (May 28 2022 at 15:40):

but sure, "production grade" Coq projects won't have a problem, and may even appreciate barebones approach. But this is far from the support burden in community forums.

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:42):

I think that using dune and coq will require reading an introduction to both dune and its coq stanzas. You would think that this is already enough that such a small addition isn’t going to matter much.

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:42):

Indeed @Rudi Grinberg there are a couple of open (and accepted) issues to make the stdlib a regular library

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:43):

so yes that's a good idea, but there is quite a few things to do first

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:43):

maybe in 2.0 version we can enforce that

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:43):

but the first todo is to require users to qualify the imports

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:43):

so Require Lists becomes From Coq Require Lists

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:43):

etc...

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:43):

and that's tricky due to some horrible horrible (legacy) code in Coq that manages that

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:44):

Sometimes I look at Coq's source code and I wonder how it can work at all XD

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:44):

I've seen few projects like it

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:45):

Actually a big blocker to do this is indeed our lack of Coq packages

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:45):

So making people write (theories stdlib) today isn’t going to work?

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:45):

It would work if we had proper packages

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:45):

What is improper about the packages today?

view this post on Zulip Karl Palmskog (May 28 2022 at 15:45):

in my view, for Dune 1.0, it's a really bad idea with (theories stdlib)

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:46):

Rudi Grinberg said:

What is improper about the packages today?

once installed, they are all stashed together in user-contrib and you have no way to identify the package a file comes from

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:46):

unless of course you drop compat with coq_makefile

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:46):

Oh this thing again

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:46):

yes

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:46):

...

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:46):

it is a big constraint

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:47):

but maybe we can get rid of it sooner than we think

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:47):

Can’t we just install in both locations and live with the wasted disk space for now?

view this post on Zulip Karl Palmskog (May 28 2022 at 15:47):

please don't drop user-contrib installation for 1.0

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:47):

but IMHO it is good that we support for a big the use case where a user can build a Coq theory with Dune and still depend on a non-dunerized theory

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:47):

Yes, I’m not proposing to drop support

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:48):

Rudi Grinberg said:

Can’t we just install in both locations and live with the wasted disk space for now?

yes we can do that, but I'm not sure we gain a lot unless we drop "dune theories can depend on non-dune theories"

view this post on Zulip Karl Palmskog (May 28 2022 at 15:48):

installation in two places is fine by me

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:48):

but YMMV

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:48):

I’m saying that dune will use the dune-package stuff while a fallback exists for makefiles

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:48):

I think we agree we want to do what you propose, the question is how to bootstrap the whole business

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:49):

So maybe using two fields is a good compromise

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:50):

but more work for us than having the current semantics in 1.0, and moving to the new semantics in 2.0

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:51):

I suppose. But it’s not straightforward, as the boot hacks were quite a time sink for both of us I think. And the work we’re talking about is useful long term

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:52):

Remind me why we need two fields though

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:52):

You mean theories and legacy_theories?

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:54):

As far as I understand, there’s work on a new stdlib right? Seems like another reason to stop special casing

view this post on Zulip Karl Palmskog (May 28 2022 at 15:56):

the "new stdlib" project is considered stalled. The largest potential for -noinit is in my view: UniMath, HoTT, and perhaps in the longer run, MathComp-based projects

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:57):

Yes, I was trying to locate the issue, but yes, we don't want special casing

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:57):

but actually yes we don't need a new field

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:57):

it should be coq lang version that controls it

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:57):

so at some point, for example, in (using coq 1.1)

view this post on Zulip Rudi Grinberg (May 28 2022 at 15:58):

@Karl Palmskog if you don’t want your students to know about libraries, why do you want them to use dune anyway? IMO that’s basically dune’s main advantage

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:58):

users have to explicitly require the stdlib

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:59):

still we need two changes upstream which are tricky, and I thought they had issues, but they have not:

view this post on Zulip Karl Palmskog (May 28 2022 at 15:59):

@Rudi Grinberg we want people to use Dune in all high-profile projects to get benefits of composition and automation in opam packaging, etc. Regular users will get benefits from this as better automation trickles down. They can then follow simple recipes for using Dune in their own projects based on a bigger library. While remaining mostly ignorant of how Coq and libraries are organized.

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 15:59):

Actually already in 2015, when I release jsCoq, users where forced to write From Coq and import the prelude explicitly.

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:00):

But I got so much backslash due to lack of compat that I had to backtrack

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:00):

wrong choice

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:00):

(myself backtracking)

view this post on Zulip Rudi Grinberg (May 28 2022 at 16:00):

The way I see the theories field look up working:

  1. Look up in the dune-package
  2. If that fails, look up in user-contrib

Does that sound reasonable?

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:03):

What's the input on theories?

view this post on Zulip Rudi Grinberg (May 28 2022 at 16:04):

The name of theories as defined in the dune files for 1.

view this post on Zulip Rudi Grinberg (May 28 2022 at 16:04):

For 2. Some sort of a reverse engineering scheme from the file structure I suppose

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:06):

I mean what's the syntax of (theories ...)

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:06):

the syntax for a theory name

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:07):

To start working today in porting project, the idea was that 2 was enough

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:07):

but at some point we want to do 1 obviously

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:12):

https://github.com/coq/coq/issues/16091

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:29):

Warnings seem necessary anyway for at least one release (and probably more), before possibly breaking every single Coq development in existence… but we’d still be allowed to Export the Coq prelude, right? So part of this could be absorbed by downstream preludes

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:35):

Yes, the breakage may not be so bad

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:35):

We need to stop Requirewithout FromIMHO

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:35):

that only leaves every single Require going into the stdlib

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:35):

that will break a lot of code, but I don't see any other way

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:36):

we could keep the status quo tho, I dunno

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:36):

Can you write a convincing argument for the entirety of the Coq userbase?

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:36):

Paolo Giarrusso said:

Can you write a convincing argument for the entirety of the Coq userbase?

I don't know

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:36):

why I need that?

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:37):

Require without From should mean: "import from current package"

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:37):

There are already a few alternatives libraries that don't use stdlib, seems obvious for it to lose special status

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:38):

and in fact, it is much clear to read From Coq Require Lists than Require Lists where you got no idea where it comes from

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:40):

I don’t know the exact general practice, but I’m not sure everybody would be happy with that attitude. An alternative might be that breaking code is rude, so you need to convince people there’s a good reason

view this post on Zulip Karl Palmskog (May 28 2022 at 16:40):

to be sure, those [Emilio's] are arguments in favor of recommending From X ..., but they don't really reach the level of "we must mandate it right now".

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:40):

of course, in the usual kind of “you have to”: there’s nothing you have to do, but if you want to have users (and happy users), there are things you probably want to do.

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:42):

Yes breaking code is not good

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:42):

but this time there is a good justification for it in many fronts

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:42):

Many people may not be happy with that attitude, however, I'm unsure what can I tell to them

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:43):

I can have meaningful discussion with build system experts, I've been myself working Coq builds since 2015 and I've learned a lot

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:43):

but discussion with non experts is just not very productive

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:43):

they'll have to trust the experts I'm afraid

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:43):

I see this often with math-comp, people love to bash math-comp

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:44):

then when I try to get meaningful discussion, it turns out they never even used it

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:44):

?!?!?!?

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:44):

who said anything about discussion?

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:44):

That part of human nature will never ever cease to amaze me

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:44):

I’m afraid your users are human beings and you don’t get to change them :-)

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:45):

Well your question was "can you write a convincing argument for the entirety of Coq userbase"

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:45):

let me answer differently

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:45):

no I can't

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:45):

it is impossible

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:45):

I can only provide a convincing argument for people that are knowleable, for the rest, I have no idea

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:46):

I don't get or want to change them

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:46):

yes

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:46):

I get to make Coq work better and more maintanable tho

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:46):

and implement a faster more modular and easier build setup

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

If Makarious had listened to what (non-expert) Isabelle users were saying

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

they would still be using proof general

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

in sequential mode

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

that's a problem with "open" development

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

eveyone is entitled to an opinion

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:47):

I think this is ultimately the domain of @Théo Zimmermann — I think major breaking changes usually get more explanations, but I haven’t investigated exactly to which extent

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

regardless of what their actual expertise is

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:48):

here the motivation is very easy: special and hardcoded cases bring lots of problems

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:48):

and in Coq's case they bring zero benefit and whole lot of special options and flags

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:48):

and considerable custom code

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:48):

we already have a mechanism for handling basic namespaces, let's use ti

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:49):

dunno, peer review works reasonably well even if the reviewers are by definition less experts than the authors — the authors just have to make their case compelling

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:49):

in any case, I am aware I am not an expert, and I most certainly don’t get a vote :-)

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:50):

you may think that peer review works well, but for many that's not the case, see for example https://twitter.com/neuralreckoning/status/1529767585990029312 which I fully share. Moreover peer review requires the reviewer to be assigned an expertise level, which doesn't happen here

The current system of journals and peer review is not serving science. I have therefore resigned from all editorial roles and will no longer do pre-publication peer review. I explain why in this article and in the thread below. Please consider joining me. http://neural-reckoning.org/reviewing.html

- Dan Goodman (@neuralreckoning)

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:50):

I consider you an expert @Paolo Giarrusso and of course I heard all you say, and if we vote you have a vote

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:50):

your question was about "the entirety of Coq's user base"

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:50):

that's very different

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:51):

if your question is can you provide a good argument for Paolo and the dev team, for sure I can

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:52):

I am shocked by how many times I have been for example "proof explained"

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:52):

by people, that sorry for them, don't know very well what they are talking about

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:53):

or told how to program in OCaml by people that don't actually know how to program in OCaml

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 16:53):

etc,etc...

view this post on Zulip Paolo Giarrusso (May 28 2022 at 16:53):

as said: dunno how much convincing will be needed for users, but I expect there will be some text in the changelog (and probably before that), and the better it is, the fewer protests you will see, and the more quickly users will migrate to the new version

view this post on Zulip Paolo Giarrusso (May 28 2022 at 17:09):

more importantly, some migration help would be great — either a warning, or an option to enable/disable the special cases if that’s easier

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:19):

Yes that's a very good point

view this post on Zulip Rudi Grinberg (May 28 2022 at 17:28):

Emilio Jesús Gallego Arias said:

the syntax for a theory name

The same one as today (theories foo ..). Perhaps I didn't underdstand the question?

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:30):

Then why you need 1 at all

view this post on Zulip Emilio Jesús Gallego Arias (May 28 2022 at 17:30):

?

view this post on Zulip Rudi Grinberg (May 28 2022 at 18:52):

The advantage would be that if we resolve something with 1, we don't need to allow the user to peek into the junk yard that is user-contrib. Where they can accidentally use all kinds of stuff they didn't explicit depend on

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2022 at 12:23):

@Rudi Grinberg unfortunately Coq already puts in scope everything in user-contrib :/

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2022 at 12:23):

So for the "1.0" version of Coq + dune we have no way to forbid stuff in user-contrib, but we should be able to do so once we bump

view this post on Zulip Karl Palmskog (May 29 2022 at 14:28):

supporting user-contrib for 1.0 is to me essential for Coq people to get hooked on using Dune. If we can reach OCaml level prevalence of Dune, then a lot of options open up for ecosystem improvements.

view this post on Zulip Emilio Jesús Gallego Arias (May 30 2022 at 12:24):

Yes @Karl Palmskog , it is clear we need to support that

view this post on Zulip Ali Caglayan (May 30 2022 at 12:25):

Rudi and I are planning to support user-contrib first, we don't have any plans to revolutionize Coq package installation structure AFAIK

view this post on Zulip Paolo Giarrusso (Jun 01 2022 at 13:35):

@Emilio Jesús Gallego Arias I realized Coq already has a process for such discussions — CEPs. Would it be appropriate here?

view this post on Zulip Paolo Giarrusso (Jun 01 2022 at 13:36):

not sure in Coq, but that's how we'd use Scala Enhancement Proposals in Scala.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 01 2022 at 13:39):

Yes, for the 2.0 library model we need something like a CEP

view this post on Zulip Emilio Jesús Gallego Arias (Jun 01 2022 at 13:39):

no question

view this post on Zulip Emilio Jesús Gallego Arias (Jun 01 2022 at 13:39):

We didn't start such document because it makes sense first to try to port the full CI to Dune and see what we discover


Last updated: Feb 04 2023 at 01:03 UTC