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):
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:
_build/install/default
is in opam layout, so we call dune install --destdir=debian/tmp
which will produce a debian layoutfor 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