Following https://github.com/ocaml/dune/issues/6982 I've implemented some initial support for composition of installed theories https://github.com/ocaml/dune/pull/7047. Please try it out and report any thing that doesn't work.
Hi folks, this PR is almost ready, modulo some minor improvements and more tests.
That being the main blocker for 1.0 language release, we will start deprecating older coq lang versions
In particular there is a big incompatiblity between dune lang 0.8 and earlier versions.
Earlier versions added by default all of user-contrib, but newer versions don't.
So you need to explicitly add your library
To me, the main question for the 1.0 Coq dune lang is whether we should keep the implicit stdlib behavior enabled, or on the contrary, require users to declare Coq
in their list of theories.
I think I'd like a roadmap as follows:
theories
field, it is added implicitly with -R
, unless users set (stdlib no)
Coq
is added by default, this means that doing (theories Coq)
will add the stdlib with -Q, IMHO that's a very good thingActually Karl's comment on a different thread made me think that we should try to see if making include_subdirs qualified the default for 1.0
Include_subdirs qualified seems reasonable for 0.8?
Stdlib with -Q seems good but much more invasive
Paolo Giarrusso said:
Include_subdirs qualified seems reasonable for 0.8?
I'd depend if that's easy to implement
Paolo Giarrusso said:
Stdlib with -Q seems good but much more invasive
That can be an option, however we gotta start at some point IMHO.
But indeed there is a tension on how to push users to migrate to saner setups. But it is easy to keep -R for the stdlib if we want.
how do you get coqc to treat stdlib as -Q? I guess you have to avoid -coqlib?
There are 4 special paths now due to the stdlib as documented in corresponding Coq issues:
Require Prelude
Coq
to the list of theories that a theory depends onSo I guess we'll do a flag that when off requires users to both add Coq
to their list of theories and From Coq Require Import Prelude
or any other lib.
Gaëtan Gilbert said:
how do you get coqc to treat stdlib as -Q? I guess you have to avoid -coqlib?
@Gaëtan Gilbert in the current PR coqc
is always called with -boot
all libraries are the same for the internal Dune lib DB
except the above 4 cases
the way it works is not too complex, a Coq library database has a field for a theory that is the stdlib if detected
detection works as in Coq
at some point once the Dune code is stable we will hopefully share all that logic (as coq-lsp has a full copy of that logic too)
do you need theories mathcomp
or theories mathcomp.installed
? The linked PR docs seem to disagree on this
You use the same name, I guess Ali tried to highlight that the theory was installed.
It is not easy to document this stuff, as OCaml users know.
ack, sorry for the dup
Maybe the main changes to tell users are, when you bump to coq-lang 0.8 two things happen:
honestly, I'd still like a definition of the user-contrib -> DB
function
does user-contrib/foo/bar/baz
always let me use theories foo.bar.baz
(hence also theories foo.bar
and theories foo
?)
maybe I'll just ask @Rodolphe Lepigre to test this
the definition is simple, should be in the docs
each subdir gets a theory
yes, you can use that
of course if you have your own theories built by dune, you want to use what is in your stanza
if you want to enforce From Coq
or equivalent in Dune, the best would be to first establish this as a preferred idiom in Coq itself. For example, Require
from Stdlib without Coq
could be deprecated.
In my view, it's unfortunate to allow different sets of idioms in Coq itself and its build system...
More than enforcing it I was thinking of making it the default for 1.0, but the idea is that you can do (use_stdlib true)
and go back to the current behavior.
Was more of a "cosmetic" thing, there is not reason the stdlib needs to be handled specially
in particular when we have several developments active that doesn't use the stdlib
As of today you can get that behavior by setting (use_stdlib no)
, then adding Coq
to the list of theories
There is really no reason for Dune using -Q by default other than we considered that to be the sane default
but we can add a flag for Dune to use -R for some theories
So the stdlib getting -Q once it is handled like a regular library is just due to that default, not because anything important
For example, Require from Stdlib without Coq could be deprecated.
That would be nice, see issue https://github.com/coq/coq/issues/5257 and https://github.com/coq/coq/issues/16091, last time I tried the code made it difficult to implement, maybe it is easier now.
Personally the way I'd go about this to first finish the loadpath unification, then implement the deprecation.
The main trouble is that actually we want to preserve -R _only_ for the actual compiling library, but that is easier than I had thought actually.
The logic would go like-R
is allowed, but only if the module under compilation in that logical path.
otherwise warning
As long as the documentation is clear enough and that you can copy-paste some boilerplate to have Stdlib in scope and the prelude loaded by default (i.e., the boilerplate contains (coq.flags -rifrom Coq Prelude)
or something like that), then I wouldn't mind going as far as changing the default behavior to not even load the prelude. But it seems best to do this change in a Coq lang version < 1.0 so that you can evaluate the backlash and still have a possibility to revert for 1.0.
@Théo Zimmermann I was thinking more of just (use_stdlib true)
setting.
But indeed very good points; IMHO the experiment is worthwhile, at some point we need to deprecate the implict nature of the Coq namespace, so given that upcoming (coq lang 0.8)
is really 1.0 beta, maybe you are right and it makes sense to already set the default there, and try to understand the backslash. 0.8 will already be not very compatible for those using deps in user-contrib, so maybe it is best to do all the changes in a single bump instead of forcing users to go thru 2 steps.
WDYT?
On the backslash side I'd be suprised if someone would find that adding From Coq
to the stdlib imports makes their life harder, on the contrary that seems like an improvement in all cases, the logic now would be:
From
=> file in your theoryIt is a small thing but IMHO helps
if From Coq
is better, then I think it makes even more sense to deprecate non-prefixing of Coq
inside Coq proper
if you break something that's already deprecated, that's better backlash-wise in my view
From => comes not from your theory
Without From => file in your theory
That is not actually enforced though, you can still do Require Coq.Init.Logic.
even when stdlib is with -Q
doing a change in Coq lets you reuse all the warning technical infrastructure and deprecation social infrastructure — line numbers, -w -
/-w +
, deprecation period, ...
Yup doing a change in Coq would be great, but I'm afraid that's a lot more work
Gaëtan Gilbert said:
From => comes not from your theory
Without From => file in your theoryThat is not actually enforced though, you can still do
Require Coq.Init.Logic.
even when stdlib is with -Q
Yes, good point. So the correct statement is weaker.
Karl Palmskog said:
if you break something that's already deprecated, that's better backlash-wise in my view
There is not breaking per-se, just config options
I am fine having the default (stdlib yes)
, if there is a good motivation
We already did all the hard work in Dune so a sensible theory database is built
Coq
is in the database if a stdlib can be found
so all the flag does is to add Coq
by default to (theories )
, and mark it implicit
Composition for installed theories has been merged, it will be available in Dune 3.8 next week
A nice property of this PR is that it will avoid Coq scanning the whole user-contrib setup if you are only using a part of it. That could provide from little to significant speedups depending on the scenario
Last updated: Oct 13 2024 at 01:02 UTC