Stream: Dune devs & users

Topic: Adding transitive deps into theories


view this post on Zulip Karl Palmskog (Jun 23 2023 at 08:52):

I have a development with the following sentence:

From VST Require Import floyd.proofauto.

However, just having (theories compcert VST) (I use a CompCert-generated file) into the dune file with Dune 3.8 and Dune-Coq 0.8 doesn't suffice:

Error: Cannot load Ltac2.Init: no physical path bound to Ltac2

That is, the transitive dependency Ltac2 (used somewhere by VST 2.12) seemingly needs to be added to theories. I don't see how this makes sense. Why should I care or want to care what dependencies my dependencies use if I just want to build? This also means that if we have a whole ecosystem of Dune packages, one person adding a dep can cascade into hundreds of people having to change their dune files.

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

This limitation is documented, unfortunately for user-contrib there is no way to know the dependencies of a particular theory, no further meta-data is there.

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

Ideas on how to improve this are welcome, but as long as we remain compatible with coq_makefile it is hard to come up with a solution.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:19):

If a package was build with with Dune, we could try to install a dune-package file in user-contrib so we could recover this information, that's a nice easy project to do if someone has cycles.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:19):

This limitation is documented,

Should be documented but I'm sure the docs can be improved a lot.

view this post on Zulip Karl Palmskog (Jun 23 2023 at 09:20):

at least if something else was installed with Dune, we should be able to avoid this kind of endless fiddling with dune files... dune-package sounds reasonable

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:21):

Yes, that's the idea.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:21):

If coq_makefile would install some metadata we could also use it too

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:21):

Like a META file for Coq theories, or anything similar.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:25):

Another interesting avenue is trying to auto-compute deps, the "theory" branch of coq-lsp kind of tries to do that, but it hooks to Coq at a lower level.

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

Anyways let's targe the dune-package support for (lang coq 1.0), that should improve lifes a lot already.

People needing to depend on packages that are built using the current version of coq_makefile will either have to specify all the deps, or tell Dune to use the full of user-contrib

view this post on Zulip Karl Palmskog (Jun 23 2023 at 09:27):

oh, is there a shorthand for using full user-contrib? Seems tempting to use in most places.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:28):

I'm unsure if that's exposed right now but we can add it very easily.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2023 at 09:28):

Note that such a flag would break vendoring easily

view this post on Zulip Paolo Giarrusso (Jun 23 2023 at 11:28):

That is, with such a flag you couldn't "override" user-contrib reliably? I guess Coq doesn't have a guaranteed search order? it's not clear why for modules with the same name...

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

What do you mean by "override" ? Such a flag would just do as Coq does and add -Q $coqlib/user-contrib ""

view this post on Zulip Paolo Giarrusso (Jun 23 2023 at 17:50):

Well, what's the problem with vendoring? I guess the problem is if you have, say, math comp in both user-contrib and your workspace and you want the workspace to override user-contrib: you never want to load a file from user-contrib when there's one in the workspace.

view this post on Zulip Paolo Giarrusso (Jun 23 2023 at 17:52):

IME that seems to work okay but I sometimes suspected bugs... And of course, if a file exists only in user-contrib, here it'll be used, while ideally the build should fail to load it. But that's a necessary evil once you enable all of user-contrib

view this post on Zulip Paolo Giarrusso (Jun 23 2023 at 17:53):

Did you mean this or sth else?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 12:50):

The problem of a "include all" flag is that is you put that theory in your workspace, indeed Dune won't see it.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 12:51):

As you won't add it to (theories ...)

view this post on Zulip Karl Palmskog (Jun 25 2023 at 12:57):

for many projects/workflows (that are just trying to build stuff without fancy composition) this is probably fine

view this post on Zulip Karl Palmskog (Jun 25 2023 at 12:58):

can I do a feature request?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:08):

Sure @Karl Palmskog , but I'm really unsure we want to add / support this.

It seems to add more complexity and a discouraged workflow to solve an unrelated issue (lack of metadata for deps).

Moreover, it breaks an expectation that all dune users have: if you depend on a dunerized lib, you can always vendor it for faster / joint development.

So adding this feature could lead to significant fragmentation for Dune packages that use the "legacy mode".

I'd rather focus on adding the required metadata to packages, for dune this is easy, for coq_makefile it shouldn't be too hard either.

view this post on Zulip Karl Palmskog (Jun 25 2023 at 13:11):

I think there is a gap between how Dune is expected to be used (OCaml style) and how it's currently used in the Coq community. We have a ton of projects using Dune in CI and the like, where vendoring/composition is not really a big concern.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:12):

