[coq.dev] New upstream split package setup. #1923

ejgallego · 2021-11-07T22:20:29Z

This should work fine once coq/coq#15560 is merged.

From today, the canonical opam packages live in Coq's repository.

I'm not sure what the best way to keep them in sync is.

palmskog · 2021-11-08T14:34:50Z

@ejgallego can you say something about how this draft PR is related to #1801? I would prefer if we only have one draft PR related to splitting of coq.dev.

ejgallego · 2021-11-08T14:37:23Z

@ejgallego can you say something about how this draft PR is related to #1801?

It implements my suggestion there, tho I'm not sure we are properly testing coq-native in the CI here.

palmskog · 2021-11-08T14:39:32Z

Indeed, coq-native testing is yet another PR, #1504, that seems stuck. Maybe you want to include the changes from that PR here?

ejgallego · 2021-11-08T21:34:44Z

Thanks for the pointer @palmskog , let's see if that works.

gares · 2021-11-09T09:49:47Z

The other PR was stuck because I could not find a failing package to test it...

ejgallego · 2021-11-09T10:38:28Z

Indeed, seems the native + split + boot rules are broken, it is hard to test this stuff.

gares · 2021-11-09T19:26:31Z

Here CI fails because of a timeout, you should remove the two commits called "hack" (or at least the unimath one).

ejgallego · 2022-01-14T13:41:20Z

Note that I'm still planning to fix this, it is a bug in how I compute the path for native in Dune, so it could go on 2.9.2 as it'll be a one line fix (hopefully)

ejgallego · 2022-06-24T17:10:17Z

Split package will be upstream soon, this PR should be also good once that goes in.

RalfJung · 2022-06-29T11:26:25Z

Now that the Coq PR coq/coq#15560 landed, this is rather urgent. Right now, the coq.dev opam package is broken.

silene · 2022-06-29T11:36:52Z

Note that the pull request does not seem correct. For example, the depopts on coq-native is missing, as far as I can tell.

core-dev/packages/coq-core/coq-core.dev/opam

ejgallego · 2022-06-29T11:55:00Z

Yes I need to fix this, sorry. Give me a minute.

core-dev/packages/coq-core/coq-core.dev/opam

silene · 2022-06-29T12:17:01Z

bwrap: execvp ./configure: No such file or directory

ejgallego · 2022-06-29T15:24:39Z

I have no idea what is going on.

gares · 2022-06-29T16:09:35Z

In the logs (saved as artifacts) I don't find the line downloading the sources of coq-core, even if later is unpacks a tgz (which is maybe empty). The url stanza is gone, are we sure this change is OK?

gares · 2022-06-29T16:10:48Z

core-dev/packages/coq/coq.dev/opam

-url {
-  src: "git+https://github.com/coq/coq.git#master"
-}
+dev-repo: "git+https://github.com/coq/coq.git"


This looks fishy, and the same holds for the other packages. IMO this opam file is fine for opam install https://github.com/coq/coq but is not good for an opam repository

Oh yes, sorry I am not familiar with how this works, I'll amend. Does this mean that we can't share the same opam files for stable opam releases, coq master and coq-core.dev ?

Does this mean that we can't share the same opam files for stable opam releases, coq master and coq-core.dev?

I do not understand. Why would you even want to share them? The build scripts, the required versions of dependencies, the conflicts, the patches, etc, everything at some point is bound to diverge.

Why does it have to diverge, since 2.0, opam will update the build definitions from a pin.

For example, any divergence of coq.dev with what we have in master is just a bug. For stable branches, also the canonical files should be the ones in the repos.

What would be an example of such a diverenge? (Other than a patch not yet upstreamed)

Maybe the opam model is just a bit weird when compared to other systems.

I agree, they should be in sync. Having the definition of the build process outside the coq git repo is quite annoying, but that's how opam works and at least it should be the same as what it is inside the repo.

Does this mean that we can't share the same opam files for stable opam releases, coq master and coq-core.dev ?

Does opam complain if you just have the url thing in master?
What I do for Iris is to auto-generate the opam repo file from the git file by appending a suitable url block.

For stable branches, also the canonical files should be the ones in the repos.

This does not make any sense at all! By definition of "stable", stable releases are not installed from a repository branch but from a tarball (or a tag, but that is frowned upon). There is absolutely no repository you can modify when you need to fix something in the Opam packaging of Coq (except the Opam repository itself, obviously). The only official Opam package for Coq is the one in the Opam repository. Anyone who argues the contrary does not understand how Opam and most package managers work.

This is the coq.dev package. There is nothing "stable" about it. It builds the latest git master commit. So it needs to be in sync with the build instructions for the latest git master commit.

For stable branches, I think what they meant is that at the time the release is made, you want to have the build instructions in sync. Later you might have to fix them, and then they start to diverge, sure.

Or they meant the coq.8.16.dev etc packages, which also should stay in sync with the respective branch.

@silene what you say is not consistent with current dune-release practices, which requires opam files in the repository, which are then updated for automatic PR submission to opam repository adding version and url fields.

This is also the workflow for stable branches. Moreover, this workflow is still not good enough so ideally the rewrite step of dune-release will be removed soon.

In fact, more evidence for this point of view that as of today, opam repo maintainers will request to apply local fixes to the repos with a must.

This should work fine once coq/coq#15560 is merged. From today, the canonical opam packages live in Coq's repository. I'm not sure what the best way to keep them in sync is.

erikmd · 2022-06-29T17:34:37Z

Thanks @ejgallego !

What would be an example of such a diverenge?

Actually I agree with @ejgallego here: that for the specific case of *.dev packages, the only sensible difference between opam-coq-archive's and upstream's (committed in master) opam files should be the line

