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
```

mathcomp-analysis will be up to 1.1.0 now

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
```

Amazing @Julien Puydt !

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.

@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.

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.

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

How do the packages generate the .install files?

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
```

Yeah, that seems pretty cumbersome. For dune I guess `dh_dune`

should do something like this (for packages that contain one dune package):

- dune build -p $pkg && dune install --destdir=debian/tmp/ $pkg (assuming Debian's dune is configured correctly, it used not to be the case)
- generate the debian install files for the corresponding dune-generated files, each section could be mapped.
- ?
- profit !

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

I'm not sure our dune is configured correctly indeed

Good point, current config line is:

https://salsa.debian.org/ocaml-team/ocaml-dune/-/blob/master/debian/rules?ref_type=heads#L22

That will set directories as follows:

```
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"
}
```

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

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

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:

```
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"
}
```

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

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

So that will set dirs for example to `/usr/doc`

that I believe it is wrong for Debian

also likely wrong for `etc`

The current behavior of ignoring the configure values once `--prefix`

is passed is quite annoying, but can be tweaked.

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

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

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

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`

Note it is only used if `--prefix`

is not passed to `dune install`

otherwise `--prefix`

will override it

Of course, once `dune install`

is good, you can use it to install dune itself

so in a sense it can also affect dune

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!

They are indexed by "section" names

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

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.

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

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.

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

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

could also understand them

but I haven't dug how a dh_dune would work

Most packages would need this for build:

- an optional, package-specific configure step
- dune build -p $pkgs # that generates _build/install/default and the opam .install files for the packages
- now
`_build/install/default`

is in opam layout, so we call`dune install --destdir=debian/tmp`

which will produce a debian layout - now dh_dune can generate the Debian .install files based on the Dune install files (or just be more traditional and scan debian/tmp, but using dune files makes multi-package setups easier)
- the rest is standard I understand

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

file

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....

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

Last updated: Oct 13 2024 at 01:02 UTC