When designing the support for composing coq theories intra-project, the main difficulty is how to determine whether a coq theory is installed publicly or not. For example, if we declare
(theories mathcomp.finset) , that will work fine in term of libraries that are in Dune's scope, but not if the library is installed globally. I'd likely hack a Filesystem -> theories map, but it feels a bit hacky.
Can't dune ask
coqc if library
foo is in his system wide scope? A la
ocamlfind query lib?
yeah, right now it should be equivalent to querying if the directory
/path/to/user-contrib/MyLibrary/Path/ exists, right?
Dune can indeed ask coq of ocamlfind for libs, however the problem here is that installing a lib breaks the substitution property, in the sense that if we define
(theory foo) which is recursive, so it also has module path
foo.bar, then when building against the installed copy,
foo.bar is available, but if you vendor that library it is not [dune will expose only foo]
this will be fixed in dune lang 2.0 by having
(legacy_theory ) and theory, and installing the proper meta-data, but we need a compat plan for 1.0
Indeed Karl, that's the plan, however I'm uneasy about the broken substitution property.
Is anyone exploring a local first model for coq libraries? I have little interest in installing anything globally. I find that it's a fragile workflow inspired by old school package managers. I'd be interested in only "installing" coq libraries per project.
So if there was a way to work with local libraries, that would be plenty sufficient at least for me.
@Rudi Grinberg installing the Coq dependencies of a project can take anywhere from a minute to several hours, and my universe is something like 50 Coq projects, many across several versions of Coq. How are per-project dependencies an improvement from, say, opam switches in workflows like this?
also, with the Coq platform, I think most (90%+) of people's dependencies will be in the platform installation (which will likely come via opam)
Is the coq compiler deterministic and produces relocatable artifacts? If so, all build time issues can be addressed by the dune cache.
Opam switches lose you some performance. The produced build plan isn’t as good and it makes it harder to use the cache because of the sandbox that’s imposed. They can be used to implement this workflow, but something on top needs to be done to make it fast.
I think that if the platform is going to be used, then you’ll quickly get to the point where multiple versions of the platform are going to be necessary. It seems that many coq projects are really sensitive to the versions of their dependencies
I have dunerized tons of projects in coq-community, but to think we will get anywhere close to, say 50% of large Coq projects using Dune in the near future would be unrealistic. This means that the Dune cache will not be generally available and opam switches (or Nix) will be the dominant mode of use of Coq for quite some time. I'm also very reluctant right now to actually use Dune in opam package definitions in the Coq opam archive, since they won't be compatible with future Dune versions and thus bitrot away (
coq_makefile+Make is much less likely to bitrot), see this comment by Emilio
as to whether
coqc is deterministic and produces relocatable artifacts, this would be a question for Emilio or other Coq devs, I suspect there may be some issues with that
Nix users don't need the dune cache. They already have a free dune cache for every nix package ;)
Opam switches lose you some performance.
I think the Coq community is currently less held back by performance numbers than by absence (dearth) of any kind of reasonable build automation and packaging for many projects.
I'm also very reluctant right now to actually use Dune in opam package definitions in the Coq opam archive, since they won't be compatible with future Dune versions and thus bitrot away (coq_makefile+Make is much less likely to bitrot), see this comment by Emilio
That would be a bit of a shame. The way we gained quick adoption of dune in OCaml is by keeping maximum compatibility with all the dune metadata written by users. I don't think it would be very hard to keep things compatible for coq projects either.
Last updated: Oct 16 2021 at 07:02 UTC