Emilio Jesús Gallego Arias (Jul 08 2020 at 11:24): Emilio Jesús Gallego Arias (Jul 08 2020 at 11:24):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.
WDYT folks?
Enrico Tassi (Jul 08 2020 at 12:35):Can't dune ask coqc if library foo is in his system wide scope? A la ocamlfind query lib?
Karl Palmskog (Jul 08 2020 at 13:16):yeah, right now it should be equivalent to querying if the directory /path/to/user-contrib/MyLibrary/Path/ exists, right?
Emilio Jesús Gallego Arias (Jul 08 2020 at 13:25):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]
Emilio Jesús Gallego Arias (Jul 08 2020 at 13:25):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
Emilio Jesús Gallego Arias (Jul 08 2020 at 13:26):Indeed Karl, that's the plan, however I'm uneasy about the broken substitution property.
Rudi Grinberg (Aug 18 2020 at 04:23):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.
Karl Palmskog (Aug 18 2020 at 11:46):@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?
Karl Palmskog (Aug 18 2020 at 11:47):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)
Rudi Grinberg (Aug 18 2020 at 16:55):Is the coq compiler deterministic and produces relocatable artifacts? If so, all build time issues can be addressed by the dune cache.
Rudi Grinberg (Aug 18 2020 at 16:57):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.
Rudi Grinberg (Aug 18 2020 at 16:58):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
Karl Palmskog (Aug 18 2020 at 19:30):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
Karl Palmskog (Aug 18 2020 at 19:33):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
Rudi Grinberg (Aug 18 2020 at 19:36):Nix users don't need the dune cache. They already have a free dune cache for every nix package ;)
Karl Palmskog (Aug 18 2020 at 19:40):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.
Rudi Grinberg (Aug 18 2020 at 19:40):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: Jun 04 2023 at 23:30 UTC