Stream: Dune devs & users

Topic: Boot library

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?

Emilio Jesús Gallego Arias (May 27 2022 at 16:02):

Likely, boot is a bit like ocaml stdlib

Emilio Jesús Gallego Arias (May 27 2022 at 16:03):

there are two cases:

• compilation of the stdlib itself: coqc needs to know that the stdlib is not available, so implicit initalization must be disabled (-boot flag)
• compilation of the libs using the stdlib in scope: an implicit dependency to Init.Prelude.vo has to be added

Second case is harder to handle

Emilio Jesús Gallego Arias (May 27 2022 at 16:03):

What's the problem with the boot library?

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.

Emilio Jesús Gallego Arias (May 27 2022 at 17:29):

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

Emilio Jesús Gallego Arias (May 27 2022 at 17:30):

with the same name

Rudi Grinberg (May 28 2022 at 02:05):

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

Emilio Jesús Gallego Arias (May 28 2022 at 10:07):

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

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

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

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)

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)

Rudi Grinberg (May 28 2022 at 15:28):

Why would the support issues be huge?

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

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?

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

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

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?

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)

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.

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.

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

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

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

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.

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.

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.

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 15:43):

maybe in 2.0 version we can enforce that

Emilio Jesús Gallego Arias (May 28 2022 at 15:43):

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

Emilio Jesús Gallego Arias (May 28 2022 at 15:43):

so Require Lists becomes From Coq Require Lists

Emilio Jesús Gallego Arias (May 28 2022 at 15:43):

etc...

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 15:44):

I've seen few projects like it

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

Rudi Grinberg (May 28 2022 at 15:45):

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

Emilio Jesús Gallego Arias (May 28 2022 at 15:45):

It would work if we had proper packages

Rudi Grinberg (May 28 2022 at 15:45):

What is improper about the packages today?

Karl Palmskog (May 28 2022 at 15:45):

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 15:46):

unless of course you drop compat with coq_makefile

Rudi Grinberg (May 28 2022 at 15:46):

Oh this thing again

Emilio Jesús Gallego Arias (May 28 2022 at 15:46):

yes

Emilio Jesús Gallego Arias (May 28 2022 at 15:46):

...

Emilio Jesús Gallego Arias (May 28 2022 at 15:46):

it is a big constraint

Emilio Jesús Gallego Arias (May 28 2022 at 15:47):

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

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?

Karl Palmskog (May 28 2022 at 15:47):

please don't drop user-contrib installation for 1.0

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

Rudi Grinberg (May 28 2022 at 15:47):

Yes, I’m not proposing to drop support

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"

Karl Palmskog (May 28 2022 at 15:48):

installation in two places is fine by me

Emilio Jesús Gallego Arias (May 28 2022 at 15:48):

but YMMV

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 15:49):

So maybe using two fields is a good compromise

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

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

Rudi Grinberg (May 28 2022 at 15:52):

Remind me why we need two fields though

Rudi Grinberg (May 28 2022 at 15:52):

You mean theories and legacy_theories?

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

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 15:57):

but actually yes we don't need a new field

Emilio Jesús Gallego Arias (May 28 2022 at 15:57):

it should be coq lang version that controls it

Emilio Jesús Gallego Arias (May 28 2022 at 15:57):

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 15:58):

users have to explicitly require the stdlib

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:

• require From Coq for stdlib
• require From Coq Require Prelude explicit too

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.

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.

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:00):

wrong choice

Emilio Jesús Gallego Arias (May 28 2022 at 16:00):

(myself backtracking)

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?

Emilio Jesús Gallego Arias (May 28 2022 at 16:03):

What's the input on theories?

Rudi Grinberg (May 28 2022 at 16:04):

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

Rudi Grinberg (May 28 2022 at 16:04):

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:06):

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:06):

the syntax for a theory name

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:07):

but at some point we want to do 1 obviously

Emilio Jesús Gallego Arias (May 28 2022 at 16:12):

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:35):

Yes, the breakage may not be so bad

Emilio Jesús Gallego Arias (May 28 2022 at 16:35):

We need to stop Requirewithout FromIMHO

Paolo Giarrusso (May 28 2022 at 16:35):

that only leaves every single Require going into the stdlib

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:36):

we could keep the status quo tho, I dunno

Paolo Giarrusso (May 28 2022 at 16:36):

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:36):

why I need that?

Emilio Jesús Gallego Arias (May 28 2022 at 16:37):

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

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

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

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

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".

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.

Emilio Jesús Gallego Arias (May 28 2022 at 16:42):

Yes breaking code is not good

Emilio Jesús Gallego Arias (May 28 2022 at 16:42):

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

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:43):

but discussion with non experts is just not very productive

Emilio Jesús Gallego Arias (May 28 2022 at 16:43):

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:43):

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:44):

?!?!?!?

Paolo Giarrusso (May 28 2022 at 16:44):

who said anything about discussion?

Emilio Jesús Gallego Arias (May 28 2022 at 16:44):

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

Paolo Giarrusso (May 28 2022 at 16:44):

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

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"

Emilio Jesús Gallego Arias (May 28 2022 at 16:45):

let me answer differently

Emilio Jesús Gallego Arias (May 28 2022 at 16:45):

no I can't

Emilio Jesús Gallego Arias (May 28 2022 at 16:45):

it is impossible

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:46):

I don't get or want to change them

Emilio Jesús Gallego Arias (May 28 2022 at 16:46):

yes

Emilio Jesús Gallego Arias (May 28 2022 at 16:46):

I get to make Coq work better and more maintanable tho

Emilio Jesús Gallego Arias (May 28 2022 at 16:46):

and implement a faster more modular and easier build setup

Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

they would still be using proof general

Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

in sequential mode

Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

that's a problem with "open" development

Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

eveyone is entitled to an opinion

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:47):

regardless of what their actual expertise is

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:48):

and considerable custom code

Emilio Jesús Gallego Arias (May 28 2022 at 16:48):

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

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

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 :-)

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)

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:50):

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:50):

that's very different

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

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"

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 16:53):

etc,etc...

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

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

Emilio Jesús Gallego Arias (May 28 2022 at 17:19):

Yes that's a very good point

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?

Emilio Jesús Gallego Arias (May 28 2022 at 17:30):

Then why you need 1 at all

Emilio Jesús Gallego Arias (May 28 2022 at 17:30):

?

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

Emilio Jesús Gallego Arias (May 29 2022 at 12:23):

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

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

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.

Emilio Jesús Gallego Arias (May 30 2022 at 12:24):

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

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

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?

Paolo Giarrusso (Jun 01 2022 at 13:36):

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

Emilio Jesús Gallego Arias (Jun 01 2022 at 13:39):

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

Emilio Jesús Gallego Arias (Jun 01 2022 at 13:39):

no question

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: Oct 13 2024 at 01:02 UTC