Stream: Dune devs & users

Topic: Dune-Coq 0.3 dependency model


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

It's common to distinguish software functionality from "black box" perspective on one hand and from the perspective of internal details on the other. My view of Dune-Coq 0.3 as black box (when theories is omitted from all dune files) is that it leaves all dependency management to Coq (and implicitly package managers/systems like opam or Nix). I think this is closely analogous to what coq_makefile does. From a purely black box perspective, how is this broken?

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

That's broken as long as you use theories, if you don't use theories then it works, but you have 0 package management.

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

So 0.3 lang as specified is broken, a subset of it may be sane

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

I have zero package management within Dune, but I can have lots of package management outside Dune

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

Specifically, vendoring is broken. Also, dune caching isn't sound.

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

specifically, caching won't recognize changes in user-contrib; if you reinstall packages you'll need to disable caching/wipe your cache.

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

However, that's only broken in those specific ways, so I understand why it might be a better tradeoff for packagers than 0.8. Not sure it's better for users.

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

how many projects need advanced Dune caching? Seems to me those that do can set up fancy tooling around it

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

Yes @Paolo Giarrusso the model is very broken

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

Karl Palmskog said:

how many projects need advanced Dune caching? Seems to me those that do can set up fancy tooling around it

all projects do benefit from caching, for example for CI, moreover here is a soundness problem so that affects every project as it can lead to incorrect builds

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

if your build takes like 30s or even a minute, the caching benefits are very modest, and you are waiting for CI/reviews anyway in a "modern" workflow

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

Don't know how many projects build that quickly — and in CI iris takes ~20 minutes since it rebuilds deps

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

"a team of full-time devs on a large codebase" (Bedrock Systems) might be the scenario that benefits most from caching, but I'm not sure that's the only one. Especially if you have client libraries, and breaking changes to port clients to.

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

Nix-based CI can cache packages easily, I think the question is how many projects get significantly helped by local Dune caching on top of dep package caching. In Coq-community, I'd say "not many"

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

and re soundness, I'm not sure this can really cause incorrect builds that succeed when they shouldn't. It can only cause spurious failure from coqc, that are clearly identified as requiring a cache wipe.

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

right, doesn't .vo dep hashes prevent soundness bugs?

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

Paolo Giarrusso said:

and re soundness, I'm not sure this can really cause incorrect builds that succeed when they shouldn't. It can only cause spurious failure from coqc, that are clearly identified as requiring a cache wipe.

@Paolo Giarrusso I mean build system soundness, the statement of that property is actually "the build is free of wrong hash coqc errors"

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

That's a big PITA, imagine you do a 20 min build just to discover the build is useless

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

Re coq-community: CI caching might be negligible, but local caching seems still useful — as soon as you have two branches

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

In any case, I think emotional terms like "broken" aren't helpful, and the OP "is this broken" is potentially about semantics. OTOH, there are probably relevant concrete questions?

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

I only used "broken" since it was used in the motivating comment. You can reformulate to "why not just continue using coq_makefile + opam dep handling" or similar

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

you lose both caching and _vendoring_, so it's not acceptable long-term for dune — to me the only options are if and when it should be actually removed.

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

And you (Karl) might be arguing for keeping 0.3 around at least until "0.9" comes up with transitive deps for user-contrib? But just guessing.

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

I don't see how a 0.9 like that, if it happened, would help the big picture, since likely the majority of projects would still be on coq_makefile without much in the way of incentives to switch (caching and vendoring is not much of a draw for most)

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:05):

so you need 0.9 + extending coq_makefile to record deps before then? And I guess you'd like help with the missing metadata? What exactly is required to avoid regressions?

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

if we'd like people to use Dune for Coq projects (Dune-Coq >= 0.8), there needs to be a way to produce dependency metadata for legacy packages using old Coq versions, and I don't see any way to do this accurately. The alternative is to get this stuff [producing dep metadata] into both coq_makefile and Dune and wait maybe 3-4 years

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

a nightmare would be if projects have to choose between Dune in their releases and being compatible with 1-2 Coq versions back. Another nightmare is if people have to look up whether their dep package gets the proper metadata

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:15):

"wait 3-4 years" is speculative and debated, so I'd suggest "wait until X happens"

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:16):