Yes, but they still depend on some libs right?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 13:12):

from Paolo's comments, I think they use Dune heavily for actual development at Bedrock, but due to the editor problems, that is not common...

view this post on Zulip Karl Palmskog (Jun 25 2023 at 13:13):

in CI, we essentially assume every dep ends up in user-contribs, since installed via opam or Nix. From Paolo's comments, I think that would work out with the flag?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:13):

Vendoring / composition may be not be a big concern until new use cases arrive, for example most of these project do likely use Coq's stdlib. For example a port to a new stdlib, or just stdlib refactoring, would require vendoring to be able to be done effectively.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:14):

Karl Palmskog said:

in CI, we essentially assume every dep ends up in user-contribs, since installed via opam or Nix. From Paolo's comments, I think that would work out with the flag?

Yes, tha'ts the model we had up to 0.8, but it is a very problematic model, in particular as you don't have any kind of dep isolation.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:14):

Let me rephrase my comment: Other than the current lack of transitive dependency detection for installed theories, does the 0.8 model pose any other critical problem ?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 13:15):

I agree it can be problematic, but we are talking about an optional non-default flag that could make things a bit easier for current users of Dune.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:16):

Karl Palmskog said:

I agree it can be problematic, but we are talking about an optional non-default flag that could make things a bit easier for current users of Dune.

Yes, the flag may make things a little bit easier for current users of Dune, however it will make the work of Dune Coq maintainers much harder, and the life of people interesting in running something like the JsCoq archive or Coq-universe harder too.

view this post on Zulip Karl Palmskog (Jun 25 2023 at 13:16):

well, I'm trying to port a bunch of projects to 0.8 right now, so far the transitive dep stuff is the most inconvienent (besides the plugin bug fixed in 3.8.2)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:16):

Also it would difficult things that may rely on coq-universe such as ci fast cached, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:16):

Karl Palmskog said:

well, I'm trying to port a bunch of projects to 0.8 right now, so far the transitive dep stuff is the most inconvienent (besides the plugin bug fixed in 3.8.2)

Then let's fix that problem for Dune 3.9

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:17):

The dune part is easy, just use the existing infra to install a dune-package file

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:17):

For Coq Community, you folks just let us know what file will you install with the deps, and we can read it.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:17):

if there are no deps info, then deps of an installed theory are still empty.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:18):

Whatever we do with the flag to add all of user-contrib, the problem you are facing now needs to be solved anyways.

view this post on Zulip Karl Palmskog (Jun 25 2023 at 13:19):

but I think this can't be solved at all until possibly 8.18.0, right? The best solution would be to have something working with both Dune and coq_makefile, and there won't be backports.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:19):

There is also the question of whether transifitive deps should be on by default or not, in the OCaml community there is a lot of discussion about this topic.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:19):

Karl Palmskog said:

but I think this can't be solved at all until possibly 8.18.0, right? The best solution would be to have something working with both Dune and coq_makefile, and there won't be backports.

This problem is independent of Coq's version.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:20):

As far as I can tell

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:20):

Coq Community project can provide a Makefile.local that installs the dep file

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:21):

True you can upstream that to Coq when you want, but IMHO it is a bit orthogonal, we are talking about saving a file coq-package that has:

(deps Theory_bar Theory_foo)

so that is easy enough

view this post on Zulip Karl Palmskog (Jun 25 2023 at 13:21):

ah, you mean something like that, sure. But often, we rely on widely-used projects like Std++, VST, etc., and all those projects would need to be persuaded to install (additional) metadata

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:22):

Yes they would need to install it, (or packages in opam could do it too)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:22):

But there is no way around that

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:22):

inferring that meta-data is too brittle, tho I'd be interesting if someone would like to write such a tool

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:24):

Still need to think more about it, but overcoming lack of metadata by going back to a model where all the namespacing is removed doesn't seem to enticing to me

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:24):

Lot's of new corner cases to handle

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:25):

And overall user experience is still bad

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:25):

If you use the flag, you lose quite a few nice things that 0.8 mode offers

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 13:25):

If you don't use the flag, you still need that bug fixed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 14:36):

Another unpleasant property is about the situation where a package not using the flag depends on a package using it.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 14:37):

Then the first package has to inherit the global scope of the first, that creates many problems, mostly by injecting a lot of spurious deps into the first one, which cannot rely on isolation anymore and thus will break a some point.

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 14:52):

@Karl Palmskog unless Coq 8.18 can infer the metadata from _CoqProject (which is fragile?), or projects migrate to dune packaging (harder), the extra metadata seems to be needed?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 14:57):