url {
src: "git+https://github.com/_/_.git#master"
}

AFAICT, storing the opam files apart in opam-coq-archive/{core-dev,extra-dev} should mostly been seen as a convenience (without the need to know in advance the exact full name of the github repository), and the "name resolution algorithm", albeit simple and sensible, was not very well documented TTBOMK, so I had opened this issue FWIW.

Beyond this documentation issue:

in terms of automation, I guess it would be interesting to have a GitHub/GitLab pipeline somewhere, that would check that the difference between opam-coq-archive and upstream specs for selected packages, doesn't diverge… @gares @Zimmi48 @palmskog if you agree with this rough idea, where should we open one such issue? maybe in this repo opam-coq-archive?

ejgallego · 2022-06-29T18:14:14Z

Actually the opam files here should be identical copies, that's the reason OPAM supports url files, submitting a PR to fix this now.

mattam82 · 2022-09-15T09:03:59Z

It seems the coqide-server package is missing here.

ejgallego force-pushed the coq+full_dune branch from 5f53b0e to 1d3b23c Compare November 8, 2021 21:34

ejgallego force-pushed the coq+full_dune branch 2 times, most recently from 56f287d to 2e235a4 Compare November 9, 2021 09:44

LasseBlaauwbroek mentioned this pull request Jan 14, 2022

Split coq packages for dev version #1801

Closed

ejgallego mentioned this pull request Jun 24, 2022

[build] Consolidation of build system infrastructure coq/coq#15560

Merged

6 tasks

ejgallego force-pushed the coq+full_dune branch from 2e235a4 to fede298 Compare June 24, 2022 17:09

ejgallego changed the title ~~[coq.dev] Attempt to split the packages.~~ [coq.dev] New upstream split package setup. Jun 24, 2022

ejgallego marked this pull request as ready for review June 24, 2022 17:10

SkySkimmer reviewed Jun 29, 2022

View reviewed changes

core-dev/packages/coq-core/coq-core.dev/opam Outdated Show resolved Hide resolved

ejgallego force-pushed the coq+full_dune branch from fede298 to 6a66dce Compare June 29, 2022 11:58

LasseBlaauwbroek reviewed Jun 29, 2022

View reviewed changes

core-dev/packages/coq-core/coq-core.dev/opam Show resolved Hide resolved

gares reviewed Jun 29, 2022

View reviewed changes

[coq.dev] New upstream split package setup.

18880ba

This should work fine once coq/coq#15560 is merged. From today, the canonical opam packages live in Coq's repository. I'm not sure what the best way to keep them in sync is.

ejgallego force-pushed the coq+full_dune branch from 6a66dce to 18880ba Compare June 29, 2022 16:16

ejgallego merged commit f959493 into coq:master Jun 29, 2022

ejgallego deleted the coq+full_dune branch June 29, 2022 17:14

ejgallego mentioned this pull request Jun 29, 2022

[coq.dev] Use url files instead of rewriting the opam files #2211

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[coq.dev] New upstream split package setup. #1923

[coq.dev] New upstream split package setup. #1923

ejgallego commented Nov 7, 2021 •

edited

Loading

palmskog commented Nov 8, 2021

ejgallego commented Nov 8, 2021

palmskog commented Nov 8, 2021

ejgallego commented Nov 8, 2021 •

edited

Loading

gares commented Nov 9, 2021

ejgallego commented Nov 9, 2021

gares commented Nov 9, 2021

ejgallego commented Jan 14, 2022 •

edited

Loading

ejgallego commented Jun 24, 2022

RalfJung commented Jun 29, 2022

silene commented Jun 29, 2022

ejgallego commented Jun 29, 2022

silene commented Jun 29, 2022 •

edited

Loading

ejgallego commented Jun 29, 2022

gares commented Jun 29, 2022

gares Jun 29, 2022

ejgallego Jun 29, 2022

silene Jun 29, 2022

ejgallego Jun 29, 2022

RalfJung Jun 29, 2022 •

edited

Loading

silene Jun 29, 2022

RalfJung Jun 29, 2022

RalfJung Jun 29, 2022 •

edited

Loading

ejgallego Jun 29, 2022

ejgallego Jun 29, 2022

erikmd commented Jun 29, 2022

ejgallego commented Jun 29, 2022

mattam82 commented Sep 15, 2022

[coq.dev] New upstream split package setup. #1923

[coq.dev] New upstream split package setup. #1923

Conversation

ejgallego commented Nov 7, 2021 • edited Loading

palmskog commented Nov 8, 2021

ejgallego commented Nov 8, 2021

palmskog commented Nov 8, 2021

ejgallego commented Nov 8, 2021 • edited Loading

gares commented Nov 9, 2021

ejgallego commented Nov 9, 2021

gares commented Nov 9, 2021

ejgallego commented Jan 14, 2022 • edited Loading

ejgallego commented Jun 24, 2022

RalfJung commented Jun 29, 2022

silene commented Jun 29, 2022

ejgallego commented Jun 29, 2022

silene commented Jun 29, 2022 • edited Loading

ejgallego commented Jun 29, 2022

gares commented Jun 29, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RalfJung Jun 29, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RalfJung Jun 29, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

erikmd commented Jun 29, 2022

ejgallego commented Jun 29, 2022

mattam82 commented Sep 15, 2022

ejgallego commented Nov 7, 2021 •

edited

Loading

ejgallego commented Nov 8, 2021 •

edited

Loading

ejgallego commented Jan 14, 2022 •

edited

Loading

silene commented Jun 29, 2022 •

edited

Loading

RalfJung Jun 29, 2022 •

edited

Loading

RalfJung Jun 29, 2022 •

edited

Loading