Emilio seems to think X is easy, so if you and Emilio can agree on X, people can help with it.

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

we can go by the Coq release schedule. Many projects are maybe 2 versions behind the latest Coq version, and they'd like to be compatible with 2 versions back. That's two years. If we can say to a maintainer of such a project, you can use Dune >= 0.8 and not have to worry about any transitive deps, regardless of what deps you have, then I'd be happy to recommend it

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

but I think it would be a miracle if we solve the metadata issue with coq_makefile for 8.18, so this would leave 8.19 as the earliest one

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:20):

if the Makefile.coq.local approach works, it'd work for quite a while back. If you want to reduce duplication, you could add support tooling in a separate package.

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

this would trigger my second nightmare, forcing maintainers to manually look up whether their prospective dep produces the required metadata

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

mixing packages that produce transitive dep metadata and those that don't seem like a recipe for disaster, possibly worse than having no metadata

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:25):

(Even "provide a forked and renamed coq_makefile as a separate package" could be an option, I've done it internally for coqdep, tho I can see questions)

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:27):

but what's the disaster? Are there packages that support dune only and would break? (Guess not?) Or packages that support dune 0.3 and would break with 0.8 because they depend on coq_makefile ones? How many?

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

if you are mixing packages with dep metadata with those that don't (possibly different versions of the same package) I think the only safe route is to specify full transitive deps, only more confusing

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:29):

but I am asking if such packages exist

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

to my knowledge, they don't exist, because as of yet nobody has used Dune-Coq >= 0.8 in a released package

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:30):

I'm talking of 0.3

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:31):

0.8 is out, if people mind its semantics they just won't start using it, no problem.

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

I think nearly all 0.3 released packages would break if they were "forced" into 0.8, since they don't use (theories ...)

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:32):

let's ignore 0.8, and assume dune starts installing its own metadata in 0.9.

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:33):

then, packages could migrate from 0.3 to 0.9 adding their direct dependencies to theories (ideally, including the transitive ones they use directly, but that's not machine-checkable today)

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

OK, but then unless changes are made to coq_makefile, you'd have to manually look inside each of your deps to see whether they use 0.9 or not (to ensure you're not specifying transitive-only deps that might break your build)

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:34):

_if_ they have deps that use coq_makefile or dune 0.3. (Dune 0.8 could still install metadata).

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:36):

and I am asking, do such projects exist, and how common they are?

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

Dune-Coq 0.3 projects that use coq_makefile deps? Probably all released packages that use Dune-Coq 0.3 do this

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:41):

judging roughly by coq-released, it seems we're talking of... 38 packages (was 20 ~2 years ago).

