Stream: Dune devs & users

Topic: user-contrib


view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 15:54):

Hi folks, I have been thinking a bit more about installed_theories for 1.0 version of the language, and this is what I think:

That should provide a good experience I think, WDYT?

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:03):

When you find a theory in contrib/, how do you add its transitive dependencies?

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:04):

For example, if we have:

(coq.theory (name a))
(coq.theory (name b) (theories a))
(coq.theory (name c) (theories b))

How do we make sure that c adds -Q for a if both a and b are installed (rather than local).

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:14):

Ahhh true :(

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:15):

For 1.1 version we will have the meta data

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:16):

So we need (unfortunately) to trade:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:16):

pick your poison

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:21):

I have no issues with providing a reduced user experience for those that rely on coq makefile theories, but it's a real shame that we need to expose these sharp edges at all to those that stick to the dune only world.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:26):

I think we can only do that as a fallback

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

For people whose dep chain is fully dunerized we can do good, right?

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

we would only need to add the pain point for those that depend on non-dunerized deps

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

Yes, it is a shame, but can we do differently?

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:30):

Emilio Jesús Gallego Arias: For people whose dep chain is fully dunerized we can do good, right?

I don't see how this can be done with installing the necessary metadata in the dune-package

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:31):

Then let's pick poison number one, even in the form of having to add to theories manually

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:31):

I think only a small subset of users will have to do that

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:31):

and will actually motivate people to port packages people are using

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:32):

so if your dep is not using dune yet

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:32):

you need to add the required libs

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:32):

that's a PITA, but still much better than today situation with make

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:32):

I don't see how the poison is enough though. Even if the user is only relying on dune libraries, how does dune know the theory dependencies of installed theories?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:32):

let's start installing dune-package for Coq theories

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:32):

Emilio Jesús Gallego Arias said:

that's a PITA, but still much better than today situation with make

Sure, that's because that's a very low bar

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:33):

in fact we can even install in two places for now

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:33):

I am assuming here we can't transition everything to dune at the same time

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:33):

I think my assumption is correct

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:33):

we need to provide a path

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:33):

yeah, transitions are a big pain

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:33):

Emilio Jesús Gallego Arias said:

let's start installing dune-package for Coq theories

Okay, but let's recall that this needs public names for lazy loading. E.g. so that when dune sees (theories foo.bar) it knows that it must look into the package of foo.

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:35):

Or an alternative lazy loading scheme I suppose

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:35):

Umm, I think we discussed not allowing that?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:35):

ah sorry, I'm confused

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:36):

we need two fields I think

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:36):

maybe that's the best (legacy_theories ) and (theories ..)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:36):

with a proper (theories pkg:foo.bar)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:36):

Yeah it is tricky to retrofit

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:38):

The pkg:foo syntax works fine. Just keep in mind that it introduces redundancies. E.g.:

(theories mathcomp:mathcomp)

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:38):

(not that I care very much about that)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:38):

wouldn't that be (theories coq-mathcomp-ssreflect:mathcomp.ssreflect) ?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:38):

yeah it looks pretty large

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:39):

ah yes, that's the full package name

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

but the package is named like that

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

and some packages like metacoq name the package different

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

I dunno

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

we can think of a nicer system

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

we could have just the package name mean all the theories?

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

but I dunno

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:42):

I suppose it's not so bad if we allow people to immediately pull more than one theory:

(theories (:coq-mathcomp-ssreflect mathcomp.ssreflect mathcomp.foobar ..))

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:44):

Yes, we have no idea how people will organize tho, now that they can

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:45):

for example, my port of compcert uses a single one, but I'm sure compcert devs would modularize that

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:45):

Sure, but note that they wouldn't be impacted by that. One can always omit the package name for theories in the dune project.

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:46):

E.g. inside mathcomp itself, one does not need to qualify the packages as dune already knows that all the theories belong to a single project.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 17:46):

they are actually 5 opam packages tho

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:47):

it still doesn't matter as dune has a package <-> theory map for every project

view this post on Zulip Ali Caglayan (Jun 23 2022 at 17:49):

There is only one theory in user-contrib and that is user-contrib

