Stream: Coq devs & plugin devs

Topic: Updating Coq to 8.19 in Debian


view this post on Zulip Julien Puydt (Mar 30 2024 at 16:20):

Here is what I can get working locally for now - nothing uploaded yet as some packages are still incompatible:

* Update Coq [4/7]
 - [X] step 1 [2/2]
   - [X] elpi 1.18.2-1
   - [X] coq 8.19.1+dfsg-1
 - [-] step 2 [13/17]
   - [X] aac-tactics 8.19.0-1
   - [X] coq-bignums 9.0.0+coq8.19-1
   - [X] coq-dpdgraph 1.0+8.19-1 ?
   - [X] coq-elpi 2.1.0-1
   - [X] coq-ext-lib 0.12.1-1
   - [ ] coq-hammer FAILURE [[https://github.com/lukaszcz/coqhammer/issues/175][upstream report]]
   - [X] coq-hott 8.19-1
   - [X] coq-libhyps 2.0.8-2
   - [X] coq-menhirlib 20231231+ds-2
   - [X] coq-record-update 0.3.3-2
   - [X] coq-reduction-effects 0.1.5-2
   - [ ] coq-stdpp FAILURE [[https://gitlab.mpi-sws.org/iris/stdpp/-/issues/205][upstream report]]
   - [ ] coq-unicoq FAILURE [[https://github.com/unicoq/unicoq/issues/90][upstream report]]
   - [X] coq-unimath 20240321-1
   - [X] flocq 4.1.4-1
   - [ ] ott FAILURE [[https://github.com/ott-lang/ott/issues/105][upstream report]]
   - [X] paramcoq 1.1.3+coq8.19-1
 - [-] step 3 [5/8]
   - [X] coq-equations 1.3-8.19-1
   - [X] coq-gappa 1.5.5-1
   - [X] coq-hierarchy-builder 1.7.0-1
   - [ ] coq-iris WAIT coq-stdpp
   - [ ] coq-math-classes FAILURE [[https://github.com/coq-community/math-classes/issues/124][upstream report]]
   - [ ] coq-mtac2 WAIT coq-unicoq
   - [X] coq-simple-io 1.8.0-5
   - [X] coqprime 8.19-1
 - [-] step 4 [1/2]
   - [X] ssreflect 2.2.0-1
   - [ ] coq-corn WAIT coq-math-classes
 - [X] step 5 [8/8]
   - [X] coq-deriving 0.2.0-2
   - [X] coq-reglang 1.2.1-2
   - [X] coq-relation-algebra 1.7.10-2
   - [X] coquelicot 3.4.1-2
   - [X] mathcomp-bigenough 1.0.1-13
   - [X] mathcomp-finmap 2.1.0-1
   - [X] mathcomp-zify 1.5.0+2.0+8.16-2
   - [X] coq-quickchick 2.0.2-2
 - [X] step 6 [6/6]
   - [X] coq-extructures 0.4.0-2
   - [X] coq-interval 4.10.0-1
   - [X] mathcomp-algebra-tactics 1.2.3-2
   - [X] mathcomp-analysis 1.0.0-2
   - [X] mathcomp-multinomials 2.2.0-2
   - [X] mathcomp-real-closed 2.0.2-2
 - [X] step 7 [1/1]
   - [X] coqeal 2.0.2-1

view this post on Zulip Julien Puydt (Apr 01 2024 at 09:07):

mathcomp-analysis will be up to 1.1.0 now

view this post on Zulip Julien Puydt (Apr 12 2024 at 15:19):

Current status of my packaging work (not ready for upload yet, obviously):

* Update Coq [4/7]
 - [X] step 1 [2/2]
   - [X] elpi 1.18.2-1
   - [X] coq 8.19.1+dfsg-1
 - [-] step 2 [15/17]
   - [X] aac-tactics 8.19.0-1
   - [X] coq-bignums 9.0.0+coq8.19-1
   - [X] coq-dpdgraph 1.0+8.19-1 ?
   - [X] coq-elpi 2.1.0-1
   - [X] coq-ext-lib 0.12.1-1
   - [X] coq-hammer 1.3.2+8.19-1
   - [X] coq-hott 8.19-1
   - [X] coq-libhyps 2.0.8-2
   - [X] coq-menhirlib 20231231+ds-2
   - [X] coq-record-update 0.3.4-1
   - [X] coq-reduction-effects 0.1.5-2
   - [X] coq-stdpp 1.10.0-1
   - [ ] coq-unicoq FAILURE [[https://github.com/unicoq/unicoq/issues/90][upstream report]]
   - [X] coq-unimath 20240331-1
   - [X] flocq 4.1.4-1
   - [ ] ott FAILURE [[https://github.com/ott-lang/ott/issues/105][upstream report]]
   - [X] paramcoq 1.1.3+coq8.19-1
 - [-] step 3 [6/8]
   - [X] coq-equations 1.3-8.19-1
   - [X] coq-gappa 1.5.5-1
   - [X] coq-hierarchy-builder 1.7.0-1
   - [X] coq-iris 4.2.0-1
   - [ ] coq-math-classes FAILURE [[https://github.com/coq-community/math-classes/issues/124][upstream report]]
   - [ ] coq-mtac2 WAIT coq-unicoq
   - [X] coq-simple-io 1.9.0-1
   - [X] coqprime 8.19-1
 - [-] step 4 [1/2]
   - [X] ssreflect 2.2.0-1
   - [ ] coq-corn WAIT coq-math-classes
 - [X] step 5 [8/8]
   - [X] coq-deriving 0.2.0-2
   - [X] coq-reglang 1.2.1-2
   - [X] coq-relation-algebra 1.7.10-2
   - [X] coquelicot 3.4.1-2
   - [X] mathcomp-bigenough 1.0.1-13
   - [X] mathcomp-finmap 2.1.0-1
   - [X] mathcomp-zify 1.5.0+2.0+8.16-2
   - [X] coq-quickchick 2.0.3-1
 - [X] step 6 [6/6]
   - [X] coq-extructures 0.4.0-2
   - [X] coq-interval 4.10.0-1
   - [X] mathcomp-algebra-tactics 1.2.3-2
   - [X] mathcomp-analysis 1.0.0-2
   - [X] mathcomp-multinomials 2.2.0-2
   - [X] mathcomp-real-closed 2.0.2-2
 - [X] step 7 [1/1]
   - [X] coqeal 2.0.2-1

view this post on Zulip Emilio Jesús Gallego Arias (Apr 16 2024 at 21:50):

Amazing @Julien Puydt !

view this post on Zulip Emilio Jesús Gallego Arias (Apr 16 2024 at 21:51):

Let me know of licencing or other issues with coq-lsp and coq-serapi; I'm very happy to support a Debian .deb build in the official CI if that would help.

view this post on Zulip Julien Puydt (Apr 18 2024 at 07:01):

@Emilio Jesús Gallego Arias I first need to upload Coq 8.19 to Debian, and then I'll be able to work on new packages. I remember I had an experimental one for coq-serapi, and only plans for alectryon and coq-lsp.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 12:19):

Other than licence issues, which should be solved by now, both serapi and coq-lsp and now standard dune package so if Debian has finally implemented something like dh_dune_ocaml things should work out of the box.

view this post on Zulip Julien Puydt (Apr 18 2024 at 12:21):

No dh_dune_ocaml, but calling dune by hand (well, override_dh_auto_{build,install}) is generally good

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 12:22):

How do the packages generate the .install files?

view this post on Zulip Julien Puydt (Apr 18 2024 at 12:27):

They're either written directly, or using d/rules. For example, coq-iris/debian/libcoq-iris.install is the one-line usr/lib/ocaml/coq/user-contrib/iris/*, while elpi's debian/libelpi-ocaml.install.in is @OCamlStdlibDir@/elpi/META, and debian/rules's override_dh_auto_install target has:

        find debian/tmp -regextype posix-awk \
          -regex '.*\.(cma|cmxs)$$' \
          >> debian/libelpi-ocaml.install

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 12:42):

Yeah, that seems pretty cumbersome. For dune I guess dh_dune should do something like this (for packages that contain one dune package):

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 12:43):

OPAM/Dune install files are specified upstream, and easy to parse, so indeed something better than grep/awk can be used

view this post on Zulip Julien Puydt (Apr 18 2024 at 13:18):

I'm not sure our dune is configured correctly indeed

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:20):

Good point, current config line is:
https://salsa.debian.org/ocaml-team/ocaml-dune/-/blob/master/debian/rules?ref_type=heads#L22

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:20):

That will set directories as follows:

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:21):

let library_path = ["/usr/lib/ocaml"]

let roots : string option Install.Roots.t =
  { lib_root = Some "/usr/lib/ocaml"
  ; man = None
  ; doc_root = None
  ; etc_root = None
  ; share_root = None
  ; bin = None
  ; sbin = None
  ; libexec_root = Some "/usr/lib/ocaml"
  }

view this post on Zulip Julien Puydt (Apr 18 2024 at 13:25):

Hmmm... but that configure line is how dune is compiled, not how it will handle things once installed

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:28):

That configure line tell dune how to handle things by default in dune install

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:29):

if --prefix is not present, it will use the dirs provided, if --prefix is set, it will use the hardcoded values below, unless some other options like --mandir where passed to dune install, so it depends what the rest of packages do for dune install. If you configure dune correctly, dune install will always use the dirs setup in configure.

Default paths when using prefix are:

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:29):

let make prefix ~relative =
  let lib_root = relative prefix "lib" in
  { lib_root
  ; libexec_root = lib_root
  ; bin = relative prefix "bin"
  ; sbin = relative prefix "sbin"
  ; share_root = relative prefix "share"
  ; man = relative prefix "man"
  ; doc_root = relative prefix "doc"
  ; etc_root = relative prefix "etc"
  }

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:30):

So likely wrong for Debian, let me see what dune itself for example does

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:30):

override_dh_auto_install:
    ./dune.exe install --destdir=$(DESTDIR) --prefix=/usr --libdir=$(OCAML_STDLIB_DIR) $(DEB_DUNE_ALL_PACKAGES)

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:31):

So that will set dirs for example to /usr/doc that I believe it is wrong for Debian

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:31):

also likely wrong for etc

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:32):

The current behavior of ignoring the configure values once --prefix is passed is quite annoying, but can be tweaked.

view this post on Zulip Julien Puydt (Apr 18 2024 at 13:32):

Wait, the configure line to build dune is used for all uses of dune afterwards?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:33):

Do we have a relevant entry for the Debian OCaml policy? I'd be happy to contribute detailed guide for Dune

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:33):