$ for i in opam-coq-archive/released/packages/*; do if grep -r -q dune $i; then echo $i; fi; done|wc -l
      38

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:42):

I hope @Emilio Jesús Gallego Arias agrees Dune-Coq 0.3 shouldn't be dropped till at least those packages are ported.

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

but I don't think those particular legacy package are all that relevant. Isn't the point to have people switch to Dune from coq_makefile? Currently, I don't think we have a case for convincing anyone but those for whom caching and vendoring are important and can live with transitive breakages

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:52):

unless coq_makefile is being deprecated, that doesn't seem as urgent, it could happen bottom-up, and it doesn't need to support all relevant Coq versions

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 11:53):

"we support Dune on Coq >= 8.8 and Dune-Coq on Coq >=8.18" would be perfectly reasonable

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

besides extraction, I personally want to use Dune because of the monorepo support (multiple subdirectories with dune file in separate package). If forking coq_makefile is on the table, would make more sense to me to fork Dune to get 0.3 + monorepo when 0.3 disappears

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 12:24):

0.3 + monorepo = 0.3, IME

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 12:27):

0.8/0.9 also supports Coq Universe's model where separate packages can be assembled into a monorepo-like thing or distributed independently.

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

yes, but the idea is that I want to continue to use the 0.3 dep model, and the main motivating example where I can't just "switch back" to coq_makefile is for monorepos

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 12:28):

you prefer that even compared to 0.8 + transitive deps?

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

prefer forking Dune? It seems preferable over transitive deps or coq_makefile with several levels of recursive make calls

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

should be feasible to just add back the 0.3 code

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

maybe it can be done as one of theose plugins that we sometimes hear about

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 12:31):

at least, you can EDIT: could build dune 3.7.x into dune-other indefinitely if you want EDIT: to maintain it yourself

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 12:31):

but I'm confused

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 12:32):

by "0.8 + transitive deps" I'm assuming transitive deps work transparently with the changes you asked for

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 12:32):

so they'd work exactly like in opam

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

my estimation for transitive deps being included consistently with packages is 3-4 years, so the question is what to do between the time when 0.3 is removed and metadata is universal

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 12:35):

keep 0.3 around until there's "enough" metadata

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

that would be reasonable to me, but would @Emilio Jesús Gallego Arias agree to keep 0.3 around for (potentially) that long?

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 13:02):

that's my question, but you probably need to refine "enough"

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 13:03):

I also suspect a CEP is warranted (IIRC @Théo Zimmermann has recently suggested such things for changes _outside_ Coq proper?), also to summarize the migration strategy for packages

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

the CEP could outline what coq_makefile needs to do to provide the metadata

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 13:05):

but yes, I think we must tie migration and removal of 0.3 somehow — and if porting away from 0.3 is as easy as @Emilio Jesús Gallego Arias has claimed, great. If not, at least incentives are better aligned.

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 13:07):

Otherwise, conflict seems inevitable, since this is trading work by Dune maintainers with work by coq-community maintainers.

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

my view is that Makefile.coq.local approach for metadata isn't practically feasible, not least because there are few incentives for anyone to do it

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 13:09):

if you want to use dune, you have incentives to provide this for your deps, or carry the transitive deps.

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

but if you need Makefile.coq.local, you are already using coq_makefile and likely don't care about others using Dune or not, even your reverse deps

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

if you're using Dune, my reading is that Emilio already committed to getting metadata generation into some near-future version

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 13:12):

a CEP would help nudge people for "yes accept this patch", and if maintainers are unresponsive then opam-coq-repository packagers can step in.

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

I doubt users or maintainers care about CEPs, but sure, if it's done as part of some general process such as Platform, at least Platform maintainers may accept patch

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 13:16):

and other maintainers haven't committed to any maintenance anyway

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 13:27):

Meanwhile, 0.8 lets one a single dune build support both vendoring and not vendoring; I think my dune submission to Iris failed because 0.3 fails on this basic property https://gitlab.mpi-sws.org/iris/iris/-/issues/471

view this post on Zulip Paolo Giarrusso (Jul 04 2023 at 13:28):

(hmm, that discussion is long and I'm not sure it'd convince you of my analysis)

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

It wasn't my intention to use "broken" in an emotional way, I just meant that indeed the 0.3 model does produce unsound builds, as it doesn't track deps in user-contrib, so that means that you have your project, you do opam update && dune build and you get a bad build, and you need to discard your cache, etc... that's a pretty bad user experience.

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

I'll use "unsound" from now on (hopefully is more technical)

view this post on Zulip Karl Palmskog (Jul 05 2023 at 08:59):

@Emilio Jesús Gallego Arias so any thoughts on a possible CEP on the metadata issue for 0.8 and whether 0.3 will be around until metadata is generated by both coq_makefile and Dune? As per Paolo's analysis, we have around 30 packages using Dune-Coq 0.3 (and more using it in CI in Coq-community), so some kind of roadmap, if not commitment, would really be nice

view this post on Zulip Karl Palmskog (Jul 05 2023 at 09:02):

even a simple statement from the Dune-Coq team along the following lines would be extremely useful for me as Coq-community maintainer:

we will try to develop a metadata format for installed packages usable by both Dune and other Coq tools such as coq_makefile, and we won't remove Dune-Coq 0.3 until such a format is widely used

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

@Karl Palmskog , I will indeed open a PR to Dune soon adding support for metadata. I was thinking of discussing the format on the PR , as it seems pretty simple, but happy to do a CEP if that's needed.

Due to non-technical reasons (resources) I cannot make any statement about 0.3 support, unless someone would like to maintain that mode, the current policy is:

Thus projects that rely on 0.3 will have to add at some point an upper bound with Dune, maybe that will happen when Dune 4 is released.

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

Adding the upper bound is a big PITA, but we'll have to work on that.

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

I agree with you that it is early to recommend 0.8

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

It is great all the testing you did, more than great, essential, but we need to fix the metadata problem and a couple of other minor problems.

view this post on Zulip Karl Palmskog (Jul 05 2023 at 17:21):

the point about the CEP to me would be to ensure that someone is willing to do and/or review work to do the metadata for coq_makefile. Dune projects are currently in a small minority in the Coq Platform and the Coq opam archive, which means even Dune people will want to depend on non-Dune/coq_makefile projects smoothly.

view this post on Zulip Karl Palmskog (Jul 05 2023 at 17:24):

I can help with drafting a CEP if bandwidth for this is a problem

view this post on Zulip Karl Palmskog (Jul 05 2023 at 17:55):

if semantics of composing a project with 0.3 with a project with 0.8 is undefined, I suggest turning it off by default

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2023 at 18:33):

Karl Palmskog said:

if semantics of composing a project with 0.3 with a project with 0.8 is undefined, I suggest turning it off by default

Unfortunately this may not so easy to achieve, just trying to figure it out would detract resources needed for more prioritary things.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2023 at 18:36):

Karl Palmskog said:

the point about the CEP to me would be to ensure that someone is willing to do and/or review work on the metadata for coq_makefile. Dune projects are currently in a small minority in the Coq Platform and the Coq opam archive, which means even Dune people will want to depend on non-Dune/coq_makefile projects smoothly.

I see, thanks for the help offer. I was planning indeed to document in the PR how to add such metadata to coq_makefile, because actually we will need to add a test-case in Dune's test-suite there.

So I propose we wait for the PR, that will add the basic infrastructure and tests, we can then discuss the details of the file.

So far what I'm planning to do is very simple, Dune will read the metadata for a theory when a coq-package file is found.

The format of that file would be something like:

(coq-package-version 1.0)
(deps A B C)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2023 at 18:36):

Maybe we can add other fields

view this post on Zulip Karl Palmskog (Jul 05 2023 at 18:39):

how about at least adding:

(logpaths X Y Z)

Since some project install to multiple directories, and we can't trust logpath opam metadata

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2023 at 18:51):

Actually I was thinking that in that case we would be closer to Coq's semantics, so we would install two coq-package files (or maybe coq-theory ?)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2023 at 18:51):

Because the projects may install in multiple paths, but these paths may not share a common root

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2023 at 18:52):

Is that what you mean @Karl Palmskog ?

view this post on Zulip Karl Palmskog (Jul 05 2023 at 18:55):

I guess you could do that, sure. But then you'd want each coq-package to contain different (logpath X) entries to differentiate them?

view this post on Zulip Karl Palmskog (Jul 05 2023 at 18:56):

or do you mean the logpath prefix is already defined by the placement of coq-package?

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

I mean logpath prefix is now inferred by the placement of coq-package yes

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

But happy to hear about other options

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

We imitate what Coq does, we scan user-contrib + COQPATH, and we infer the logpath from the file structure

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

In the model where we don't install everything in the same tree, yes we want that metadata to contain logpath

view this post on Zulip Rodolphe Lepigre (Jul 05 2023 at 19:16):

I'm wondering: isn't this plan kind of reinventing the wheel? I proposed a possible scheme here a while ago, where we could just say that a Coq package is just a standard opam package (with its Coq-only, OCaml-only, and mixed-Coq-OCaml dependencies). Such a package, if it defines theories, would simply have a coq-theories folder in the lib directory for the package (as reported by ocamlfind), it this folder exists, it would then be directly added to the COQPATH when you have a direct dependency on the package.

Something like that does not require any additional form of metadata, and it would kill two birds with one stone, by setting a path to the complete annihilation of the user-contrib folder on the long run.

view this post on Zulip Rodolphe Lepigre (Jul 05 2023 at 19:19):

Patching coq_makefile to install the theories twice, once in user-contrib for compatibility, and also as described above should not be hard. And dune could be easily made to follow the same scheme. The installation scheme is independent from the build system, and closer to what exists for OCaml.

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

@Rodolphe Lepigre I don't think this plan is reinventing the wheel. We are working under different assumptions, that is:

But indeed once the compat assumption is dropped (likely for (lang coq 1.1) we will implement separate installation I think, but that will provide 1-way compatibility (projects using (lang coq 1.1) can't be used from coq_makefile anymore, unless indeed coq_makefile can find out the libs)

The topic of whether Coq should fuse with the build system is a very interesting one, which I'm exploring in coq-lsp / fcc.

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

Whether to reuse ocamlfind, is something that I've been wondering about, but the META format is too limited I think. At some point we had an issue to develop a coqfind binary, but that got discarded. I guess at this point dune will gain coqfind like tech, the idea is to put all this in a lib tho, that can be shared by dune, Coq, and coq-lsp/fcc

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

Also note that opam packages and ocamlfind packages are not the same

view this post on Zulip Karl Palmskog (Jul 05 2023 at 20:38):

we already have a non-opam packaging ecosystem in Nix, so tying things completely to opam should be avoided in my view

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2023 at 21:49):

I guess Rodolphe meant ocamlfind instead opam. The idea makes sense for (lang coq 1.1) IIUC, however I'm unsure META can handle what we need tho.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 05 2023 at 21:50):

Actually there are two ideas in his proposal:

Both IMHO make sense, however I think they are not possible for our 2-way compat goal in (lang coq 1.0) , in fact coq-lsp is already playing with idea 2

view this post on Zulip Paolo Giarrusso (Jul 06 2023 at 01:12):

"1.1 can't be used in coq_makefile" is the kind of statement that calls for a separate CEP; depending on coq_makefile patches and Coq > 8.Y is reasonable, but requiring patches to clients might be another matter depending on the patches.

view this post on Zulip Rodolphe Lepigre (Jul 06 2023 at 05:18):

Yeah, sorry, I did kind of mean ocamlfind packages indeed. However, I don't think I was suggesting to have Require handle deps (though that is an interesting idea). I was just thinking that coq_makefile would take a list of findlib packages to depend on in a variable, and that these would be handled exactly as potential plugins (with -I <LIB_PATH>), and adding a COQPATH extension with <LIB_PATH>/coq-theories/ (which might exist or not). In dune things would go the same way, except that the list of findlib packages depended on would be in some filed of the coq.theories stanza.

Essentially, if one would rsync all the <LIB_PATH>/coq-theories/ folders into lib/coq-core/user-contrib/, one would get the same thing as what is currently in user-contrib. This does not solve conflicts in having several packages defining the same theories, but that could be solved in a second step.

view this post on Zulip Rodolphe Lepigre (Jul 06 2023 at 05:22):

Also, how does my plan not handle theories dependencies? As long as we are fine with an "all or nothing" approach for a single ocamlfind package, I think that just works. If packages are too coarse-grained, they can be split into several, but that would need to be decided per-project. Or maybe I'm missing something?

view this post on Zulip Paolo Giarrusso (Jul 06 2023 at 07:20):

Symlinks rather than rsync might be quite a bit cheaper. But such changes to user-contrib seem hard to retrofit with Coq <= 8.17 — at least, harder than "add one file".

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

Rodolphe Lepigre said:

I don't think I was suggesting to have Require handle deps (though that is an interesting idea).

I inferred that from the post you linked "You could then interpret From lib_name Require some.module.path as running an ocamlfind query lib_name to search for the library path, and then search for the qualified module under that path."

That makes sense, but requires patching Coq.

I was just thinking that coq_makefile would take a list of findlib packages to depend on in a variable, and that these would be handled exactly as potential plugins (with -I <LIB_PATH>), and adding a COQPATH extension with <LIB_PATH>/coq-theories/ (which might exist or not). In dune things would go the same way, except that the list of findlib packages depended on would be in some filed of the coq.theories stanza.

That'd be great, but I'm unsure you can retrofit the needed meta-data in the META format; but if someone comes up with a proposal to extend findlib with Coq support I'd be very happy to have a look.

Note that still you need the META file record the deps for coq.theories.

view this post on Zulip Rodolphe Lepigre (Jul 06 2023 at 21:22):

I see, I was missing the fact that you still need to know the (strictly) transitive dependencies somehow.

Looking at the META man-page, it seems that the requires field could be used for that purpose.


Last updated: May 25 2024 at 20:01 UTC