Coq Call 2022 05 25

• May 25th, 2022, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• 8.15.2

• META files / plugins and dune (Ali)

  • Today there are two loading mechanisms for loading plugins:

    • The "legacy" method, which searches for a plugin using its private name.
    • The "new" method, which searches for a plugin using its public name.

  • What's the problem?

    • The new method relies on the existance of a META file for mapping public names to private names.
    • This means in principle, and entire package needs to be built before its META file is generated. This means that building .v files against core plugins will lose their incrementality since our plugins are part of the coq-core package.
    • In a dune build, the META file is part of the _build/install directory. (In Ali's opinion) it is fragile to rely on it's existance.
      • Technically specifying the META file as a build target doesn't work, since dune doesn't know how to build it directly.
      • The only supported (by dune) way of relying on this file is to use the (package coq-core) dependency, however this will suffer from the same loss of incrementality. There is also a question of "What is a plugin doing in a core-package if it isn't "core"").

  • Solutions?

    • dune generates a "local" version of the coq-core META file called META.coq-core before the entire package is built. This could be used instead but there is a snag:

      The directory layout of this META file is different from the one in the install directory. This leads to findlib not being able to read it.

      We could in principle, patch dune to remedy this, but this seems like the wrong direction. (Ali says:) It seems silly to rely on the layout of the install directory during a build.

      Therefore it seems sensible to Ali to submit a findlib patch which fixes findlib not being able to read META.coq-core.

      See https://github.com/ocaml/dune/issues/5767 the problem is that the expected content of META.package (produced in _build/default/) and bla/META (put in _build/install/...) are different with the first needing a directory field. However dune is producing them by symlinking the 2nd to the 1st, as long as dune does that it's going to be wrong. IMO (Gaëtan) dune is where the bug is, a findlib patch is not the right solution.

    • Stop putting plugins in (package coq-core).

      • Ali says: If plugins are really to be "plugged in" to a "core" version of Coq, what business do they have in this package?
      • If we seperate them out into seperate packages, users will not have to know (umbrella packages).
      • It will allow for builds to be incremental. If you need ltac, then dune will know to build only coq-core and the ltac package.
      • We would also stop using the legacy loading method and have a single loading method for plugins.
      • The downsides are:
        • There are now more packages.
        • The legacy loading method is lenient.

    • Stop relying on META files to do name mapping. Ali: If dune can map between public and private names without issue, then we probably ought to be able to.

Notes

• 8.15.2 done by Gaëtan early next week, Changelog PR done first to keep it in 8.16

• configure PR. We would rather have a way for configure to be lax when it can't check dependencies, but having a specific thing for lablgtk is too restrictive. The debian package should rather be fixed in this case, e.g. by patching Coq's configure.

• plugins and findlib: the fix should be in dune, Emilio thinks it is doable.

• dune plugin tutorial examples to see how it works and what's to improve

• not urgent for 8.16, coq_makefile plugins do work. dune plugins require more work.