yes, if it's to be done properly with transitive deps, I don't see how it could be added for existing packages robustly. Many packages don't even use _CoqProject or the standard calls of coq_makefile

view this post on Zulip Karl Palmskog (Jun 25 2023 at 14:58):

the whole deal with everyone in the world declaring Ltac2 as a dependency because some project 10 levels down uses it in a proof is pretty annoying

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:05):

Agreed.
Re “should transitives deps be on by default”, “private” deps don’t exist in Coq AFAICT?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:06):

I think the closest is CompCert's bundling of things like Flocq (turned off in Platform)

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:08):

Ah, but if you depend on an installed package, your deps need it too — you can't statically link it...

Even using a private copy seems questionable, since definitional equality typically exposes internals.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:19):

I don't see how it could be added for existing packages robustly.

It seems to me that such packages could install a coq-package file? Why that would not be robust?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:20):

I meant that we have a bunch of legacy packages out there, and seemingly all feasible solutions lead to some kind of multi-year effort to get new releases to contain the required metadata, and the metadata never being added for old packages

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:21):

you could approximate dep data from opam packages I guess: look at logpath of all opam dep packages

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:22):

but this data is incomplete and sometimes inaccurate for existing packages in the Coq opam archive

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:22):

Packagers can update meta-data without having to do a new release, but indeed, there is some adjustements to be made, meanwhile the missing meta-data needs to be specified or inferred somehow.

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

Old packages are not likely to use (lang coq 0.8) to start with tho, so I'm unsure I can understand that scenario with "old packages"

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:24):

the idea is that, likely forever, packages with (lang coq 0.8) (and beyond) need to depend on coq_makefile-installed old packages. For example, MathComp packages are so compatible and stable they seldom need new releases

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:25):

Yes they do, and what is the problem?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:26):

I want to reach a point where I have a project with (lang coq 0.8) and don't need to declare a huge number of transitive (theories ...), many of which I get through legacy coq_makefile packages

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:27):

In your example with math-comp huge is equal to 1 tho

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:28):

what's an example of "huge"?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:28):

RegLang as an example uses MathComp but isn't in the mathcomp logpath

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:29):

I'd say 5-15 dependencies are not uncommon in research artifacts, and some dependencies may have several logpaths to declare

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:29):

when looking transitively, this could go to 10-30 dependencies

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:30):

Looking at Coq's CI your number seems quite high to me, in fact due to poor packaging and build tools, dependency use in the Coq universe is not so common, but indeed let's assume we have a package where N = 30

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:30):

And you want to reach a point where you don't have to write the trans dependencies

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:30):

How do you want to reach that point?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:30):

either by metadata being installed automatically or some flag

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:31):

metadata will happen (for Dune packages), now let's think of the flag, how would that flag work?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:32):

Dune packages are going to be tiny minority for foreseeable future

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:32):

flag is what we discussed above

view this post on Zulip Gaëtan Gilbert (Jun 25 2023 at 15:33):

What are the precise properties dune needs? I'm wondering if we can do something like giving coqc access to all user-contrib but coqdep only sees the explicit dependencies
Then if a direct dependency is not visible to coqdep we would need to make it produce an error

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:35):

Karl Palmskog said:

flag is what we discussed above

flag has a lot of bad properties so far, so I don't see how to implement the flag properly. In particular if the main gain for the flag so far is avoiding to add a couple of packages like Ltac2. But I'm happy for someone to come up with an specification of the flag, but that spec should include a complete spec for all possible combinations of packages in a workspace setting the flag differently.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:35):

Gaëtan Gilbert said:

What are the precise properties dune needs? I'm wondering if we can do something like giving coqc access to all user-contrib but coqdep only sees the explicit dependencies
Then if a direct dependency is not visible to coqdep we would need to make it produce an error

Dune Coq rules need to be reasonably simple and maintenable, that's the main point.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:36):

That solution seems to me like a lot of effort compared to the alternative (add the metadata)

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:36):

re Gaetan's proposal, that as is would break too — if I depend on A, and A depends on Z, I want to be able to Require things from Z directly...

but maybe I see an automatic alternative: if building A loads Z, then coq_makefile could add Z to the metadata?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:36):

I think the problem is not adding Ltac2 itself, but having to change the (theories ..) every time one of my deps changes a dep (or their deps adds a dep, etc.)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:37):

coq-lsp 0.2 will have better capabilities in this regard, it doesn't even need coqdep, but that's at the cost of a much deeper integration (in the line @Gaëtan Gilbert ) points out

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:37):

