Coq's dune build/install system should distinguish ocaml libs and coq libs

[SnarkBoojum]

The matter was discussed recently on zulip, but no satisfactory solution was proposed.

With this configure line:

./configure -bindir /usr/bin -libdir /usr/lib/ocaml -configdir /etc/xdg/coq -datadir /usr/share/coq -mandir /usr/share/man -docdir /usr/share/doc/coq -coqdocdir /usr/share/texmf/tex/latex/misc

the build lines:

dune build -p coq-core,coq-stdlib,coqide-server,coqide --display=verbose
dune build @stdlib-html --display=verbose

and the install line:

dune install coq-core coq-stdlib coqide-server coqide  --destdir=$(CURDIR)/debian/tmp --prefix=/usr --mandir=/usr/share/man --libdir=/usr/lib/ocaml

Then Prelude.vo ends up in /usr/lib/ocaml/coq/theories/Init/Prelude.vo, while everything looks for it in /usr/lib/ocaml/theories/Init/Prelude.vo.

There should be libdir to install the ocaml libs for coq, and a coqlibdir to install the coq libs for coq (ie: stdlib). The problem is that the dune build organisation confuses the two.

[SnarkBoojum]

Here is a work-in-progress patch to try to find every place where coq doesn't find its parts:
workaround_upstream_15452.txt

[ejgallego]

This is a known issue due to lib_root being mapped incorrectly it seems. A fix is on the way.

For now I recommend amending the coq-stdlib.install file with a simple sed script.

[SnarkBoojum]

I tried to dig into those .install files:

1. they come by identical pairs (one in toplevel, the other in _build/default) ;
2. they say where the files to be installed are, not where to ;
3. their format is unclear.

Can you tell me more about them?

[ejgallego]

Oh indeed, sorry, you don't need to mess with the install files, but with the dune install command.

You can do dune install --libdir=/usr/lib coq-stdlib and that should map the directory correctly. To be more concrete, the problem is that dune generates stuff like this in the .install files:

lib: [
  "_build/install/default/lib/coq-core/boot/boot.a" {"boot/boot.a"
....

and

lib_root:
  "_build/install/default/lib/coq/theories/Arith/Arith.v" {"coq/theories/Arith/Arith.v"}
....

but for some reason lib_root doesn't point to /usr/lib but to /usr/lib/ocaml, so it needs refinement. I guess this is a consequence of dune used mostly for opam packages to this point, but it should not be a problem to make the setup more flexible.

I remember having discussed this setup with Dune devs as to extend the semantics, but I can't find the discussion in my notes yet.

I have a better fix on the way, but won't happen this week given my deadlines sorry.

[ejgallego]

Answers to your questions:

1. The files in the source dir are "promoted" from the build dir, this is due to opam needing them there, I think this will stop to be the case at some point.
2. The format is based on opam's install format, it creates a triplet for every file, (section, build_location, relative_install_path) where the relative install path refers to the section root.
3. I am not sure where the format documentation is, but it is pretty straightfoward IMHO

[SnarkBoojum]

That's not as simple as passing -libdir /usr/lib when installing coq-stdlib: it will put the files in the right directory, but the prelude will still be searched as /usr/lib/ocaml/coq/theories/Init/Prelude.vo because that's what I gave at configure-time.

[ejgallego]

Oh, what happens if libdir is set to that dir instead, does Coq still fail? That should be easy to fix.

[SnarkBoojum]

Ah, the problem is that the same libdir is used for ocaml libraries, coq libraries and the plugins. So I'm still trying to find out what to set where and what to patch so everything works.

There's a three-step testing to do:

• ocamlfind list |grep coq (to see if ocaml libraries are found) ;
• strace coqidetop.opt 2>&1|grep Prelude.vo (to see if the prelude is found) ;
• strace coqidetop.opt 2>&1|grep plugins (to see if plugins are found).

Hopefully I won't discover more checking steps once I'll have those three settled...

[ejgallego]

@SnarkBoojum let me have a look at the code that determines the location of things, we should be able to figure out if the Debian layout will work at all indeed.

[SnarkBoojum]

I would say part of the problem is that you have to look at the codes (plural!) that determine the location of things... duplication doesn't help there.

I think I have something going with the combination of:

1. configure with -libdir /usr/lib ;
2. install coq-stdlib with -libdir /usr/lib ;
3. install coq-core, coqide-server and coqide with -libdir /usr/lib/ocaml ;
4. the attached patch (newer version of the above)
   workaround_upstream_15452.txt

[SnarkBoojum]

Trying to ompile coq-elpi gave me another needed modification, for the CoqMakefile system:
workaround_upstream_15452.txt

[SnarkBoojum]

Pfff... even with that, CoqMakefile.in still puts all files to install in the same FILESTOINSTALL list, and hence in the same directory...

[SnarkBoojum]

I'm wondering if I shouldn't have several configure-build for the various parts.

[SnarkBoojum]

No, there's no way I can get everything right : even if I get all of coq right (I can), that will still get anything using CoqMakefile.in wrong... So what am I left with? Coq in /usr/lib/coq and a symlink in /usr/lib/ocaml so ocaml libs get found, perhaps?

[SnarkBoojum]

For the record: I did the symlink trick to make everything work. Dirty, but working.

[ejgallego]

Thanks for all the work and feedback @SnarkBoojum ; I hope we can address this properly in the hacking session scheduled for the Winter Hackathon

[JasonGross]

@SnarkBoojum can you help me apply the symlink trick to https://github.com/JasonGross/coq-packaging/tree/master/debian? Since the findlib PR was merged, non-opam Coq (even when built without dune) seems to no longer be able to build plugins, see #15635

[SnarkBoojum]

Well, that was just a case of having a debian/my_package.links to create a symlink. But it's now obsolete since I reworked the packaging.

Why do you need to package coq for Ubuntu if there is already a Debian package for it?

[gares]

@JasonGross I think you can just cd debian/tmp/usr/lib/ocaml; ln -s ../coq-core . as a quick fix

[JasonGross]

Why do you need to package coq for Ubuntu if there is already a Debian package for it?

Is there a debian nightly build? I have packages for every released version of Coq that I can build and automatic builds of the tip of every branch, to use on CI

@gares, thanks, I'll try that

[SnarkBoojum]

@JasonGross ah, no, there's no nightly build ; but you could still use the debian/ directory above as a basis.

[JasonGross]

@SnarkBoojum Ah, yeah, I could do that. Where does it live? I don't see a link to your packaging in this issue thread.

[SnarkBoojum]

Sorry, I mixed with another thread on github (about another package entirely...). Here is a place where you can find everything.

[JasonGross]

@SnarkBoojum Thanks.

When I look at the diff between your control file and mine, I see

-Standards-Version: 3.9.5
+Standards-Version: 4.6.0
 Build-Depends:
- debhelper (>= 9),
+ bash (>= 5.0),
+ debhelper-compat (= 13),
+ dh-exec,
  dh-ocaml (>= 0.9.5~),
- ocaml-nox (>= 4.05.0),
- ocaml-best-compilers,
+ dh-python,
+ ocaml-dune,
+ ocaml-nox (>= 4.05),
+ ocaml-native-compilers,
  ocaml-findlib (>= 1.8.0),
- dune (>= 2.5.1),
- libfindlib-ocaml-dev (>= 1.8.0),
- libzarith-ocaml-dev (>= 1.10),
- liblablgtk3-ocaml-dev (>= 3.1.0),
- liblablgtksourceview3-ocaml-dev (>= 3.1.0),
- texlive-latex-extra,
- hevea (>= 1.10-7)
+ camlp5 (>= 6.14),
+ liblablgtk3-ocaml-dev,
+ liblablgtksourceview3-ocaml-dev (>= 3.0~beta8),
+ libnum-ocaml-dev,
+ libounit-ocaml-dev,
+ libzarith-ocaml-dev,
+ python3,
+ rsync,
+ tex-common

What's the reason you depend on camlp5 and libnum-ocaml-dev? I believe neither of these is required anymore. Any why not version dune and zarith and lablgtk3 and findlib with the minimum versions required by Coq? And why ocaml-dune rather than dune? And why debhelper-compat (= 13)?

[gares]

Also libfindlib-ocaml-dev is needed for master

[ejgallego]

What do we do with this bug, the problem and a workaround was proposed in #15452 (comment)

Dune assumes an "Opam" layout, that is to say, lib_root == ocaml_lib_root , so IMHO, if we want Dune to add a new directory for OCaml libraries IMHO we should move this bug to Dune's issue tracker.

[SnarkBoojum]

Well, now in Debian the coq libs are in /usr/lib/ocaml/coq... which might not be ideal but makes sense...

[ejgallego]

I think that's up to you, indeed, the OPAM layout is not generic enough IMHO (but makes sense for them to identify lib with lib/ocaml as they are an OCaml package manager) .

I wonder what Nix people think about how Dune installs things @vbgl @Zimmi48 ?

So I propose we either close this bug, or move it Dune's repos.

[SnarkBoojum]

According to the FHS, libraries can end up in various places depending on the usage -- and so do binaries (bin or libexec?) ; so indeed perhaps dune itself should be a bit less heavy-handed in its classification.

[ejgallego]

@SnarkBoojum Dune has the following notions of install sections https://dune.readthedocs.io/en/stable/dune-files.html#install-1

Indeed, once we use Dune for more languages, I think we should make lib to take an argument, so maybe let's move this bug to Dune's repo and discuss FHS support there.

Maybe the easiest is just to keep the current sections, but add an aditional ocaml_sublib variable, that can be set to OCaml, then OCaml libraries are installed in $lib/$ocaml_sublib, and for OPAM that variable is empty [then other languages can correctly use lib_root.

[JasonGross]

Is there any update on this? Has the bug been copied / moved to dune? Are there plans to support installing .vo files and OCaml files in different directories?

[ejgallego]

I'm afraid we had no cycles to move this ahead, but if someone wants to help with this I'm happy to help / support the intiative.

I wonder tho if the solution we proposed would work, for example:

• set configure coqlib to /usr/lib/coq
• install coq-stdlib with --libdir=/usr/lib, overriding the Debian default of /usr/lib/ocaml