Stream: Coq devs & plugin devs

Topic: Debian packaging of Coq using Dune

Julien Puydt (Nov 13 2021 at 22:36):

I'm trying to move the Debian coq package from the Makefile-based build system to the dune-based one.

I can get most things to build in two commands:

        dune build -p coq-core,coq-stdlib,coqide
        dune build @stdlib-html

but installing is quirkier:

        dune install coq-core coq-stdlib coqide --destdir=... --prefix=... --libdir=...

seems to install the software side as expected in the destination directory ; but I could find how to make it install the document side -- the only place I found something about installing it was the install-doc-stdlib-html target in Makefile.doc -- does that mean that part isn't covered by dune?

Julien Puydt (Nov 13 2021 at 23:35):

Oh, and on a MIPSEL box, the compilation fails with:

dune build -p coq-core,coq-stdlib,coqide
File "topbin/dune", line 24, characters 7-15:
24 |  (name coqc_bin)
            ^^^^^^^^
Error: No rule found for topbin/coqc_bin.exe

(I tried it because the package using Makefile-based build was already failing on a few architectures for unclear reasons: https://buildd.debian.org/status/package.php?p=coq )

Julien Puydt (Nov 14 2021 at 11:03):

I just received a bug report ; the reason might be because they are bytecode architectures -- I'll see if compiling with dune improves things on that front

Julien Puydt (Nov 14 2021 at 13:59):

No, dune or not, it doesn't compile -- have those architectures been abandoned?

Gaëtan Gilbert (Nov 14 2021 at 14:09):

there's no "no dune" option

Julien Puydt (Nov 14 2021 at 14:13):

The package I pushed in Debian yesterday uses Makefiles using dune ; the version I'm working on uses dune directly

Julien Puydt (Nov 14 2021 at 14:13):

In either case, there's no magic to work on those platforms

Emilio Jesús Gallego Arias (Nov 14 2021 at 19:00):

Hi @Julien Puydt , thanks a lot for all the nice info and tests! Points:

• documentation: indeed, the documentation is for now installed only using the makefile system, we hope to fix that soon with a new feature in dune 3.0
• byte-only architectures: they are properly supported in dune however we likely added some assumption about a native object somewhere. I'd be happy to fix coq to work with byte-only, but the main problem is that we don't have a way to test that locally easily

Emilio Jesús Gallego Arias (Nov 14 2021 at 19:00):

if someone would point out how to create a byte-only opam switch I'll gladly try to have a look.

Emilio Jesús Gallego Arias (Nov 14 2021 at 19:00):

On the other hand, I'm unsure how Coq is useful in byte-only architectures, it is pretty slow for practical use

Emilio Jesús Gallego Arias (Nov 14 2021 at 19:00):

so maybe it should just be disabled?

Emilio Jesús Gallego Arias (Nov 14 2021 at 19:01):

Not sure how good the ocaml support is gonna be in upcoming years too, so if upstream is gonna abandon that too not sure it is worth spending a lot of manpower on that

Rudi Grinberg (Nov 14 2021 at 19:48):

@Emilio Jesús Gallego Arias it’s enough to remove ocamlopt from PATH to simulate a byte code only environment.

Julien Puydt (Nov 14 2021 at 20:10):

I can disable architectures, yes. If the support is lost upstream, there's little point

Emilio Jesús Gallego Arias (Nov 14 2021 at 20:17):

Rudi Grinberg said:

Emilio Jesús Gallego Arias it’s enough to remove ocamlopt from PATH to simulate a byte code only environment.

Thanks @Rudi Grinberg , will try and see

Julien Puydt (Nov 14 2021 at 20:19):

What's the license on coq.inria.fr/files/barron_logo.png ? I see many links to it, so I would like to put them in the package and link to a local copy

Julien Puydt (Nov 14 2021 at 20:20):

In fact, the whole generated doc has links for this and a few css files all over the place -- I'll want to make something that works offline

Julien Puydt (Nov 14 2021 at 20:30):

Ah, the logo is the same as ide/coqide/coq.png

Emilio Jesús Gallego Arias (Nov 14 2021 at 20:36):

@Hugo Herbelin do you remember who did the logo?

Emilio Jesús Gallego Arias (Nov 14 2021 at 20:36):

We should be able to license it the way we want I understand

Julien Puydt (Nov 14 2021 at 20:40):

If it's already in the sources, I have no license issue

Julien Puydt (Nov 14 2021 at 20:41):

for the list of .css linked to by the doc, things are less clear

Julien Puydt (Nov 14 2021 at 20:42):

doc/common/styles/html/coqremote seems to have a few .css -- I'll have to check if they're the same

Emilio Jesús Gallego Arias (Nov 14 2021 at 21:15):

@Julien Puydt doc install is pretty easy anyways, basically a straight copy of the artifacts

Hugo Herbelin (Nov 15 2021 at 10:08):

The CoqIDE variant of the logo seems to be due to Claude Marché. The css in doc/common/styles/html/coqremote are from Jean-Marc Notin (but are from LaTeX-generated documentation I believe). The file coqdoc.css if originally from the original author of coqdoc, that is Jean-Christophe Filliâtre. For the css in the sphinx-processed reference manual, git log says that Clément Pit-Claudel, Maxime Dénès and Paul Steckler were involved. Are there licence issues?

Théo Zimmermann (Nov 15 2021 at 11:28):

If files were committed in the repo, there's no reason to consider that there would be any license issue.

Julien Puydt (Nov 15 2021 at 12:29):

Well, there is for the reference manual, but I think those files are ok. I patch the stdlib documentation so it doesn't need internet access to be readable:

    # all the html files point to the same logo - ship it and point to it
    cp ide/coqide/coq.png _build/default/doc/stdlib/html/logo.png
    find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/files/barron_logo.png,logo.png,g"
    # all the html files point to some remote css - but they can be local too
    cp doc/common/styles/html/coqremote/modules/node/node.css _build/default/doc/stdlib/html/
    find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/modules/node/node.css,node.css,g"
    cp doc/common/styles/html/coqremote/modules/system/defaults.css _build/default/doc/stdlib/html/
    find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/modules/system/defaults.css,defaults.css,g"
    cp doc/common/styles/html/coqremote/modules/system/system.css _build/default/doc/stdlib/html/
    find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/modules/system/system.css,system.css,g"
    cp doc/common/styles/html/coqremote/modules/user/user.css _build/default/doc/stdlib/html/
    find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/modules/user/user.css,user.css,g"
    find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/sites/all/themes/coq/coqdoc.css,coqdoc.css,g"
    cp tools/coqdoc/style.css _build/default/doc/stdlib/html/
    find _build/default/doc/stdlib/html/ -name "*.html" | xargs sed -i -e "s,//coq.inria.fr/sites/all/themes/coq/style.css,style.css,g"

Last updated: Sep 09 2024 at 04:02 UTC