@Karl Palmskog that option is bad, sure, the question is if adding the metadata in packages would be so bad

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:37):

Karl Palmskog said:

I think the problem is not adding Ltac2 itself, but having to change the (theories ..) every time one of my deps changes a dep (or their deps adds a dep, etc.)

Then have the dep declare their deps in their metadata, what is the problem with that?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:38):

again, only a tiny minority is going to be using Dune. If coq_makefile is not onboard, we get the nightmare (in my view)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:38):

Paolo Giarrusso said:

re Gaetan's proposal, that as is would break too — if I depend on A, and A depends on Z, I want to be able to Require things from Z directly...

but maybe I see an automatic alternative: if building A loads Z, then coq_makefile could add Z to the metadata?

I think Gaëtan proposal is very interesting but indeed there is lots of questions open, that's why I chose to do a "zero-config" build approach in coq-lsp which is a more experimental and coupled setup.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:39):

Karl Palmskog said:

again, only a tiny minority is going to be using Dune. If coq_makefile is not onboard, we get the nightmare (in my view)

Then have coq_makefile be on board?

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:39):

Karl: nobody's assuming a migration to dune, just adding the metadata file by hand wherever needed

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:39):

I think?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:40):

Paolo Giarrusso said:

Karl: nobody's assuming a migration to dune, just adding the metadata file by hand wherever needed

Yes, all you need is to install a coq-package file, coq_makefile I think has support already to install extra files.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:40):

coq-package or whatever name you want, in the end it is just a file with a bunch of fields, so sexp or json would work.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:40):

or even META format

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:40):

is the problem is that Karl himself has to add the metadata for half of coq-community? I can imagine that being a nontrivial amount of work?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:40):

getting manual changes like this just into all Platform projects is likely going to take >= a year

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:40):

I think that's not so importnat

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:41):

Karl Palmskog said:

getting manual changes like this just into all Platform projects is likely going to take >= a year

Well we have dune universe working with most of the platfrom and took us more like an afternoon, but indeed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:41):

there is no free lunch

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:42):

only realistic option (in my view) is to try to get metadata installation into, say, coq_makefile in 8.18.0 or 8.19.0

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:42):

@Karl Palmskog you are pointing out the pain with adding the metadata, but I wonder how you are assesing the pain of the "flag" solution

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:42):

because the pain of the flag solution is _at least_ 3 orders of magnitude more

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:42):

at least the flag was a local change and not some social engineering project

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:43):

in truth the costs seem on different sets of people

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:43):

Not only that, the costs are wildy different

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:43):

as in a very complex set of rules vs adding a file with a bunch of names

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:44):

that even a person that doesn't know how to program can do it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:44):

on the other side working with the Dune API seems to be challenging (which I think is not, but indeed ppl get intimidated?)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:45):

and moreover you have a very complex rule setup, still noone answered to a few key questions about semantics I posed above

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:45):

I'm surprised "let Coq use user-contrib as it used to" can be that expensive, but mostly both estimates are biased by "who must do the work"

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:45):

Karl Palmskog said:

only realistic option (in my view) is to try to get metadata installation into, say, coq_makefile in 8.18.0 or 8.19.0

Why do you need to modify coq_makefile for this?

coq_makefile already supports installing an extra file

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:46):

we can realistically make Platform projects include these files, again with a >= year timeframe. Other projects outside Coq-community are not going to do this

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:46):

Paolo Giarrusso said:

I'm surprised "let Coq use user-contrib as it used to" can be that expensive, but mostly both estimates are biased by "who must do the work"

Just writing out the semantics is a multi-day project.

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:46):

but I do agree that "one year" is not a lower bound — "add one line per package" seems easy enough to crowd-source

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:47):

@Emilio Jesús Gallego Arias it sounds like you want sth saner than what dune has done before coq-dune 0.8, but that's not an axiom?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:47):

Karl Palmskog said:

we can realistically make Platform projects include these files, again with a >= year timeframe. Other projects outside Coq-community are not going to do this

Why projects outside of Coq community would refuse to add meta-data?

Why would it take more than a year to add a bunch of coq-package files?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:47):

because most maintainers don't care, they don't use Dune

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:48):

this can be done centrally in the opam packages

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:48):

Karl Palmskog said:

because most maintainers don't care, they don't use Dune

How have you gathered this "interest" data?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:48):

Most is here what, like 51% ? 80% ?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:48):

just trying to make people do tags/releases fails most of the time

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:49):

Paolo Giarrusso said:

Emilio Jesús Gallego Arias it sounds like you want sth saner than what dune has done before coq-dune 0.8, but that's not an axiom?

I don't see how packages setting the flag and those not setting the flag can work together in a sane way.

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:49):

we now have the Platform where people are at least incentivized to do releases

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:49):

Karl Palmskog said:

just trying to make people do tags/releases fails most of the time

well if upstream of your dependency doesn't want the dependency used, it seems quite futile to me to try to use that depedency?

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:50):

I'd say my fail ratio for asking for release for non-Platform project is like 80%

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:50):

Emilio: yeah, nobody's asking for sane behavior :-)

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

Karl Palmskog said:

just trying to make people do tags/releases fails most of the time

I agree in the sense that as of today, a lot of processes in the package maintance setup require a lot of manual action. This is recipe for disaster.

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:50):

but also, you'll only get the "good" behavior if all your deps add metadata

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:51):

Paolo Giarrusso said:

Emilio: yeah, nobody's asking for sane behavior :-)

Well that's a very personal opinion, but the main motivation for me to work is Dune is to use it for my own projects, so I do want my build system to be sane.

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:51):

this [good behavior only if everyone adds metadata] is why, if metadata installation could be automated and part of coq_makefile make install, it may succeed

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:51):

Paolo Giarrusso said:

but also, you'll only get the "good" behavior if all your deps add metadata

Yes. If your deps are not willing to collaborate with you to add a one-line file, then IMHO you have bigger problems

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:51):

Emilio: sure, so you just need all your deps to add the metadata and your build system will be sane

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:52):

Karl Palmskog said:

this is why, if metadata installation could be automated and part of coq_makefile make install, it may succeed

sure, that'd be great, but not a required thing

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 15:52):

Paolo Giarrusso said:

Emilio: sure, so you just need all your deps to add the metadata and your build system will be sane

my build system is still sane if it doesn't have the metadata. It is now that the user will have to provide the missing metadata

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:52):

however, while Karl maintains coq-community and knows it best, I'm surprised that so many packages get actual users

view this post on Zulip Karl Palmskog (Jun 25 2023 at 15:53):

we get users, but in many cases not sanely. People do things like make install from Git repo, then go on their merry way

view this post on Zulip Paolo Giarrusso (Jun 25 2023 at 15:58):

what about sth like this?

but maybe I see an automatic alternative: if building A loads Z, then coq_makefile could add Z to the metadata?

more precisely, you'd need to learn Z's base-path using Z's meta-data — but that's just to be the logical path you're building, so basically logpath

view this post on Zulip Karl Palmskog (Jun 25 2023 at 16:01):

I agree, but this assumes logpath exists and is accurate, which is not the case for many opam packages (but is for a large fraction, at least)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 16:08):

Paolo Giarrusso said:

Emilio: sure, so you just need all your deps to add the metadata and your build system will be sane

Note that my definition of sane here is "works correctly", which is not the case with the hack. In fact we have https://github.com/ocaml/dune/issues/7909 which turns out it is already pretty hard to fix due to some packages declaring (lang coq ) < 0.8

view this post on Zulip Emilio Jesús Gallego Arias (Jun 25 2023 at 16:09):

I still couldn't figure out a sane semantics for the fix

view this post on Zulip Karl Palmskog (Jun 26 2023 at 10:56):

Emilio Jesús Gallego Arias said:

Karl Palmskog said:

just trying to make people do tags/releases fails most of the time

I agree in the sense that as of today, a lot of processes in the package maintance setup require a lot of manual action. This is recipe for disaster.

in many cases, the barriers are not technical. For example, before the Platform, there was no way we were getting releases of Iris, even with flawless packaging/distribution. Now there are packages like VST Iris.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 26 2023 at 11:02):

I agree, there seem to be important cultural challenges in the Coq ecosystem.

Tho I rarely see technical or cultural issues in this context as non interdependent.

view this post on Zulip Karl Palmskog (Jun 26 2023 at 11:07):

if you solve something in the tooling, and people migrate to that tooling by default, there may be no need to do costly social engineering exercises like proposing metadata PRs to people who don't care. Those kind of tradeoffs are crucial to consider in my view.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 26 2023 at 11:13):

I'm afraid I can't understand how doing a PR that add dependency meta-data is:

Can you extend a bit on what makes it so challenging?

