Julien Puydt (Nov 06 2021 at 14:56): Julien Puydt (Nov 06 2021 at 14:56):Hi, I'm trying to take over the maintenance of the Debian package, and it's not going as smoothly as I would like.
Good: I think I get it to compile. At least it compiles a long time and _build/install/default and
Bad: I have to get the reference manual out because of license issues. For this, I drop doc/changelog, doc/plugin_tutorial, doc/sphinx and doc/whodidwhat from the archive, to concentrate on the stdlib documentation. "make doc-stdlib-html" seems to work (it surely work a long time on something), but _build_default/doc/stdlib/html/ is empty and the gorgeous _build/default/doc/stdlib/index-list.html points to non-existing html files. Similarly _build/install/default/doc doesn't contain much more than a few README.md. _build_vo/default/doc/stdlib looks pretty good with a full html/ directory, but the corresponding index-list.html doesn't point to those files! In there, Library.* files look correct (even if short).
Bad: in the test suite, everything fails with "Error: Unable to locate library Prelude with prefix Coq." ; I have ./_build/install/default/lib/coq/theories/Init/Prelude.vo, ./_build/default/theories/Init/Prelude.vo and ./_build_vo/default/lib/coq/theories/Init/Prelude.vo so I think it's not making a real effort there ;-)
Karl Palmskog (Nov 06 2021 at 14:58):ping @Enrico Tassi who is the resident Debian expert
Karl Palmskog (Nov 06 2021 at 15:15):I broke off the discussion about manual relicensing to here, I think that particular issue should be solvable in the medium term: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Change.20of.20manual.20license.20for.20DFSG.20compatibility
Julien Puydt (Nov 06 2021 at 15:53):I'm a Debian expert, but I'm only a beginner in Coq and lack experience with OCaml (especially dune/menhir/whatever...), so I'm a bit over my head for now -- that will improve!
Karl Palmskog (Nov 06 2021 at 16:08):I think it would help if you gave us details on what Coq version you are trying to build. Is it Coq master? If so, it uses Dune to build all OCaml files, but make to build all Coq files after coqc is done.
Karl Palmskog (Nov 06 2021 at 16:10):the "default build" is embodied in our opam package definitions, such as this one: https://github.com/ocaml/opam-repository/tree/master/packages/coq/coq.8.14.0
Julien Puydt (Nov 06 2021 at 16:26):I have ocaml 4.11.1, dune 2.7.1, zarith 1.11, ocamlfind 1.8.1, ounit 2.2.3... which should all be pretty much correct.
Karl Palmskog (Nov 06 2021 at 16:30):if it helps, we do have Docker containers that are built from Debian for many versions of Coq:
Julien Puydt (Nov 06 2021 at 16:36):Karl Palmskog said:
if it helps, we do have Docker containers that are built from Debian for many versions of Coq:
Hmmm... I'll check if my packages build in a clean environment when it will build in a dirty one -- for now
The tests are run with:
CAML_LD_LIBRARY_PATH=$(shell pwd)/kernel/byterun COQLIB=$(shell pwd) $(MAKE) test-suite COMPLEXITY= PRINT_LOGS=1
does that look sane? I fear the building system changed since the actual version in Debian...
Gaëtan Gilbert (Nov 06 2021 at 16:56):that's definitely outdated, the 2 env variables are wrong
Julien Puydt (Nov 06 2021 at 16:58):I see four of them: CAML_LD_LIBRARY_PATH, COQLIB, COMPLEXITY and PRINT_LOGS... what are the two wrongs?
Gaëtan Gilbert (Nov 06 2021 at 17:00):in shell syntax, foo=bla make bar=bli sets the env variable foo locally to the command, and make sets the make variable bar
Gaëtan Gilbert (Nov 06 2021 at 17:01):ie only CAML_LD_LIBRARY_PATH and COQLIB are env variables
Julien Puydt (Nov 06 2021 at 17:07):It turns out that if I disable checks, I can install something in debian/tmp which pretty much looks like what I'll want to put in packages
Gaëtan Gilbert (Nov 06 2021 at 17:10):something like
OCAMLPATH=$(pwd)/_build_vo/default/lib make -C test-suite COQBIN=$(pwd)/_build_vo/default/bin COQLIB=$(pwd)/_build_vo/default/lib/coq
may work
Gaëtan Gilbert (Nov 06 2021 at 17:12):(based on what CI does)
Julien Puydt (Nov 06 2021 at 17:13):/usr/lib/stublibs/dllcoqrun_stubs.so looks like a strange path
Julien Puydt (Nov 06 2021 at 17:14):oh, that line looks like tests run!
Julien Puydt (Nov 06 2021 at 17:15):at least its doing many TEST/CHECK things... and no FAIL in sight
Julien Puydt (Nov 06 2021 at 17:17):Ah, I have seen a few FAILED fly by, so things aren't 100% perfect -- but at least I feel like you pushed me much further!
Julien Puydt (Nov 06 2021 at 17:22):bugs/opened/bug_3889.v...still active ?
Julien Puydt (Nov 06 2021 at 17:22):most failures I have seen are from File not found on loadpath : ltac2_plugin.cmxs
Gaëtan Gilbert (Nov 06 2021 at 17:31):ugh this damn _build_vo stuff
this will need @Emilio Jesús Gallego Arias
Julien Puydt (Nov 06 2021 at 17:31):The installation script tries to do smart things about a .coq-native directory... obsolete?
Gaëtan Gilbert (Nov 06 2021 at 17:32):no
Gaëtan Gilbert (Nov 06 2021 at 17:33):depending on what it does
Emilio Jesús Gallego Arias (Nov 06 2021 at 19:16):Why you need to pass special stuff
Emilio Jesús Gallego Arias (Nov 06 2021 at 19:16):just use make test-suite ?
Emilio Jesús Gallego Arias (Nov 06 2021 at 19:16):Tho may fixes on master where not backported to 8.14, so who knows
Emilio Jesús Gallego Arias (Nov 06 2021 at 19:20):For Debian tho you can just use dh_dune and Dune 2.9
Emilio Jesús Gallego Arias (Nov 06 2021 at 19:21):as you will likely choose on a per-distro basis whether to enable native
Emilio Jesús Gallego Arias (Nov 06 2021 at 19:21):that should get you 99% there easily
Emilio Jesús Gallego Arias (Nov 06 2021 at 19:21):modulo any custom packaging stuff you'd like to do
Julien Puydt (Nov 06 2021 at 20:33):Emilio Jesús Gallego Arias said:
For Debian tho you can just use dh_dune and Dune 2.9
Hmmm... there's no dune 2.9 in Debian yet, and there's no dh_dune as far as I know
Gaëtan Gilbert (Nov 06 2021 at 20:38):Emilio Jesús Gallego Arias said:
just use
make test-suite?
I thought it was broken? https://github.com/coq/coq/issues/14342#issuecomment-844798676
Julien Puydt (Nov 06 2021 at 20:44):Gaëtan Gilbert said:
Emilio Jesús Gallego Arias said:
just use
make test-suite?I thought it was broken? https://github.com/coq/coq/issues/14342#issuecomment-844798676
I can confirm "Error: Cannot find plugins directory" -- I'll stick with the previous line!
Gaëtan Gilbert (Nov 06 2021 at 20:50):Julien Puydt said:
bugs/opened/bug_3889.v...still active ?
what's the error there btw?
Julien Puydt (Nov 06 2021 at 21:17):Gaëtan Gilbert said:
Julien Puydt said:
bugs/opened/bug_3889.v...still active ?
what's the error there btw?
Error: Anomaly "Could not find a solvable obligation."
Julien Puydt (Nov 06 2021 at 21:22):I can't help but notice that the debian source package for coq has the following binary packages: coq, coqide, coq-theories, libcoq-ocaml and libcoq-ocaml-dev, while the upstream source package for coq seems to have the following: coq-core, coq-doc, coqide, coqide-server, coq and coq-stdlib.
I obviously won't ship coq-doc for license reasons, but perhaps I should follow upstream and change the binary package names in Debian?
Gaëtan Gilbert (Nov 06 2021 at 21:22):Julien Puydt said:
Gaëtan Gilbert said:
Julien Puydt said:
bugs/opened/bug_3889.v...still active ?
what's the error there btw?
Error: Anomaly "Could not find a solvable obligation."
oh that's normal
Gaëtan Gilbert (Nov 06 2021 at 21:23):you're seeing this in summary.log?
Gaëtan Gilbert (Nov 06 2021 at 21:24):can you treat just make test-suite (no env vars) with https://github.com/coq/coq/pull/15136 ?
Julien Puydt (Nov 06 2021 at 21:33):I have no summary.log : I don't get to the end of the test suite, because it's interrupted by: ocamlfind: Package `coqide-server.protocol' not found
Julien Puydt (Nov 06 2021 at 21:35):I get 43 failures ; one is bug/opened/bug_3889.v.log as already mentioned.
I see Error: Unbound module Mltop in misc/side-eff-leak-univs.log and misc/non-marshalable-state.log.
I have Error: Unbound module Pcoq in misc/quotation_token.log
Also Error: Unbound module Names in misc/poly-capture-global-univs.log
and all the rest is: Error: File not found on loadpath : ltac2_plugin_cmxs
Julien Puydt (Nov 06 2021 at 21:46):I'll try pull 15136 -- though I hope there were no other changes than what I see in commit a92bb09a -- expect new in twenty minutes
Julien Puydt (Nov 06 2021 at 21:49):Well, that came much faster : compilation breaks much sooner with Error: Cannot find plugins directory
Gaëtan Gilbert (Nov 06 2021 at 21:50):is that a fresh build?
Julien Puydt (Nov 06 2021 at 21:54):That was a fresh build, but as I said the commit was applied by hand and didn't quite look right (no COQ_NOT_CONFIGURED in my test-suite/Makefile!), so I wasn't expecting a miracle.
I'll go to bed now ; tomorrow I'll try to make clean binary packages from what I get with nocheck -- which means the question of which binary packages (follow the *.opam list or the current Debian list) will need consideration.
Gaëtan Gilbert (Nov 06 2021 at 21:56):oh you're not on master
Gaëtan Gilbert (Nov 06 2021 at 21:56):ignore the *.opam files they're not compatible with the "native compute" feature
Enrico Tassi (Nov 07 2021 at 06:34):Julien Puydt said:
I can't help but notice that the debian source package for coq has the following binary packages: coq, coqide, coq-theories, libcoq-ocaml and libcoq-ocaml-dev, while the upstream source package for coq seems to have the following: coq-core, coq-doc, coqide, coqide-server, coq and coq-stdlib.
I obviously won't ship coq-doc for license reasons, but perhaps I should follow upstream and change the binary package names in Debian?
No, you should follow the ocaml policy, see the doc of dh-ocaml. In particular the lib packages are needed to compile coq plugins like aac-tactics. The contain cm* stuff, which is not needed to run coq.
Splitting further serves no purpose for Debian, imo.
Enrico Tassi (Nov 07 2021 at 06:37):Emilio Jesús Gallego Arias said:
For Debian tho you can just use dh_dune and Dune 2.9
google for "debian dh_dune" gives no results to me. What are you referring to?
Hugo Herbelin (Nov 07 2021 at 08:01):@Enrico Tassi will know more how the Debian Coq team is organized but for the latest Debian packages, we had an interaction with Ralf Treinen. You probably contacted him I guess.
Enrico Tassi (Nov 07 2021 at 08:12):That is great. I did recently retire from Debian, since I have no more time to dedicate to it. I guess my knowledge about the packaging policies will quicly fade, but I think what I just wrote is still up to date.
Julien Puydt (Nov 07 2021 at 08:49):Gaëtan Gilbert said:
oh you're not on master
Eh, no, I package released versions!
Julien Puydt (Nov 07 2021 at 09:06):Enrico Tassi said:
Julien Puydt said:
I can't help but notice that the debian source package for coq has the following binary packages: coq, coqide, coq-theories, libcoq-ocaml and libcoq-ocaml-dev, while the upstream source package for coq seems to have the following: coq-core, coq-doc, coqide, coqide-server, coq and coq-stdlib.
I obviously won't ship coq-doc for license reasons, but perhaps I should follow upstream and change the binary package names in Debian?
No, you should follow the ocaml policy, see the doc of dh-ocaml. In particular the lib packages are needed to compile coq plugins like aac-tactics. The contain cm* stuff, which is not needed to run coq.
Splitting further serves no purpose for Debian, imo.
Well, I wasn't thinking of dropping the lib packages, but splitting as libcoq-stdlib, libcoq-core, coqide-server, coqide and coq. If I understand well, using u: for an upstream package and d: for a Debian one, the current situation is that d:libcoq is u:coq-core, d:coq-theories is u:coq-stdlib, d:coq is u:coq and d:coqide is u:coqide. u:coqide-server is new, not in Debian. Am I right?
Gaëtan Gilbert (Nov 07 2021 at 09:09):coqide-server is necessary for coqide so certainly in debian
Gaëtan Gilbert (Nov 07 2021 at 09:10):I would need to see some file lists to say more (I don't want to guess based on package names)
Julien Puydt (Nov 07 2021 at 11:28):Ah, in fact libcoq-stdlib doesn't make sense, since it's not a library in the operating system sense -- hence the coq-theories name.
I have file lists: https://packages.debian.org/sid/amd64/coq-theories/filelist https://packages.debian.org/sid/amd64/coqide/filelist https://packages.debian.org/sid/amd64/libcoq-ocaml-dev/filelist https://packages.debian.org/sid/amd64/libcoq-ocaml/filelist https://packages.debian.org/sid/amd64/coq/filelist
(for the current packages)
Guillaume Melquiond (Nov 07 2021 at 11:33):Gaëtan Gilbert said:
coqide-server is necessary for coqide so certainly in debian
No, it is just an artifact due to Dune. Coqide is perfectly happy if it is not installed.
Gaëtan Gilbert (Nov 07 2021 at 11:34):d:coq-theories is u:coq-stdlib + the stdlib html doc
Gaëtan Gilbert (Nov 07 2021 at 11:34):Guillaume Melquiond said:
Gaëtan Gilbert said:
coqide-server is necessary for coqide so certainly in debian
No, it is just an artifact due to Dune. Coqide is perfectly happy if it is not installed.
coqide-server is coqidetop, coqide certainly needs it (it's in debian coq)
Gaëtan Gilbert (Nov 07 2021 at 11:38):d:coqide looks pretty close to u:coqide
u:coq-core and u:coqide-server are split across the others: executables and misc stuff in d:coq, plugin dynlinked executables in libcoq-ocaml, other compilation products in libcoq-ocaml-dev
Guillaume Melquiond (Nov 07 2021 at 11:39):Look, for 8.14, Opam ships packages for coq and coqide, but not coqide-server. Yet, coqide works perfectly fine. So, I insist, coqide-server is not needed.
Gaëtan Gilbert (Nov 07 2021 at 11:40):in terms of packaging sure
in terms of the files it contains it is needed
Gaëtan Gilbert (Nov 07 2021 at 11:40):in other words opam coqide includes dune coqide-server
Gaëtan Gilbert (Nov 07 2021 at 11:40):(or possibly it's in opam coq)
Guillaume Melquiond (Nov 07 2021 at 11:43):Yes, it is in coq. The coqide-server Opam package only contains libraries that are useful for compiling things like Coqide, but it contains nothing needed for executing it.
Gaëtan Gilbert (Nov 07 2021 at 11:47):opam show coqide-server
[ERROR] No package matching coqide-server found
where's the coqide-server package?
Guillaume Melquiond (Nov 07 2021 at 11:47):As I said, it is not needed, so I did not package it in Opam.
Guillaume Melquiond (Nov 07 2021 at 11:48):There are only two Opam packages for 8.14, coq and coqide.
Julien Puydt (Nov 07 2021 at 11:49):Wouldn't it make sense to put u:coqide-server in d:coqide?
Julien Puydt (Nov 07 2021 at 11:50):I must admit I have a hard time knowing what file is part of what u:package... that doesn't help deciding what d:packages should contain
Gaëtan Gilbert (Nov 07 2021 at 11:50):currently it's also used by some other ides AFAIK
Guillaume Melquiond (Nov 07 2021 at 11:50):And more importantly, it does not depend on GTK.
Julien Puydt (Nov 07 2021 at 11:51):Oh, u:coqide-server is not coqide-only
Julien Puydt (Nov 07 2021 at 11:51):that would indeed push me to put it in coq
Guillaume Melquiond (Nov 07 2021 at 12:09):Anyway, as far as 8.14 is concerned, there are only two upstream packages, u:coq and u:coqide. Whether there are more upstream packages for 8.15 is up to the 8.15 maintainer.
Julien Puydt (Nov 07 2021 at 12:15):The previous d:coq wanted a usr/lib/coq/plugins/micromega/csdpcert -- I see a /usr/bin/csdpcert I don't know where to put...
Guillaume Melquiond (Nov 07 2021 at 12:17):That is the same file, better keep it in d:coq.
Julien Puydt (Nov 07 2021 at 12:23):d:libcoq-ocaml-dev contained usr/lib/coq-core/gramlib/.pack/gramlib.cma -- should it now contain usr/lib/coq-core/gramlib/*.cma ?
Gaëtan Gilbert (Nov 07 2021 at 12:24):yes
Julien Puydt (Nov 07 2021 at 15:00):Hmmm... several questions:
(1) Where do .ml and .mli go (I know they are source -- but they got installed by the make install targets) ?
(2) What are .cmt and .cmti files and where do they fit?
(3) usr/lib/coqide/META, usr/lib/coqide/dune-package and usr/lib/coqide/opam -- where do they go?
Gaëtan Gilbert (Nov 07 2021 at 15:16):(1) Where do .ml and .mli go (I know they are source -- but they got installed by the make install targets) ?
(2) What are .cmt and .cmti files and where do they fit?
they're both used for "jump to definition" dev workflow
Julien Puydt (Nov 07 2021 at 15:18):Gaëtan Gilbert said:
they're both used for "jump to definition" dev workflow
They weren't in the d:packages before, what should I do?
Julien Puydt (Nov 07 2021 at 15:21):I see from debian packages for other OCaml software that META, dune-package and opam get shipped, so I'll ship them too
Julien Puydt (Nov 07 2021 at 15:28):and also .ml, .mli, .cmt and .cmti files get in lib*-ocaml-dev packages, so that's settled!
Emilio Jesús Gallego Arias (Nov 07 2021 at 15:42):Gaëtan Gilbert said:
ignore the *.opam files they're not compatible with the "native compute" feature
Actually they are if you use dune 2.9 and fix a policy for native, what they don't have is "dynamic detection of native" depending on the value of coqc -config
Emilio Jesús Gallego Arias (Nov 07 2021 at 15:44):Guillaume Melquiond said:
Gaëtan Gilbert said:
coqide-server is necessary for coqide so certainly in debian
No, it is just an artifact due to Dune. Coqide is perfectly happy if it is not installed.
What do you mean by "an artifact due to Dune"; we choose to create that package just out of modularity reasons, not due to any Dune policy
Emilio Jesús Gallego Arias (Nov 07 2021 at 15:46):indeed .ml etc... files are required in the -dev package
Gaëtan Gilbert (Nov 07 2021 at 15:58):required is too strong, you can compile stuff without them
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:03):I don't remember the exact wording of the Debian policy but IIRC -dev goes beyond compilation
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:03):but yeah I'm pretty sure they should be there, along with the cmt etc...
Julien Puydt (Nov 07 2021 at 16:04):I just managed to obtain .deb packages... first time! Let's install and see how things go...
Julien Puydt (Nov 07 2021 at 16:07):badly, as expected... sigh... we'll see tomorrow morning if I find the time
Karl Palmskog (Nov 07 2021 at 16:08):maybe of interest: https://github.com/JasonGross/coq-debian-build-scripts
I think a lot of people are still using these debs in CI through a PPA (https://launchpad.net/~jgross-h)
Julien Puydt (Nov 07 2021 at 16:15):I'll have a look but not any file with a deb extension is really a Debian package
Julien Puydt (Nov 07 2021 at 16:15):(I have names...)
Julien Puydt (Nov 07 2021 at 16:30):my coq provides "coq-" and depends on coq-theories, and coq-theories depends on "coq-" -- there's a loop there
Gaëtan Gilbert (Nov 07 2021 at 16:31):what's "coq-"?
Julien Puydt (Nov 07 2021 at 16:35):I don't know what "coq-" is ; I'll try to see tomorrow morning
Julien Puydt (Nov 07 2021 at 16:36):I guess I broke some dep computations (I took everything I couldn't understand out of debian/rules, and that means most of it is gone)
Julien Puydt (Nov 07 2021 at 16:38):Provides: coq-${F:CoqABI} <- if ${F:CoqABI} 's subst doesn't happen correctly, I guess that gives a coq-
Julien Puydt (Nov 07 2021 at 16:39):hmmm... the loop was already there before... that's strange
Gaëtan Gilbert (Nov 07 2021 at 17:05):the current package says Provides: coq-8.12.0+4.11.1
Julien Puydt (Nov 07 2021 at 17:12):I just launched coqide and checked the following is correct:
Lemma h: forall a: nat, a = a.
Proof.
auto.
Qed.
that must mean I made a step forward...
Julien Puydt (Nov 07 2021 at 17:12):No more computer time for me today!
Paolo Giarrusso (Nov 07 2021 at 17:13):@Julien Puydt are loops a problem? https://www.debian.org/doc/debian-policy/ch-relationships.html implies dpkg supports them
Paolo Giarrusso (Nov 07 2021 at 17:13):(it also suggests some potential problems, but from https://wiki.debian.org/CircularBuildDependencies it doesn't seem an urgent one...)
Paolo Giarrusso (Nov 07 2021 at 17:17):and I thought I had seen loops used to encode "install both together"... installing coq-core without coq-theories would "work" but I'm not sure it'd be useful for anybody yet.
Julien Puydt (Nov 08 2021 at 06:56):No, it's indeed used to force co-installation -- which brings up the question: why two packages?!
I mean, they come from the same source, they have to be installed together...
Guillaume Melquiond (Nov 08 2021 at 07:38):The original reason was that coq-theories was supposed to have an all architecture, contrarily to coq. (But it never worked properly.)
Enrico Tassi (Nov 08 2021 at 08:58):Indeed the idea was to build .vo files on a fast machine (amd64) and use them also on slower hardware.
Julien Puydt (Nov 08 2021 at 08:59):So perhaps I could merge them?
Announce: this morning I upload to Debian Experimental the package I got yesterday, for testing and feedback !
I have files with extensions .ml, .mli, .cma, .cmi, .cmo, .cmx, .cmxs, .cmt, .cmti, .whatever and I'm not sure I put the right ones in the right package (I get warnings from tools...) -- can someone run down what those files are and whether they belong to libcoq-ocaml (runtime files) or libcoq-ocaml-dev (compile-time files)?
Enrico Tassi (Nov 08 2021 at 08:59):Said that, there is at least one project out there which can take advantage of a separate package for the stdlib, coq-tactician. It was also the (main?) motivation for splitting in opam.
Enrico Tassi (Nov 08 2021 at 09:01):@Julien Puydt all these details should be taken care of by dh_ocaml (and are given in its policy/doc, namely /usr/share/doc/dh-ocaml/ocaml_packaging_policy.html). I don't get why you would change these things
Guillaume Melquiond (Nov 08 2021 at 09:01):The .cmxs files should be part of libcoq-ocaml; all the other ones should be part of libcoq-ocaml-dev.
Enrico Tassi (Nov 08 2021 at 09:02):Julien Puydt said:
So perhaps I could merge them?
It depends if you/others plan to package coq-tactician or not
Guillaume Melquiond (Nov 08 2021 at 09:02):(.cmxs is just a fancy name for .so.)
Enrico Tassi (Nov 08 2021 at 09:04):Guillaume Melquiond said:
(
.cmxsis just a fancy name for.so.)
(if you get hit in the head and forget ABIs are useful ;-)
Gaëtan Gilbert (Nov 08 2021 at 09:10):Guillaume Melquiond said:
The
.cmxsfiles should be part oflibcoq-ocaml; all the other ones should be part oflibcoq-ocaml-dev.
some of the cmos are also for libcoq-ocaml (the ones which correspond to a cmxs)
Enrico Tassi (Nov 08 2021 at 09:16):We changed Coq build system, but these files were there even before (in 8.13 or 8.12) so @Julien Puydt should just copy what was done before.
Julien Puydt (Nov 08 2021 at 10:58):I did copy what was done.
Why does lintian give me two warnings for each .cmxs file: ocaml-dangling-cmxs and shared-library-lacks-prerequisites ?
Julien Puydt (Nov 08 2021 at 11:02):Enrico Tassi said:
Julien Puydt said:
So perhaps I could merge them?
It depends if you/others plan to package coq-tactician or not
Well, if coq-theories can't be installed without coq, I don't see how adding coq-tactician to the mix will help...
Julien Puydt (Nov 08 2021 at 11:04):libcoq-ocaml-dev also has a warning ocaml-dangling-cmi for each cmi file
Karl Palmskog (Nov 08 2021 at 11:04):I think what Enrico means is that there are members in the community who want to have a "modular stdlib", i.e., want to hook in different versions of the stdlib or no stdlib
Karl Palmskog (Nov 08 2021 at 11:05):steps have been taken to enable this modularization, so it may be worth keeping in mind for future packaging.
Julien Puydt (Nov 08 2021 at 11:30):Gaëtan Gilbert said:
Guillaume Melquiond said:
The
.cmxsfiles should be part oflibcoq-ocaml; all the other ones should be part oflibcoq-ocaml-dev.some of the
cmos are also for libcoq-ocaml (the ones which correspond to a cmxs)
Hmmm... So I should:
Guillaume Melquiond (Nov 08 2021 at 11:44):Seems sensible. That said, I don't know if there are actual users who dynamically link against .cmo files.
Gaëtan Gilbert (Nov 08 2021 at 12:58):if coqtop.byte is distributed then so should plugins.cmo
Guillaume Melquiond (Nov 08 2021 at 13:09):Gaëtan Gilbert said:
if coqtop.byte is distributed then so should plugins.cmo
For a long time, bytecode plugins were statically linked inside coqtop.byte. Are you saying that they are now dynamically loaded?
Gaëtan Gilbert (Nov 08 2021 at 13:12):they've been dynlinked in byte for a long time
Julien Puydt (Nov 08 2021 at 14:31):Enrico Tassi said:
We changed Coq build system, but these files were there even before (in 8.13 or 8.12) so Julien Puydt should just copy what was done before.
Things aren't that clear ; the OCaml Packaging Policy doesn't say anything about .cmt and .cmti files, for example and there were none in the previous package.
And lintian is pretty unhappy about libcoq-ocaml* putting files in /usr/lib but not in /usr/lib/ocaml/, about finding .cmi files without the corresponding .mli or .ml file (ocaml-dangling-cmi)... so that I also have the impression that not everyone agrees with what I should put where.
I'll shuffle things around until it looks right.
Jason Gross (Nov 09 2021 at 06:09):maybe of interest: https://github.com/JasonGross/coq-debian-build-scripts
I think a lot of people are still using these debs in CI through a PPA (https://launchpad.net/~jgross-h)
The Debian folder I have targeting the development branches might be of more interest: https://github.com/JasonGross/coq-packaging/tree/master/debian. It's moderately less kludgy. (I still need to branch for 8.14 though)
Julien Puydt (Nov 10 2021 at 07:13):Jason Gross said:
maybe of interest: https://github.com/JasonGross/coq-debian-build-scripts
I think a lot of people are still using these debs in CI through a PPA (https://launchpad.net/~jgross-h)
The Debian folder I have targeting the development branches might be of more interest: https://github.com/JasonGross/coq-packaging/tree/master/debian. It's moderately less kludgy. (I still need to branch for 8.14 though)
Your debian folder looks very much like mine -- indeed I removed most of libcoq-*.install.in to use debian/rules to populate it. But don't you get lintian unhappy?
Julien Puydt (Nov 10 2021 at 07:40):My libcoq-ocaml_8.14.0+dfsg-2_amd64.deb has for example /usr/lib/coq-core/clib/clib.cma and /usr/lib/coq-core/clib/clib.cmxs ; my libcoq-ocaml-dev_8.14.0+dfsg-2_amd64.deb has /usr/lib/coq-core/clib/clib.a and /usr/lib/coq-core/clib/clib.cmxa.
I'm not happy with it because:
I must be missing something...
Gaëtan Gilbert (Nov 10 2021 at 08:03):isn't there a more explicit lint message? this doesn't seem very useful
Julien Puydt (Nov 10 2021 at 08:10):It's not useful, and trying to read how lintian comes to this hint... no clue, it's Perl.
I also noticed that "file clib.cmxs" says it's dynamically linked and "ldd clib.cmxs" says it's statically linked -- so perhaps lintian is just wrong about the file type and the reports are bogus.
Gaëtan Gilbert (Nov 10 2021 at 08:14):I think dune generates both the static and dynamic files for every library
so clib.cmxs is useless
Gaëtan Gilbert (Nov 10 2021 at 08:14):and clib.cm(x)a is for the -dev package
Julien Puydt (Nov 10 2021 at 08:16):Well, the install targets do install .cmxs files ; and the packaging policy says to ship them in libcoq-ocaml
Julien Puydt (Nov 10 2021 at 08:24):Sigh... I also have many warnings about unstripped-static-library, but again: does lintian really know what it's talking about?
Enrico Tassi (Nov 10 2021 at 09:42):I think you should ask these details to the ocaml task force in Debian, here: https://wiki.debian.org/Teams/OCamlTaskForce/ they probably know better
Emilio Jesús Gallego Arias (Nov 10 2021 at 11:06):clib.cmxs and other cmxs may be needed if you are using a findlib plugin loader
Emilio Jesús Gallego Arias (Nov 10 2021 at 11:07):dh_dune indeed doesn't exist, but should be a very nice thing to have if we could make some time for it
Emilio Jesús Gallego Arias (Nov 10 2021 at 11:07):IIUC there is a systematic way to take the install files generated by dune and produce the debian ones
Julien Puydt (Nov 11 2021 at 14:36):Eh, I just discovered my coq package installs the lib in usr/lib/coq-core, and the theories in usr/lib/coq ; so of course trying to compile coq-elpi (the next thing I'll package) doesn't work... sigh...
Emilio Jesús Gallego Arias (Nov 11 2021 at 15:25):@Julien Puydt that should not be a problem
Julien Puydt (Nov 11 2021 at 15:26):Well, if I don't tell coq-elpi where coq is, then I get unbound modules (Loc and Names, if memory serves) ; and if I point it to coq, then it doesn't find the theories (which do get installed in /usr/lib/coq !) -- so it's a problem
Théo Zimmermann (Nov 11 2021 at 15:40):Coq-Elpi should know that the OCaml libraries are under coq-core though.
Julien Puydt (Nov 11 2021 at 15:49):Well, here "make -k build" fails because the Loc and Names modules aren't found ; and if I "make -k build COQLIB=/usr/lib/coq-core", then there's a failure because there's no /usr/lib/coq-core/theories...
Emilio Jesús Gallego Arias (Nov 11 2021 at 15:52):I dunno how elpi rules are, but indeed coq_makefile in 8.14 has to notions, COQLIB for the vo files
Emilio Jesús Gallego Arias (Nov 11 2021 at 15:52):and COQCORELIB for the ml files
Emilio Jesús Gallego Arias (Nov 11 2021 at 15:53):so something went off
Emilio Jesús Gallego Arias (Nov 11 2021 at 15:53):where is your packaging tree
Emilio Jesús Gallego Arias (Nov 11 2021 at 15:53):?
Emilio Jesús Gallego Arias (Nov 11 2021 at 15:53):likely indeed you are building in the tmp/ prefix as typical for debian, for that you can try the regular env var [I forgot the name]
Emilio Jesús Gallego Arias (Nov 11 2021 at 15:54):DESTDIR indeed
Julien Puydt (Nov 11 2021 at 15:54):If you take coq-elpi upstream and type "make build", then you get a failure -- no strange prefix or anything yet
Julien Puydt (Nov 11 2021 at 15:55):Even the "make clean" fails because it tries to look for Makefile.test.coq in all apps directories -- I just added one with:
%:
@echo $@
to avoid the problem
Emilio Jesús Gallego Arias (Nov 11 2021 at 15:55):I dunno @Julien Puydt , coq-elpi in opam works just fine and uses that layout
Karl Palmskog (Nov 11 2021 at 15:57):the coq-elpi opam package uses the following to build:
make "build" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" "OCAMLWARN="
Karl Palmskog said:
the coq-elpi opam package uses the following to build:
make "build" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" "OCAMLWARN="
Yes, that's what I saw in coq-elpi.opam.
Gaëtan Gilbert (Nov 11 2021 at 15:58):kinda weird to have to pass coqbin
Julien Puydt (Nov 11 2021 at 16:07):make -k build COQLIB=/usr/lib/coq-core || make -k build COQCORELIB=/usr/lib/coq-core
makes the compilation pass... by first failing, then trying again, not updating the targets it managed to build on the first pass.
Ugly, isn't it?
Gaëtan Gilbert (Nov 11 2021 at 16:09):what's wrong with just the 2nd one?
Julien Puydt (Nov 11 2021 at 16:11):With just the second one, coq isn't found (unbound modules Loc and Names)
Julien Puydt (Nov 11 2021 at 16:12):Ah, in fact setting COQCORELIB in the second one isn't necessary
Enrico Tassi (Nov 11 2021 at 17:02):the first run it calls coqmakefile, in the second run it does not.If you open an issue with logs I can look at it on monday.
I override COQBIN since the makefile lets you override which coq to use by setting this. But in opam you want the opam one to be used, no matter what the user env says.
Julien Puydt (Nov 11 2021 at 17:58):I reworked my package from scratch and things compile flawlessly now... no clue why I had problems before :unamused:
Julien Puydt (Nov 12 2021 at 15:34):Ok my coq package is starting to look like I could upload it to unstable (still have to check if things like why3 accept compiling with it though!), but I'm wondering about the following files in the previous package: /usr/lib/coq/tools/make-both-single-timing-files, /usr/lib/coq/tools/make-both-time-files, /usr/lib/coq/tools/make-one-time-file and (of course) /usr/lib/coq/tools/TimeFileMaker.py : I do ship them too... but am I supposed to?
Emilio Jesús Gallego Arias (Nov 12 2021 at 15:47):@Julien Puydt , yup, I think you wanna ship them
Emilio Jesús Gallego Arias (Nov 12 2021 at 15:47):Let me know if you wanna me have a look to the package, I'm experienced with both Coq and Debian build systems
Emilio Jesús Gallego Arias (Nov 12 2021 at 15:47):you got a public repos ?
Julien Puydt (Nov 12 2021 at 15:53):Here you have a link: https://tracker.debian.org/pkg/coq
(I have a few other commits not pushed yet)
Gaëtan Gilbert (Nov 12 2021 at 15:54):the timing files are used for the timing targets of coq_makefile
Emilio Jesús Gallego Arias (Nov 12 2021 at 15:55):Ok thanks, let me know when you want a review
Emilio Jesús Gallego Arias (Nov 12 2021 at 15:55):IMHO we should be able to simplify the current version quite a bit
Julien Puydt (Nov 12 2021 at 16:48):Gaëtan Gilbert said:
the timing files are used for the timing targets of coq_makefile
The fact that they end up in /usr/lib although they are execs is pretty wrong -- they should probably end up in bin/ (with better names)
Julien Puydt (Nov 12 2021 at 16:49):Emilio Jesús Gallego Arias said:
IMHO we should be able to simplify the current version quite a bit
My version is already much simpler than what was there in the first place... I'm open to suggestions
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:50):Julien Puydt said:
Gaëtan Gilbert said:
the timing files are used for the timing targets of coq_makefile
The fact that they end up in /usr/lib although they are execs is pretty wrong -- they should probably end up in bin/ (with better names)
Note that in master we install these files in libexec , which is, TTOMK the right location
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:50):(install
(section libexec)
(package coq-core)
(files
(TimeFileMaker.py as tools/TimeFileMaker.py)
(make-one-time-file.py as tools/make-one-time-file.py)
(make-both-time-files.py as tools/make-both-time-files.py)
(make-both-single-timing-files.py as tools/make-both-single-timing-files.py)))
@Julien Puydt we did a big rework of the build system to use a tool with more capabilities called dune, it can for example produce build files etc....
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:51):I'll have a look when you have a final version and let you know, but it is not too far fetched to try to have a dh_dune that could work out of the box for Coq
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:51):Coq used to have a super custom build system, it is not the case anymore
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:51):still 8.14 not in the best shape tho
Julien Puydt (Nov 12 2021 at 16:52):Emilio Jesús Gallego Arias said:
Julien Puydt we did a big rework of the build system to use a tool with more capabilities called
dune, it can for example produce build files etc....
Ah, yes, but I only package released versions -- and as far as I know, the 8.14.0's preferred build system is still the Makefiles
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:52):let's say that was not an easy transition
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:52):Ah, yes, but I only package released versions -- and as far as I know, the 8.14.0's preferred build system is still the Makefiles
We may actually switch that to Dune even for 8.14 , actually all that is preventing that is a bug in coq native rules of Dune
Julien Puydt (Nov 12 2021 at 16:52):Of course, I'll switch to the dune build system with the next release.
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:52):that I will fix in 2.9.2
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:53):Dune support for 8.14 is fine , once I fix that bug
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:53):I have been using dune for Coq exclusively since 8.10
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:54):Actually 8.14 already uses dune
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:54):for the most complex parts (OCaml)
Julien Puydt (Nov 12 2021 at 16:54):I don't know enough about dune yet, but it looks saner than the current Makefile system (which is that way because it must be quite old -- not a judgement on the devs)
Emilio Jesús Gallego Arias (Nov 12 2021 at 16:54):Yeah, also building OCAml is not easy
Emilio Jesús Gallego Arias (Nov 12 2021 at 17:03):So you get an idea, a workflow to build a dune package in the debian style is a bit like this:
at this stage, you already have a build layout under _build/install/$profile , you could use dune install --destdir=tmp if you would like to follow the typical workflow, but this is just a copy operation.
so all that remains to be done is to take dune-generated install files and maybe postprocess them
Julien Puydt (Nov 12 2021 at 17:15):@Emilio Jesús Gallego Arias yes, like I did for https://salsa.debian.org/ocaml-team/elpi -- I know how to do that ;-)
Julien Puydt (Nov 12 2021 at 17:20):(in fact, I looked at the .opam file to see how things should be done...)
Emilio Jesús Gallego Arias (Nov 12 2021 at 18:01):Oh very nice! Thanks, I was not aware of it.
Emilio Jesús Gallego Arias (Nov 12 2021 at 18:02):would be great if we can factor that to a dh_dune thing
Emilio Jesús Gallego Arias (Nov 12 2021 at 18:02):Dune 3.0 will be released soon, I'm sure if some tweak would help debian the devs would agree to include it
Julien Puydt (Nov 12 2021 at 20:25):Emilio Jesús Gallego Arias said:
Dune 3.0 will be released soon, I'm sure if some tweak would help debian the devs would agree to include it
Well, dune is already in Debian, so why wouldn't dune 3.0 be? Perhaps I can even get a hand in updating it...
Julien Puydt (Nov 12 2021 at 21:38):My package for coq gets a lot of warnings for three things:
W: libcoq-ocaml: shared-library-lacks-prerequisites usr/lib/coq-core/clib/clib.cmxs (for each and every cmxs file in the package!)
I: libcoq-ocaml-dev: ocaml-dangling-cmi usr/lib/coq-core/gramlib/gramlib__Gramext.cmi (for all cmi files whose name looks like foo_bar.cmi)
I: libcoq-ocaml-dev: unstripped-static-library usr/lib/coq-core/clib/clib.a (cArray.o cEphemeron.o cList.o cMap.o cObj.o cPath.o cSet.o cString.o cThread.o cUnix.o diff2.o dyn.o exninfo.o hMap.o hashcons.o hashset.o heap.o iStream.o int.o minisys.o monad.o option.o orderedType.o predicate.o range.o segmenttree.o store.o terminal.o trie.o unicode.o unionfind.o) (for 35 of the 39 .a in the package)
I'm suspecting 1 and 3 are false positives because the tool doesn't know about Coq's way to handle object files, and I think the ocaml-dangling-cmi is because it was told about a rule "no cmi without ml/mli" but not some exception for __-named cmi.
In short: please confirm I'm innocent and I should file neat bug reports...
Julien Puydt (Nov 12 2021 at 21:43):I had a look and I think the four .a not getting 3 are: /usr/lib/coq-core/lib/lib.a, /usr/lib/coq-core/lib/library.a, /usr/lib/coq-core/vm/coqrun.a and /usr/lib/coq-core/vm/libcoqrun_stubs.a, in case that helps.
Gaëtan Gilbert (Nov 12 2021 at 22:13):this is nothing to do with coq afaict, you should ask the debian ocaml experts
Julien Puydt (Nov 12 2021 at 22:15):I did ask the Debian OCaml experts, and the only who answered said something like "Oh, I have the same ; no clue"
Julien Puydt (Nov 12 2021 at 22:18):I think 1 is linked to objdump -T /usr/lib/coq-core/clib/clib.cmxs showing many UND -- but perhaps it's normal that those objects have many such things?
Julien Puydt (Nov 12 2021 at 22:20):For 2, the question of what cmi files with a double underscore means is certainly not Debian-specific
Gaëtan Gilbert (Nov 12 2021 at 22:21):I don't have any UND in my objdump
could be because I compiled in dev mode not release mode, I dunno
https://lintian.debian.org/tags/shared-library-lacks-prerequisites says it's about ldd
Gaëtan Gilbert (Nov 12 2021 at 22:21):Julien Puydt said:
For 2, the question of what cmi files with a double underscore means is certainly not Debian-specific
it's ocaml specific
Julien Puydt (Nov 12 2021 at 22:24):Yes, but for most cmi, there is an associated ml/mli file -- for all with-__ ones, there is none
Julien Puydt (Nov 12 2021 at 22:24):no UND!? That's bad...
Julien Puydt (Nov 12 2021 at 22:29):What's strange is that my coq package seems to work whenever I try it (aac-tactics and coq-float were broken with the old one too, so that doesn't count!) -- I'm still waiting on the ssreflect compilation against it
Julien Puydt (Nov 12 2021 at 22:30):Ok, that will be for tomorrow
Gaëtan Gilbert (Nov 12 2021 at 22:38):Julien Puydt said:
no UND!? That's bad...
turns out I grepped the wrong command, I have 190 UND
Gaëtan Gilbert (Nov 12 2021 at 22:39):Julien Puydt said:
Yes, but for most cmi, there is an associated ml/mli file -- for all with-__ ones, there is none
there is one, foo__bar.cmi comes from bar.mli in library foo (library is a dune concept)
Gaëtan Gilbert (Nov 12 2021 at 22:40):Julien Puydt said:
What's strange is that my coq package seems to work whenever I try it (aac-tactics and coq-float were broken with the old one too, so that doesn't count!) -- I'm still waiting on the ssreflect compilation against it
what's strange about it? lints are not errors
Julien Puydt (Nov 13 2021 at 07:32):Gaëtan Gilbert said:
Julien Puydt said:
Yes, but for most cmi, there is an associated ml/mli file -- for all with-__ ones, there is none
there is one, foo__bar.cmi comes from bar.mli in library foo (library is a dune concept)
I'll have to check and report to the tool devs!
Julien Puydt (Nov 13 2021 at 07:34):Gaëtan Gilbert said:
Julien Puydt said:
What's strange is that my coq package seems to work whenever I try it (aac-tactics and coq-float were broken with the old one too, so that doesn't count!) -- I'm still waiting on the ssreflect compilation against it
what's strange about it? lints are not errors
I try to leverage tools whenever I can to ensure my packages quality -- and if the tool isn't good enough, I'll report so it can be improved. That's why I'm looking into those hints.
Julien Puydt (Nov 13 2021 at 08:21):Hmmmm... in my elpi package, I see the situation of those .cmi files can be quite complex:
Julien Puydt (Nov 13 2021 at 08:27):are multiple double-underscore possible?
Emilio Jesús Gallego Arias (Nov 13 2021 at 11:41):the .cmi warnings are IMHO spurious, for the others I'd try asking at https://discuss.ocaml.org/
Last updated: Jun 04 2023 at 19:30 UTC