Stream: Coq devs & plugin devs

Topic: Taking over maintenance of the Debian package


view this post on Zulip 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 ;-)

view this post on Zulip Karl Palmskog (Nov 06 2021 at 14:58):

ping @Enrico Tassi who is the resident Debian expert

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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...

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 16:56):

that's definitely outdated, the 2 env variables are wrong

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 17:01):

ie only CAML_LD_LIBRARY_PATH and COQLIB are env variables

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 17:12):

(based on what CI does)

view this post on Zulip Julien Puydt (Nov 06 2021 at 17:13):

/usr/lib/stublibs/dllcoqrun_stubs.so looks like a strange path

view this post on Zulip Julien Puydt (Nov 06 2021 at 17:14):

oh, that line looks like tests run!

view this post on Zulip Julien Puydt (Nov 06 2021 at 17:15):

at least its doing many TEST/CHECK things... and no FAIL in sight

view this post on Zulip 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!

view this post on Zulip Julien Puydt (Nov 06 2021 at 17:22):

bugs/opened/bug_3889.v...still active ?

view this post on Zulip Julien Puydt (Nov 06 2021 at 17:22):

most failures I have seen are from File not found on loadpath : ltac2_plugin.cmxs

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 17:31):

ugh this damn _build_vo stuff
this will need @Emilio Jesús Gallego Arias

view this post on Zulip Julien Puydt (Nov 06 2021 at 17:31):

The installation script tries to do smart things about a .coq-native directory... obsolete?

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 17:32):

no

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 17:33):

depending on what it does

view this post on Zulip Emilio Jesús Gallego Arias (Nov 06 2021 at 19:16):

Why you need to pass special stuff

view this post on Zulip Emilio Jesús Gallego Arias (Nov 06 2021 at 19:16):

just use make test-suite ?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 06 2021 at 19:20):

For Debian tho you can just use dh_dune and Dune 2.9

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 06 2021 at 19:21):

that should get you 99% there easily

view this post on Zulip Emilio Jesús Gallego Arias (Nov 06 2021 at 19:21):

modulo any custom packaging stuff you'd like to do

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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."

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 21:23):

you're seeing this in summary.log?

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Julien Puydt (Nov 06 2021 at 21:49):

Well, that came much faster : compilation breaks much sooner with Error: Cannot find plugins directory

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 21:50):

is that a fresh build?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 21:56):

oh you're not on master

view this post on Zulip Gaëtan Gilbert (Nov 06 2021 at 21:56):

ignore the *.opam files they're not compatible with the "native compute" feature

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julien Puydt (Nov 07 2021 at 08:49):

Gaëtan Gilbert said:

oh you're not on master

Eh, no, I package released versions!

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 09:09):

coqide-server is necessary for coqide so certainly in debian

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 11:34):

d:coq-theories is u:coq-stdlib + the stdlib html doc

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 11:40):

in terms of packaging sure
in terms of the files it contains it is needed

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 11:40):

in other words opam coqide includes dune coqide-server

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 11:40):

(or possibly it's in opam coq)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Guillaume Melquiond (Nov 07 2021 at 11:47):

As I said, it is not needed, so I did not package it in Opam.

view this post on Zulip Guillaume Melquiond (Nov 07 2021 at 11:48):

There are only two Opam packages for 8.14, coq and coqide.

view this post on Zulip Julien Puydt (Nov 07 2021 at 11:49):

Wouldn't it make sense to put u:coqide-server in d:coqide?

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 11:50):

currently it's also used by some other ides AFAIK

view this post on Zulip Guillaume Melquiond (Nov 07 2021 at 11:50):

And more importantly, it does not depend on GTK.

view this post on Zulip Julien Puydt (Nov 07 2021 at 11:51):

Oh, u:coqide-server is not coqide-only

view this post on Zulip Julien Puydt (Nov 07 2021 at 11:51):

that would indeed push me to put it in coq

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Guillaume Melquiond (Nov 07 2021 at 12:17):

That is the same file, better keep it in d:coq.

view this post on Zulip 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 ?

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 12:24):

yes

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2021 at 15:46):

indeed .ml etc... files are required in the -dev package

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 15:58):

required is too strong, you can compile stuff without them

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip Julien Puydt (Nov 07 2021 at 16:07):

badly, as expected... sigh... we'll see tomorrow morning if I find the time

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Julien Puydt (Nov 07 2021 at 16:15):

(I have names...)

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 16:31):

what's "coq-"?

view this post on Zulip Julien Puydt (Nov 07 2021 at 16:35):

I don't know what "coq-" is ; I'll try to see tomorrow morning

view this post on Zulip 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)

view this post on Zulip 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-

view this post on Zulip Julien Puydt (Nov 07 2021 at 16:39):

hmmm... the loop was already there before... that's strange

view this post on Zulip Gaëtan Gilbert (Nov 07 2021 at 17:05):

the current package says Provides: coq-8.12.0+4.11.1

view this post on Zulip 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...

view this post on Zulip Julien Puydt (Nov 07 2021 at 17:12):

No more computer time for me today!