That's the whole point, dune doesn't need any other configuration

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:33):

Julien Puydt said:

Wait, the configure line to build dune is used for all uses of dune afterwards?

The whole point of dune configure is to set common parameter for dune install

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:33):

Note it is only used if --prefix is not passed to dune install

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:33):

otherwise --prefix will override it

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:35):

Of course, once dune install is good, you can use it to install dune itself

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:35):

so in a sense it can also affect dune

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:36):

Anyways for Debian that's not even needed, as we could skip the install step, as opam/dune install files are agnostic over the paths!

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:36):

They are indexed by "section" names

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:37):

See https://dune.readthedocs.io/en/stable/usage.html#destination-directory

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:39):

I guess tho that dh_dune would have to move the files at some point, so maybe indeed it is still better to use dune install for this, so maybe just automating the splitting would work.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:40):

In the end I see no point not to have a dh_dune

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:41):

That would make the maintainence of all packages very simple, of all the packages I use, only a couple would need a bit o extra config.

view this post on Zulip Julien Puydt (Apr 18 2024 at 13:42):

I have written some tools to help with managing Coq packages https://tracker.debian.org/pkg/dh-coq

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:43):

Note that for Coq dune packages, they also use the stadnard build form, so dh_dune could also understand them

view this post on Zulip Julien Puydt (Apr 18 2024 at 13:44):

but I haven't dug how a dh_dune would work

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:47):

Most packages would need this for build:

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:47):

for each $pkg in $pkgs Dune will generate a pkg.install file

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:48):

so in general dh_dune would need a simple tool that takes pkg.install as input and generates the right libfoo-ocaml.install pkg.install (for packages that ship things in bin), the doc packages, etc....

view this post on Zulip Emilio Jesús Gallego Arias (Apr 18 2024 at 13:48):

It seems to me that this step doesn't entail special difficulty


Last updated: Oct 13 2024 at 01:02 UTC