Also, how can tooling solve packages missing dependency meta-data? So far this remains mostly a manual process (which is often aided by linters, but I don't know of a language where this is fully solved by tooling)

view this post on Zulip Karl Palmskog (Jun 26 2023 at 11:14):

a majority of PRs I submit to Coq projects outside coq-community and mathcomp are not merged, or even commented on, even when they fix trivial things like enabling to build with latest Coq

view this post on Zulip Emilio Jesús Gallego Arias (Jun 26 2023 at 11:14):

But yes I agree that of course if tooling can solve a problem and in the process avoid a costly social engineering exercise of course we should try to solve the tooling (provided the cost of the tooling is not hugely more than the cost of the exercise)

But I have to admit I fail to see how this is the case here.

For coq-universe, in a couple of hours we were done, not only with the metadata, but with the full missing build specs which are way more challenging

view this post on Zulip Emilio Jesús Gallego Arias (Jun 26 2023 at 11:16):

Karl Palmskog said:

a majority of PRs I submit to Coq projects outside coq-community and mathcomp are not merged, or even commented on, even when they fix trivial things like enabling to build with latest Coq

Why is that?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 26 2023 at 11:16):

Karl Palmskog said:

a majority of PRs I submit to Coq projects outside coq-community and mathcomp are not merged, or even commented on, even when they fix trivial things like enabling to build with latest Coq

Why is that?

view this post on Zulip Karl Palmskog (Jun 26 2023 at 11:17):

probably because authors don't care, they put up repos for other reasons than maintaining a project

view this post on Zulip Karl Palmskog (Jun 26 2023 at 11:17):

they also have their own way of handling building in many cases, sometimes even without coq_makefile

view this post on Zulip Rodolphe Lepigre (Jun 26 2023 at 11:24):

No answer to PRs basically mean that these projects are dead right? In which case, who cares about porting them to more recent Coq / build infrastructure?

view this post on Zulip Karl Palmskog (Jun 26 2023 at 11:55):

other people may depend on these projects, and the authors might get around to making a release eventually due to some paper. PRs take time to review, and if they bring no obvious benefit they might be ignored or closed for this reason. "This PR helps people who use Dune depend on your project" is not really a convincing sell

view this post on Zulip Karl Palmskog (Jun 26 2023 at 11:59):

if we count "no answer to PRs" as sufficient for a project being dead, shouldn't this include Coq itself? How many PRs are bot-closed without any comment? From what I remember, strictly positive.

view this post on Zulip Rodolphe Lepigre (Jun 26 2023 at 12:00):

Not any reasonable issue or PR I would think.

view this post on Zulip Rodolphe Lepigre (Jun 26 2023 at 12:01):

Personally, I would not depend on any project that does not have at least a minimal amount of activity.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 26 2023 at 12:22):

Certainly Coq would have no problem merging such a PR

view this post on Zulip Paolo Giarrusso (Jun 26 2023 at 17:51):

FWIW, in the Haskell world adding such metadata to the opam package does NOT require author/maintainer consent — Hackage trustees can do it, and Karl would clearly qualify

view this post on Zulip Karl Palmskog (Jun 26 2023 at 18:06):

even if we wanted to do it, we can't add dependency metadata centrally with good accuracy using current tools

view this post on Zulip Karl Palmskog (Jun 26 2023 at 18:09):

and unless it can be done nearly-automatically and accurately, it's not worth the (human) effort, since the Dune userbase in Coq community is tiny

view this post on Zulip Karl Palmskog (Jun 26 2023 at 18:13):

as per above, if the format is agreed on and specified, we may be able to add metadata incrementally to Platform projects within a year or two, and majority of Coq-community projects in same timeframe. And that is for new releases only. I don't see anything else happening.

view this post on Zulip Karl Palmskog (Jun 27 2023 at 15:50):

I thought about the implications for Coq-community, and what I arrived at is that the only sane thing to do is to:

The alternative is to have released packages that break anytime a transitive dependency (within the transitive opam ranges) changes.

view this post on Zulip Karl Palmskog (Jun 27 2023 at 16:53):

here is an example of how things will break:

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 16:59):

But if you don't rely on transitive deps, it seems you have the opposite problem if coq-bar adds a dependency?

It seems here coq-foo should depend on coq-quux directly if and only if it has direct requires. And enforcing this requires discipline, or adapting coq+dune to allow machine-checking.

view this post on Zulip Karl Palmskog (Jun 27 2023 at 17:00):

yes, a similar problem will happen if coq-bar does a release that depends on both coq-quux and coq-baz

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 17:02):

But if transitive deps work and you list directly everything that you import yourself, all dependency changes would work.

view this post on Zulip Karl Palmskog (Jun 27 2023 at 17:02):