view this post on Zulip 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

view this post on Zulip 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...)

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Nov 08 2021 at 09:02):

(.cmxs is just a fancy name for .so.)

view this post on Zulip Enrico Tassi (Nov 08 2021 at 09:04):

Guillaume Melquiond said:

(.cmxs is just a fancy name for .so.)

(if you get hit in the head and forget ABIs are useful ;-)

view this post on Zulip Gaëtan Gilbert (Nov 08 2021 at 09:10):

Guillaume Melquiond said:

The .cmxs files should be part of libcoq-ocaml; all the other ones should be part of libcoq-ocaml-dev.

some of the cmos are also for libcoq-ocaml (the ones which correspond to a cmxs)

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip 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...

view this post on Zulip Julien Puydt (Nov 08 2021 at 11:04):

libcoq-ocaml-dev also has a warning ocaml-dangling-cmi for each cmi file

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Julien Puydt (Nov 08 2021 at 11:30):

Gaëtan Gilbert said:

Guillaume Melquiond said:

The .cmxs files should be part of libcoq-ocaml; all the other ones should be part of libcoq-ocaml-dev.

some of the cmos are also for libcoq-ocaml (the ones which correspond to a cmxs)

Hmmm... So I should:

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 08 2021 at 12:58):

if coqtop.byte is distributed then so should plugins.cmo

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Nov 08 2021 at 13:12):

they've been dynlinked in byte for a long time

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Gaëtan Gilbert (Nov 10 2021 at 08:03):

isn't there a more explicit lint message? this doesn't seem very useful

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 10 2021 at 08:14):

and clib.cm(x)a is for the -dev package

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 11 2021 at 15:25):

@Julien Puydt that should not be a problem

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Nov 11 2021 at 15:40):

Coq-Elpi should know that the OCaml libraries are under coq-core though.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 11 2021 at 15:52):

and COQCORELIB for the ml files

view this post on Zulip Emilio Jesús Gallego Arias (Nov 11 2021 at 15:53):

so something went off

view this post on Zulip Emilio Jesús Gallego Arias (Nov 11 2021 at 15:53):

where is your packaging tree

view this post on Zulip Emilio Jesús Gallego Arias (Nov 11 2021 at 15:53):

?

view this post on Zulip 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]

view this post on Zulip Emilio Jesús Gallego Arias (Nov 11 2021 at 15:54):

DESTDIR indeed

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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="

view this post on Zulip Julien Puydt (Nov 11 2021 at 15:57):

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.

view this post on Zulip Gaëtan Gilbert (Nov 11 2021 at 15:58):

kinda weird to have to pass coqbin

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Nov 11 2021 at 16:09):

what's wrong with just the 2nd one?

view this post on Zulip Julien Puydt (Nov 11 2021 at 16:11):

With just the second one, coq isn't found (unbound modules Loc and Names)

view this post on Zulip Julien Puydt (Nov 11 2021 at 16:12):

Ah, in fact setting COQCORELIB in the second one isn't necessary

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 15:47):

@Julien Puydt , yup, I think you wanna ship them

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 15:47):

you got a public repos ?

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Nov 12 2021 at 15:54):

the timing files are used for the timing targets of coq_makefile

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 15:55):

Ok thanks, let me know when you want a review

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 15:55):

IMHO we should be able to simplify the current version quite a bit

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)))

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:51):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:51):

still 8.14 not in the best shape tho

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:52):

let's say that was not an easy transition

view this post on Zulip 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

view this post on Zulip Julien Puydt (Nov 12 2021 at 16:52):

Of course, I'll switch to the dune build system with the next release.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:52):

that I will fix in 2.9.2

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:53):

Dune support for 8.14 is fine , once I fix that bug

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:53):

I have been using dune for Coq exclusively since 8.10

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:54):

Actually 8.14 already uses dune

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:54):

for the most complex parts (OCaml)

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:54):

Yeah, also building OCAml is not easy

view this post on Zulip 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

view this post on Zulip 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 ;-)

view this post on Zulip Julien Puydt (Nov 12 2021 at 17:20):

(in fact, I looked at the .opam file to see how things should be done...)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 18:01):

Oh very nice! Thanks, I was not aware of it.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 18:02):

would be great if we can factor that to a dh_dune thing

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Julien Puydt (Nov 12 2021 at 21:38):

My package for coq gets a lot of warnings for three things:

  1. W: libcoq-ocaml: shared-library-lacks-prerequisites usr/lib/coq-core/clib/clib.cmxs (for each and every cmxs file in the package!)

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

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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 12 2021 at 22:13):

this is nothing to do with coq afaict, you should ask the debian ocaml experts

view this post on Zulip 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"

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Julien Puydt (Nov 12 2021 at 22:24):

no UND!? That's bad...

view this post on Zulip 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

view this post on Zulip Julien Puydt (Nov 12 2021 at 22:30):

Ok, that will be for tomorrow

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Julien Puydt (Nov 13 2021 at 08:27):

are multiple double-underscore possible?

view this post on Zulip 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: Feb 06 2023 at 19:03 UTC