view this post on Zulip Ali Caglayan (Jun 23 2022 at 17:50):

I don't see any other way to support depending on user-contrib

view this post on Zulip Ali Caglayan (Jun 23 2022 at 17:50):

We can at the same time introduce new installation layout for coq packages

view this post on Zulip Ali Caglayan (Jun 23 2022 at 17:50):

We pass -Q user-contrib "" to coqc and that's it

view this post on Zulip Ali Caglayan (Jun 23 2022 at 17:50):

That way if you write a theory in your theories field dune can find it from the proper place with all the correct metadata

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 17:51):

Here's another idea. It comes at the cost of making lazy loading less granular, and it doesn't work for private theories:

When trying to resolve mathcomp.foo in:

(coq.theory
 (name a)
 (package c)
 (theories mathcomp.foo))

We look into the dune-project (or opam file) of the package c. In particular, the depends field. Then we eagerly load all the packages in that depends field and resolve mathcomp.foo from there.

view this post on Zulip Ali Caglayan (Jun 23 2022 at 17:59):

Is it too late to go back to (public_name)?

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 18:00):

It's not enough. Public names work because they introduce a restriction on library/theory names

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 18:01):

E.g. theory foo(\.\alpha)* must always live in package foo.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 18:02):

Ali Caglayan said:

We pass -Q user-contrib "" to coqc and that's it

we can also pass -Q user-contrib/foo foo and have more control, no?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 18:03):

How do rust or other large-scale build systems organize this?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 18:03):

are packages 1:1 to libraries?

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 18:04):

Emilio Jesús Gallego Arias said:

are packages 1:1 to libraries?

I believe so

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 18:04):

that could make sense for Coq too

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 18:04):

maybe not

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 18:04):

ummm

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 18:04):

haha

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 18:06):

i don't think it's such a bad idea tbh.

view this post on Zulip Rudi Grinberg (Jun 23 2022 at 18:07):

but note that users will still need to know about packages for plugins

view this post on Zulip Ali Caglayan (Jun 23 2022 at 18:07):

Emilio Jesús Gallego Arias said:

Ali Caglayan said:

We pass -Q user-contrib "" to coqc and that's it

we can also pass -Q user-contrib/foo foo and have more control, no?

No because not every directory in user-contrib is a theory, some are multiple or even half. The only sound solution IMO is to treat the whole thing as a theory.

view this post on Zulip Ali Caglayan (Jun 23 2022 at 18:09):

btw -Q user-contrib "" is actually what Coq is doing last time I checked. We obviously want to do this with -boot however.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 18:40):

using more granular -Q for user-contrib does allow to fail when the user forgets deps and are installed, that's a big up for me. True, it allows the user to declare weird stuff for non-dunerized packages.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2022 at 18:40):

So I think that's a tradeoff

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2022 at 15:31):

Summary of some possible rules:

Install
=======

1.0 version [for (package coq-foo) (theory Bar)]
  lib/coq-foo/dune-package
  lib/coq/user-contrib/Bar/Foo.v

1.1 version [for (package coq-foo) (theory Bar)]]
  lib/coq-foo/dune-package
  lib/coq-foo/Bar/Foo.v

Read
====

1.0 version [(theories Bar)]
  will do -boot -Q lib/coq/user-contrib/Bar Bar

1.1 version [(theories coq-pkg1.Util coq-pkg2.Util)] ??
  will do -boot -Q lib/coq-pkg1/Bar Bar -boot -Q lib/coq-pkg2/Bar Bar
  => error (likely)

2.0 version [(theories coq-pkg1.Util coq-pkg2.Util)] ??
  will do -boot -Q lib/coq-pkg1/Bar coq-pkg1.Bar -boot -Q lib/coq-pkg2/Bar coq-pkg2.Bar?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 03 2023 at 00:08):

This is the only real blocker to have a working dune setup for almost all Coq opam packages, hopefully we can implement it soon

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:48):

I had a stab at implementing it over the holidays, but I ran into a few issues. It would be good to have a hacking session so we can discuss some of the difficulties I encountered.

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:51):

One of the design issues at the moment is that the entire coq_lib logic relies on a theory coming equiped with basically a stanza. There are two ways we can go about changing this.

  1. Make up a stanza for installed user-contrib
  2. Relax the data in coq_lib to have something less than a stanza.

