Emilio Jesús Gallego Arias (Jun 23 2022 at 15:54): Emilio Jesús Gallego Arias (Jun 23 2022 at 15:54):Hi folks, I have been thinking a bit more about installed_theories for 1.0 version of the language, and this is what I think:
coq:lib to see where the library is installed, eventually supporting COQPATH-boot by default! That is to say, if we don't have (boot) in scope, we docoqc -boot so it won't auto-scan anythingcoq:lib, then we add -R $coqlib Coq and nothing for user-contrib.(theories declared, we find them as last resort in coq:contrib and then we add -Q $contrib/theory_path theoryThat should provide a good experience I think, WDYT?
Rudi Grinberg (Jun 23 2022 at 17:03):When you find a theory in contrib/, how do you add its transitive dependencies?
Rudi Grinberg (Jun 23 2022 at 17:04):For example, if we have:
(coq.theory (name a))
(coq.theory (name b) (theories a))
(coq.theory (name c) (theories b))
How do we make sure that c adds -Q for a if both a and b are installed (rather than local).
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:14):Ahhh true :(
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:15):For 1.1 version we will have the meta data
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:16):So we need (unfortunately) to trade:
(legacy_transitive_theories ...) until their deps are ported to Dune Emilio Jesús Gallego Arias (Jun 23 2022 at 17:16):pick your poison
Rudi Grinberg (Jun 23 2022 at 17:21):I have no issues with providing a reduced user experience for those that rely on coq makefile theories, but it's a real shame that we need to expose these sharp edges at all to those that stick to the dune only world.
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:26):I think we can only do that as a fallback
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:27):For people whose dep chain is fully dunerized we can do good, right?
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:27):we would only need to add the pain point for those that depend on non-dunerized deps
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:27):Yes, it is a shame, but can we do differently?
Rudi Grinberg (Jun 23 2022 at 17:30):Emilio Jesús Gallego Arias: For people whose dep chain is fully dunerized we can do good, right?
I don't see how this can be done with installing the necessary metadata in the dune-package
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:31):Then let's pick poison number one, even in the form of having to add to theories manually
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:31):I think only a small subset of users will have to do that
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:31):and will actually motivate people to port packages people are using
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:32):so if your dep is not using dune yet
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:32):you need to add the required libs
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:32):that's a PITA, but still much better than today situation with make
Rudi Grinberg (Jun 23 2022 at 17:32):I don't see how the poison is enough though. Even if the user is only relying on dune libraries, how does dune know the theory dependencies of installed theories?
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:32):let's start installing dune-package for Coq theories
Rudi Grinberg (Jun 23 2022 at 17:32):Emilio Jesús Gallego Arias said:
that's a PITA, but still much better than today situation with make
Sure, that's because that's a very low bar
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:33):in fact we can even install in two places for now
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:33):I am assuming here we can't transition everything to dune at the same time
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:33):I think my assumption is correct
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:33):we need to provide a path
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:33):yeah, transitions are a big pain
Rudi Grinberg (Jun 23 2022 at 17:33):Emilio Jesús Gallego Arias said:
let's start installing dune-package for Coq theories
Okay, but let's recall that this needs public names for lazy loading. E.g. so that when dune sees (theories foo.bar) it knows that it must look into the package of foo.
Rudi Grinberg (Jun 23 2022 at 17:35):Or an alternative lazy loading scheme I suppose
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:35):Umm, I think we discussed not allowing that?
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:35):ah sorry, I'm confused
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:36):we need two fields I think
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:36):maybe that's the best (legacy_theories ) and (theories ..)
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:36):with a proper (theories pkg:foo.bar)
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:36):Yeah it is tricky to retrofit
Rudi Grinberg (Jun 23 2022 at 17:38):The pkg:foo syntax works fine. Just keep in mind that it introduces redundancies. E.g.:
(theories mathcomp:mathcomp)
(not that I care very much about that)
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:38):wouldn't that be (theories coq-mathcomp-ssreflect:mathcomp.ssreflect) ?
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:38):yeah it looks pretty large
Rudi Grinberg (Jun 23 2022 at 17:39):ah yes, that's the full package name
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:39):but the package is named like that
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:39):and some packages like metacoq name the package different
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:39):I dunno
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:39):we can think of a nicer system
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:39):we could have just the package name mean all the theories?
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:39):but I dunno
Rudi Grinberg (Jun 23 2022 at 17:42):I suppose it's not so bad if we allow people to immediately pull more than one theory:
(theories (:coq-mathcomp-ssreflect mathcomp.ssreflect mathcomp.foobar ..))
Yes, we have no idea how people will organize tho, now that they can
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:45):for example, my port of compcert uses a single one, but I'm sure compcert devs would modularize that
Rudi Grinberg (Jun 23 2022 at 17:45):Sure, but note that they wouldn't be impacted by that. One can always omit the package name for theories in the dune project.
Rudi Grinberg (Jun 23 2022 at 17:46):E.g. inside mathcomp itself, one does not need to qualify the packages as dune already knows that all the theories belong to a single project.
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:46):they are actually 5 opam packages tho
Rudi Grinberg (Jun 23 2022 at 17:47):it still doesn't matter as dune has a package <-> theory map for every project
Ali Caglayan (Jun 23 2022 at 17:49):There is only one theory in user-contrib and that is user-contrib
Ali Caglayan (Jun 23 2022 at 17:50):I don't see any other way to support depending on user-contrib
Ali Caglayan (Jun 23 2022 at 17:50):We can at the same time introduce new installation layout for coq packages
Ali Caglayan (Jun 23 2022 at 17:50):We pass -Q user-contrib "" to coqc and that's it
Ali Caglayan (Jun 23 2022 at 17:50):That way if you write a theory in your theories field dune can find it from the proper place with all the correct metadata
Rudi Grinberg (Jun 23 2022 at 17:51):Here's another idea. It comes at the cost of making lazy loading less granular, and it doesn't work for private theories:
When trying to resolve mathcomp.foo in:
(coq.theory
(name a)
(package c)
(theories mathcomp.foo))
We look into the dune-project (or opam file) of the package c. In particular, the depends field. Then we eagerly load all the packages in that depends field and resolve mathcomp.foo from there.
Ali Caglayan (Jun 23 2022 at 17:59):Is it too late to go back to (public_name)?
Rudi Grinberg (Jun 23 2022 at 18:00):It's not enough. Public names work because they introduce a restriction on library/theory names
Rudi Grinberg (Jun 23 2022 at 18:01):E.g. theory foo(\.\alpha)* must always live in package foo.
Emilio Jesús Gallego Arias (Jun 23 2022 at 18:02):Ali Caglayan said:
We pass
-Q user-contrib ""to coqc and that's it
we can also pass -Q user-contrib/foo foo and have more control, no?
Emilio Jesús Gallego Arias (Jun 23 2022 at 18:03):How do rust or other large-scale build systems organize this?
Emilio Jesús Gallego Arias (Jun 23 2022 at 18:03):are packages 1:1 to libraries?
Rudi Grinberg (Jun 23 2022 at 18:04):Emilio Jesús Gallego Arias said:
are packages 1:1 to libraries?
I believe so
Emilio Jesús Gallego Arias (Jun 23 2022 at 18:04):that could make sense for Coq too
Emilio Jesús Gallego Arias (Jun 23 2022 at 18:04):maybe not
Emilio Jesús Gallego Arias (Jun 23 2022 at 18:04):ummm
Emilio Jesús Gallego Arias (Jun 23 2022 at 18:04):haha
Rudi Grinberg (Jun 23 2022 at 18:06):i don't think it's such a bad idea tbh.
Rudi Grinberg (Jun 23 2022 at 18:07):but note that users will still need to know about packages for plugins
Ali Caglayan (Jun 23 2022 at 18:07):Emilio Jesús Gallego Arias said:
Ali Caglayan said:
We pass
-Q user-contrib ""to coqc and that's itwe can also pass
-Q user-contrib/foo fooand have more control, no?
No because not every directory in user-contrib is a theory, some are multiple or even half. The only sound solution IMO is to treat the whole thing as a theory.
Ali Caglayan (Jun 23 2022 at 18:09):btw -Q user-contrib "" is actually what Coq is doing last time I checked. We obviously want to do this with -boot however.
Emilio Jesús Gallego Arias (Jun 23 2022 at 18:40):using more granular -Q for user-contrib does allow to fail when the user forgets deps and are installed, that's a big up for me. True, it allows the user to declare weird stuff for non-dunerized packages.
Emilio Jesús Gallego Arias (Jun 23 2022 at 18:40):So I think that's a tradeoff
Emilio Jesús Gallego Arias (Oct 14 2022 at 15:31):Summary of some possible rules:
Install
=======
1.0 version [for (package coq-foo) (theory Bar)]
lib/coq-foo/dune-package
lib/coq/user-contrib/Bar/Foo.v
1.1 version [for (package coq-foo) (theory Bar)]]
lib/coq-foo/dune-package
lib/coq-foo/Bar/Foo.v
Read
====
1.0 version [(theories Bar)]
will do -boot -Q lib/coq/user-contrib/Bar Bar
1.1 version [(theories coq-pkg1.Util coq-pkg2.Util)] ??
will do -boot -Q lib/coq-pkg1/Bar Bar -boot -Q lib/coq-pkg2/Bar Bar
=> error (likely)
2.0 version [(theories coq-pkg1.Util coq-pkg2.Util)] ??
will do -boot -Q lib/coq-pkg1/Bar coq-pkg1.Bar -boot -Q lib/coq-pkg2/Bar coq-pkg2.Bar?
This is the only real blocker to have a working dune setup for almost all Coq opam packages, hopefully we can implement it soon
Ali Caglayan (Jan 03 2023 at 11:48):I had a stab at implementing it over the holidays, but I ran into a few issues. It would be good to have a hacking session so we can discuss some of the difficulties I encountered.
Ali Caglayan (Jan 03 2023 at 11:51):One of the design issues at the moment is that the entire coq_lib logic relies on a theory coming equiped with basically a stanza. There are two ways we can go about changing this.
The first is a bit hacky but the second will require a lot more thought than I have been able to give it.
Ali Caglayan (Jan 03 2023 at 11:53):Since user-contrib files do not come with an associated dune or _CoqProject file we cannot really hold the hand of the user about setting up correct flags.
Ali Caglayan (Jan 03 2023 at 11:54):If I have a user-contrib theory A and a theory X that depends on A, then I have to match the flags in A (like -noinit, -indices-matter etc.)
Ali Caglayan (Jan 03 2023 at 11:54):That is perhaps a suitable cost for a user interested in doing advanced things like this so this is not a big worry.
Ali Caglayan (Jan 03 2023 at 11:55):A bigger worry would be how we partition user-contrib. If I have a theory that depends on say mathcomp, then there is no way for us to make sure we really meant that or more specifically mathcomp.algebra.
Ali Caglayan (Jan 03 2023 at 11:58):We can provide in the future, an alternative installation solution which has nice dune-package meta data using COQPATH or something. But that will require more future work.
Ali Caglayan (Jan 03 2023 at 11:59):My main worry with user-contrib is that we are trying to bend over backwards to support a flawed design, which makes our implementation more susceptable to bugs etc.
Ali Caglayan (Jan 03 2023 at 11:59):I'm still in favour of supporting it, but it is not easy so far.
Gaëtan Gilbert (Jan 03 2023 at 12:03):Ali Caglayan said:
If I have a user-contrib theory A and a theory X that depends on A, then I have to match the flags in A (like -noinit, -indices-matter etc.)
no? It's perfectly possible to use a noinit library together with a yesinit library
also possible to give up on indices matter although likely to be inconsistent
regardless I don't see why dune would care
Paolo Giarrusso (Jan 03 2023 at 12:06):Even if it should, it can't for user-contrib I guess, so it's one less problem
Emilio Jesús Gallego Arias (Jan 03 2023 at 14:44):I have in mind something much simpler like what is done for ocamlfind packages in the OCaml world, the infrastructure for "installed libs" is already there
Emilio Jesús Gallego Arias (Jan 03 2023 at 14:44):but yes we gotta do a hacking session
Rodolphe Lepigre (Jan 03 2023 at 15:48):Yeah, I agree with this. We should not reinvent the wheel: I would just define a Coq package to be an ocamlfind package containing a directory named coq-lib (or something similar) inside. The corresponding entry in the META file could then define both plugins and other Coq packages that are depended on.
I really think that before more hacking takes place, an installation format should be agreed upon (whether it is the one I hinted above, which I also think is what @Emilio Jesús Gallego Arias had in mind, or something else), so that we all understand where this is going.
I'd be happy to take part in a hacking session to discuss all this.
Emilio Jesús Gallego Arias (Jan 03 2023 at 15:50):Yes, indeed as noted above there are two orthogonal things:
I want to do 1 first, then migration of many packages should provide a good base for the design requirements of 2.
Ali Caglayan (Jan 03 2023 at 19:59):Gaëtan Gilbert said:
Ali Caglayan said:
If I have a user-contrib theory A and a theory X that depends on A, then I have to match the flags in A (like -noinit, -indices-matter etc.)
no? It's perfectly possible to use a noinit library together with a yesinit library
also possible to give up on indices matter although likely to be inconsistent
regardless I don't see why dune would care
From the point of view of Dune, if a user is importing a library (say HoTT) and a file fails to be imported due to having different compilation flags, this error will not be very useful. What I was hoping was that Dune would step in and tell the user that the library has differing flags.
Gaëtan Gilbert (Jan 03 2023 at 20:23):it will not fail to be imported
Ali Caglayan (Jan 03 2023 at 21:14):It will fail to get imported if I make a conflicting assumption to one in prelude. For example, reserving a notation level to be a different associativity.
Paolo Giarrusso (Jan 04 2023 at 05:53):does dune even check flag consistency across theory stanzas today?
Paolo Giarrusso (Jan 04 2023 at 05:54):either way, I think we all agree this can't be in scope for user-contrib since the info isn't there.
Ali Caglayan (Jan 04 2023 at 16:06):We don't check flag consistency, but it is something I would like to do, or at least make aparent to the user.
Last updated: Oct 13 2024 at 01:02 UTC