I don't see how this can be solved without changing Dune, or not relying on Dune-Coq >= 0.8. If I don't add the Quux in (theories Bar Quux), my project doesn't build with Dune-Coq 0.8. This is the only place I'm forced to record this transitive dependency.

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 17:03):

Is Quux needed even if you don't use Quux directly?

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 17:04):

And it seems opam deps have similar problems today if you rely on sth that you only depend on indirectly?

view this post on Zulip Karl Palmskog (Jun 27 2023 at 17:04):

it's needed by the Dune build. The Dune build with Dune-Coq 0.8 will say the following without the Quux in (theories Bar Quux):

Error: Cannot load Quux.X: no physical path bound to Quux

... when my project loads something from Bar that depends on Quux.

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 17:05):

Ah, so there are two separate problems, and only one would be fixed if transitive deps worked.

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 17:06):

(IIUC!)

view this post on Zulip Karl Palmskog (Jun 27 2023 at 17:07):

hm? If we could somehow magically know the transitive deps ofcoq-bar, it would suffice to write (theories Bar) in dune in coq-foo. Then, the release of coq-foo would be oblivious to the new coq-bar dropping its dep on coq-quux/Quux

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 17:08):

That breaks if coq-bar drops the dependency but you had a direct require, I think

view this post on Zulip Karl Palmskog (Jun 27 2023 at 17:08):

sure, if you had some From Quux ... in coq-foo, then yes. But I assume this is not the case in the above.

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 17:09):

Yep, we're describing distinct but "kind-of dual" scenarios

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 17:09):

Said otherwise: if a dep is only "declared transitively" (Foo depends on Bar, and Bar depends on Quux, but Foo does not depend on Quux directly), Foo should be able to Require Bar, and that should load Quux, but a direct Require Quux in Foo should fail.

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 17:10):

and I've never seen the ingredients for such a semantics in Coq?

view this post on Zulip Paolo Giarrusso (Jun 27 2023 at 17:12):

Also, opam deps do not have this semantics and can cause such breakage — have you seen this in practice Karl?

view this post on Zulip Karl Palmskog (Jun 27 2023 at 17:12):

I would be fine with a scenario where I theoretically could do From Quux in coq-foo and not fail, if it allowed me to skip the Quux in (theories Bar Quux)

view this post on Zulip Karl Palmskog (Jun 27 2023 at 17:13):

yes, I see things break due to unrecorded opam deps that were included transitively from time to time, can't recall a specific example

view this post on Zulip Karl Palmskog (Jun 27 2023 at 17:14):

but at least that is easy to fix at opam level: just add the dependency package explicitly

view this post on Zulip Emilio Jesús Gallego Arias (Jun 28 2023 at 09:07):

Paolo Giarrusso said:

That breaks if coq-bar drops the dependency but you had a direct require, I think

That's exactly the problem that happens in OCaml and the reason Dune added (implicit_transitive_deps false), as sometimes users of a library found themselves using a library that was pulled transitively, then the dep dropped that library, and the build breaks.

I think I have a model where this can be avoided (making the transitive deps "private") but that's out of scope for (lang coq 1.0) , and in fact I bet there are some open problems that would require research.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 28 2023 at 09:07):

I'm unsure what the current state-of-the-art on this is

view this post on Zulip Karl Palmskog (Jul 04 2023 at 08:41):

I wrote a summary of my view of Dune-Coq 0.8 use in Coq-community: https://github.com/coq-community/manifesto/issues/87#issuecomment-1619803762

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:00):

Note that implicit transitive devs is a model that is not problem-free, so in this sense both models are similar: changes in the dependencies of a dependency can break upstream users; while people tend to view the transitive breakage as more acceptable, for me both problems stand on equal footing.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:01):

They are really dual: when no implicit transitive deps packages break when a library add a dep, when implicit packages break when a library removes a dep.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:01):

So often does that happen is open actually.

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:02):

I think implicit transitive deps have a long history, e.g., it's implied by Parnas 1971, p. 2:

We now consider making a change in the completed system. We ask, "What changes can be made to one module without involving change to other modules?" We may make only those changes which do not violate the assumptions made by other modules about the module being changed. In other words, a single module may be changed only while the "connections" still "fit". Here, too, we have a strong argument for making the connections contain as little information as possible.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:07):

Yes they have a long history, as explicit ones do I guess. But breakage happens in both, just pointing that out, as implicit transitive deps are no silver bulltet either (and this is why dune supports disabling them and some industrial users need that functionality)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:08):