The first is a bit hacky but the second will require a lot more thought than I have been able to give it.

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:53):

Since user-contrib files do not come with an associated dune or _CoqProject file we cannot really hold the hand of the user about setting up correct flags.

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:54):

If I have a user-contrib theory A and a theory X that depends on A, then I have to match the flags in A (like -noinit, -indices-matter etc.)

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:54):

That is perhaps a suitable cost for a user interested in doing advanced things like this so this is not a big worry.

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:55):

A bigger worry would be how we partition user-contrib. If I have a theory that depends on say mathcomp, then there is no way for us to make sure we really meant that or more specifically mathcomp.algebra.

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:58):

We can provide in the future, an alternative installation solution which has nice dune-package meta data using COQPATH or something. But that will require more future work.

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:59):

My main worry with user-contrib is that we are trying to bend over backwards to support a flawed design, which makes our implementation more susceptable to bugs etc.

view this post on Zulip Ali Caglayan (Jan 03 2023 at 11:59):

I'm still in favour of supporting it, but it is not easy so far.

view this post on Zulip Gaëtan Gilbert (Jan 03 2023 at 12:03):

Ali Caglayan said:

If I have a user-contrib theory A and a theory X that depends on A, then I have to match the flags in A (like -noinit, -indices-matter etc.)

no? It's perfectly possible to use a noinit library together with a yesinit library
also possible to give up on indices matter although likely to be inconsistent
regardless I don't see why dune would care

view this post on Zulip Paolo Giarrusso (Jan 03 2023 at 12:06):

Even if it should, it can't for user-contrib I guess, so it's one less problem

view this post on Zulip Emilio Jesús Gallego Arias (Jan 03 2023 at 14:44):

I have in mind something much simpler like what is done for ocamlfind packages in the OCaml world, the infrastructure for "installed libs" is already there

view this post on Zulip Emilio Jesús Gallego Arias (Jan 03 2023 at 14:44):

but yes we gotta do a hacking session

view this post on Zulip Rodolphe Lepigre (Jan 03 2023 at 15:48):

Yeah, I agree with this. We should not reinvent the wheel: I would just define a Coq package to be an ocamlfind package containing a directory named coq-lib (or something similar) inside. The corresponding entry in the META file could then define both plugins and other Coq packages that are depended on.

I really think that before more hacking takes place, an installation format should be agreed upon (whether it is the one I hinted above, which I also think is what @Emilio Jesús Gallego Arias had in mind, or something else), so that we all understand where this is going.

I'd be happy to take part in a hacking session to discuss all this.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 03 2023 at 15:50):

Yes, indeed as noted above there are two orthogonal things:

I want to do 1 first, then migration of many packages should provide a good base for the design requirements of 2.

view this post on Zulip Ali Caglayan (Jan 03 2023 at 19:59):

Gaëtan Gilbert said:

Ali Caglayan said:

If I have a user-contrib theory A and a theory X that depends on A, then I have to match the flags in A (like -noinit, -indices-matter etc.)

no? It's perfectly possible to use a noinit library together with a yesinit library
also possible to give up on indices matter although likely to be inconsistent
regardless I don't see why dune would care

From the point of view of Dune, if a user is importing a library (say HoTT) and a file fails to be imported due to having different compilation flags, this error will not be very useful. What I was hoping was that Dune would step in and tell the user that the library has differing flags.

view this post on Zulip Gaëtan Gilbert (Jan 03 2023 at 20:23):

it will not fail to be imported

view this post on Zulip Ali Caglayan (Jan 03 2023 at 21:14):

It will fail to get imported if I make a conflicting assumption to one in prelude. For example, reserving a notation level to be a different associativity.

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 05:53):

does dune even check flag consistency across theory stanzas today?

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 05:54):

either way, I think we all agree this can't be in scope for user-contrib since the info isn't there.

view this post on Zulip Ali Caglayan (Jan 04 2023 at 16:06):

We don't check flag consistency, but it is something I would like to do, or at least make aparent to the user.


Last updated: Feb 04 2023 at 02:03 UTC