Add dev packages for Coq Platform packages which don't have one as yet #2080

MSoegtropIMC · 2022-01-25T13:41:15Z

This PR adds .dev packages for those packages in Coq Platform which don't have one as yet.

The packages are all derived from and/or checked against the latest released packages and adjusted.

palmskog · 2022-01-25T13:45:27Z

@MSoegtropIMC what's the reasoning behind having coq-dpdgraph depend on conf-automake rather than conf-autoconf? This is not what we are testing in the coq-dpdgraph CI.

MSoegtropIMC · 2022-01-25T13:46:58Z

The released packages have automake/autoconf already run. If you build from git you need to run automake.

MSoegtropIMC · 2022-01-25T13:48:13Z

That is the release opam packages don't have and don't need the ["autoreconf" "-i" "-s"] step.

MSoegtropIMC · 2022-01-25T13:50:15Z

But possibly I messed it up - what is the right conf package for autoreconf? As far as I understand this, autoreconf first calls automake and then autoconf and the automake package included the autoconf package.

extra-dev/packages/coq-dpdgraph/coq-dpdgraph.dev/opam

palmskog · 2022-01-25T13:59:26Z

I don't personally understand the difference between autoreconf and autoconf. I just followed the lead from packages such as Flocq and Interval, and used the same idiom for build dependencies (i.e., conf-autoconf).

silene · 2022-01-25T13:59:39Z

As far as I understand this, autoreconf first calls automake and then autoconf and the automake package included the autoconf package.

autoreconf calls automake only if there is a file Makefile.am. If there is only a file Makefile.in, it should directly call autoconf. But take that with a grain of salt, since I am not completely sure what would happen if you have a file configure.ac (instead of configure.in) but no file Makefile.am.

palmskog · 2022-01-25T13:59:45Z

I don't personally understand the difference between autoreconf and autoconf. I just followed the lead from packages such as Flocq and Interval, and used the same idiom for build dependencies (i.e., conf-autoconf).

MSoegtropIMC · 2022-01-25T14:12:22Z

@silene : thanks for sharing these details! I guess it is safe to switch to autoconf then.

@palmskog : I had a lot of trouble with packages committing to git automake output but not updating this always, so that autoconf usually works, but not always. I spent sufficient time debugging this (debugging m4 is a lot fo fun) that at some point I decided that it simplifies my life to always use autoreconf -i -s which never failed me to get things (a makefile) done.

MSoegtropIMC · 2022-01-25T14:13:43Z

Btw.: what does the dev criterion mean in ["autoconf"] {dev}? That source is from git?

extra-dev/packages/coq-stdpp/coq-stdpp.dev/opam

extra-dev/packages/coq-libhyps/coq-libhyps.dev/opam

extra-dev/packages/coq-iris/coq-iris.dev/opam

extra-dev/packages/coq-interval/coq-interval.dev/opam

extra-dev/packages/coq-gappa/coq-gappa.dev/opam

silene · 2022-01-25T14:49:40Z

what does the dev criterion mean in ["autoconf"] {dev}? That source is from git?

As a rule of thumb, yes. I think there are actually three different cases:

The package is pinned to a local repository. (opam pin /path/to/repo)
The url field was ignored and the dev-repo field was used instead. (opam pin coq-foo --dev-repo)
The url field was used but it does not point to a tarball. (opam install coq-foo.dev)

palmskog · 2022-01-25T16:39:11Z

I see the following for gappa.dev:

# bwrap: execvp bison: No such file or directory

Is there a missing dependency on Bison?

MSoegtropIMC · 2022-01-25T17:21:13Z

Is there a missing dependency on Bison?

It does have "conf-bison" {build} already.

Co-authored-by: Karl Palmskog <palmskog@gmail.com>

palmskog · 2022-01-25T17:24:01Z

OK, it looks like you will have to add the system packages for bison and flex to the CI configuration for the gappa.dev package to build.

MSoegtropIMC · 2022-01-25T18:22:11Z