I guess it is often the case that deps evolution tend to be additive, and we have internalized that, so we prefer implicit as they break on removal but are robust w.r.t. addition. Tho, when you have deps conflicts for example that's a mess (and it has happen often in OPAM actually)

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:08):

but why not support both models in Dune-Coq then? My view is that I can usually fix breakages with implicit deps by updating opam package metadata. But I'll need to make (possibly conditional) source patches to fix breakages with explicit transitive deps

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:08):

That is one of the reasons dune is gaining opam functionality as we speak now, so it is aware of forward-conflicts

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:09):

Sure we do support both models in Dune

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:09):

What we don't have is installed packages recording their deps yet

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:09):

Karl Palmskog said:

but why not support both models in Dune-Coq then? My view is that I can usually fix breakages with implicit deps by updating opam package metadata. But I'll need to make (possibly conditional) source patches to fix breakages with explicit transitive deps

How can you fix an implict dep breakage with opam metadata?

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:10):

by updating bounds or adding a dep

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:10):

The dep needs to be added in the dune file, if a dep of your binary was using Yojson for example, but didn't declare it, and relied on a dep to declare it, you need to patch the dune file.

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:10):

the typical breakage is that an implicit transitive dep is not installed, so make sure it gets installed

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:11):

Using bounds would work for both implicit and explicit

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:11):

Karl Palmskog said:

the typical breakage is that an implicit transitive dep is not installed, so make sure it gets installed

That fixes nothing because dune won't see the dep regardless if it is installed or not as it provides isolation.

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:11):

I view this from an opam archive maintainer view. I have a bunch of released packages, and I want them to continually build

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:11):

Yes, from that point of view you have the same problem with explicit and implicit

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:12):

The only difference is that one model breaks when deps are removed, the other when deps are added

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:12):

and I guess this latter case is very common

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:12):

the example breakage I gave in the summary can't be fixed by opam archive metadata

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:12):

but implicit transitive deps that go missing can be fixed

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:12):

They cannot

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:13):

how can they be?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:13):

if you do (libraries lwt)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:13):

and lwt drops their yojson dep which you need

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:13):

if I turn an implicit dep into an explicit dep, the dep will always be installed and coqc will find it

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:13):

then you need to update to (libraries lwt yojson)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:14):

No, coqc will not find it

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:14):

unless you don't have deps, then of course when you don't have deps lots of stuff can happen

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:15):

if I put the implicit dep under depends in the opam package, it gets installed in user-contrib. Then coqc finds it

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:15):

You are talking about a model where there is no library scope

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:15):

That model is a dep-less model

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:15):

Not a model with implicit vs explicit deps

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:16):

I'm talking about the implicit vs explicit model as implemented by Dune for OCaml and Coq

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:16):

The dep-less model has many other problems actually, but these do belong now to opam not to dune

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:16):

indeed, but that's a pretty bad property I'd say

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:17):

as you get way less static guarantess from your build / CI

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:17):

but we are dealing with reality here: tons of packages will be installed with coq_makefile in user-contrib for the foreseeable future

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:17):

as you lack dep isolation your package is vulnerable to all global side-effects

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:17):

as you lack dep isolation your package is vulnerable to all global side-effects

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:17):

Karl Palmskog said:

but we are dealing with reality here: tons of packages will be installed with coq_makefile in user-contrib for the foreseeable future

Yes, we are dealing with that. And what's the problem again?

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:18):

the problem to me is that Dune-Coq 0.8 is unusable for long term packaging of releases

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:19):

That's what you think, but:

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 10:21):

Would it be more productive to focus on 0.9 with implicit transitive deps?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:22):

So once implicit transitive deps work (which they will soon) it'd be an illusion to think that will solve long-term package maintenance challenges

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:22):

Paolo Giarrusso said:

Would it be more productive to focus on 0.9 with implicit transitive deps?

Implicit transitive deps are already in 0.8, what it is missing is the meta-data from installed packages in user-contrib

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 10:23):

That's what I should have said then.
And it's likely deps are added more often than removed, so it seems this "illusion" will be closer to reality?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:24):

Maybe, I don't have enough data. All that I know is that implicit transitive deps created large breakages in opam

view this post on Zulip Karl Palmskog (Jul 04 2023 at 10:24):

what it is missing is meta-data from installed packages in user-contrib

as said elsewhere, I think this is 1-3 years away from happening in a meaningful way (if at all), and will likely leave old packages / Coq versions hanging

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 10:24):

I don't recall the specific issue, but a popular library dropped a dep, and basically all depending packages had to be patched.


Last updated: May 25 2024 at 21:01 UTC