OK, it looks like you will have to add the system packages for bison and flex to the CI configuration for the gappa.dev package to build.

Why is that? CI doesn't have depext support?

palmskog · 2022-01-25T18:24:56Z

I generally try to stay out of the CI setup, but no, it doesn't have depext support. You'll have to add the packages here in the .gitlab-ci.yml file: https://github.com/coq/opam-coq-archive/blob/76553b80984336c7ec21efd9ae49f65338cc0640/.gitlab-ci.yml#L22

MSoegtropIMC · 2022-01-25T18:29:18Z

Are there known difficulties with depext? With opam 2.1 it should be quite easy to do (at least if you have permissions to install system packages without password).

Co-authored-by: Karl Palmskog <palmskog@gmail.com>

gares · 2022-01-26T08:32:42Z

There is no depext support because we never added it. I think it is the right thing to do, your are welcome to hack the scripts:
https://github.com/coq/opam-coq-archive/blob/1f0f0ec84c738d88a8ee550494917e9387975ebb/scripts/opam-coq-install-remove#L60-L77

The quick fix is to install bison and the other deps upfront.

MSoegtropIMC · 2022-01-26T08:47:04Z

@gares:

There is no depext support because we never added it.

As far as I know in opam 2.1 it is built in. So is CI on opam 2.0 or did you some tricks to disable it?

gares · 2022-01-26T08:58:17Z

Not really a trick: https://github.com/coq/opam-coq-archive/blob/1f0f0ec84c738d88a8ee550494917e9387975ebb/.gitlab-ci.yml#L16

Maybe it's time to switch to 2.1 (it is not beta anymore, right?)

MSoegtropIMC · 2022-01-26T09:15:59Z

Maybe it's time to switch to 2.1 (it is not beta anymore, right?)

No, it is released. It 2.1.2 now (https://opam.ocaml.org/blog/opam-2-1-2/).

MSoegtropIMC · 2022-01-26T09:22:21Z

@palmskog : can we merge this now? I don't think we need to wait for CI for the commit of your changes - except for the gappa depext issues it did run through before and you anyway suggested to do this PR without CI and that "extra-dev is Wild-West".

Or do you want me to fix the bison/flex dependencies? I would rather enable depext but do this after the Coq Platform release.

I can also keep the dev packages in the Coq Platform local opam repo.

MSoegtropIMC · 2022-01-26T09:26:58Z

Btw.: we can also remove the gappa.dev package from here. Please note that the release package lives in the main opam repo, but since they don't have the concept of a dev repo I put the dev package here. But I can also keep it local to Coq platform (or remove it entirely and always use gappa releases).

palmskog · 2022-01-26T09:30:38Z

Fine by me to have the gappa.dev package here. @gares should we merge this now or fix the opam version and ci?

MSoegtropIMC · 2022-01-26T10:38:13Z

@palmskog : I need this to be merged before 1 PM German time or I will keep the packages in the Coq Platform patch repo in the release. I don't think it is worth it to delay the Coq Platform release just for the opam cleanup.

MSoegtropIMC · 2022-01-26T11:35:31Z

Thanks! I do the final Coq Platform PR right away.

RalfJung · 2022-08-12T19:35:16Z

extra-dev/packages/coq-stdpp/coq-stdpp.dev/opam

@@ -0,0 +1,43 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"


I would appreciate if this package would be removed. We deliberately did not put a coq-stdpp.dev (or coq-iris.dev) package into this repository. The 'dev' version is meant for local pinning only. This is not just cosmetic; I noticed these packages because they lead to strange behavior of our CI.

I am surprised that the people maintaining this software (and supposedly even maintaining this package!) did not get pinged...

Note that this is not the first time this happened, there were "rogue" coq-iris.dev packages already in 2017 and they have been removed again (#191 -- though those versions really made no sense, this time at least the dev packages are actually properly tracking git).

#2256 proposes to remove these packages again.

Add dev packages for Coq Platform packages which don't have one as yet

73caa15