Coq refman currently recommends using export
locality wherever possible, e.g., for Instance
declarations. Do we want this for Platform projects as well? Some projects can't switch to export
since they want to be compatible with Coq before export
was available, but plugins should be fine, right?
one obvious exception to export
is for typeclass Hint Mode
, where I think global
should nearly always be used...
why the locality thing may be more sensitive for Platform projects: we arguably risk breaking everyone's code by going from global
to export
I don't think Hint Mode
is special, but I agree that "always use #[export]
" is a bad suggestion.
In your case, IMHO and as a rule of thumb:
Hint Mode
come in the same module as the class? Then it should be #[global]
to be available wherever the class is used?#[local]
, or be #[export]
.Ditto for other commands, like Arguments foo
or Hint Opaque foo
: there, you should check whether the command lives next to the foo
constant.
More generally, hints living together with their _subject_ can should be global [EDIT: rather than export]. Instances (EDIT: and Hint Resolve
) are trickier, because their subjects involve their entire statement, but Haskell's rules suggest the subjects include both the class, and the constants that are mentioned in the statement conclusion.
I haven't had the chance to develop this thought, but I think the goal of #[export]
is a (weaker) version of Haskell's coherence.
There is a caveat, Require
is recursive and you can mention the subject even if you never required nor imported the library where it comes from (you have to use a long name, like FooLib.FooMod.subject
). So IMO the only safe option is to have your users Import your library if they want to mention the subject. As soon as one write FooLib
for a non imported FooLib
then he relies on implicitly loaded hints (in a random order, since the transitivity closure of Require is not specified).
(Added in a few corrections, sorry for the edits).
@Enrico Tassi Thanks for the reminder; indeed, switching toexport
will break FooLib.FooMod.subject
.
even if you never required
no
And conversely, if a subject is meant for use qualified, you can't use #[export]
for related hints unless you manually lift them to an outer module (which can be error-prone). But that's probably a topic for the CEP on namespaces.
@Gaëtan Gilbert we can read that as "even if you never wrote an explicit Require
yourself"
@Gaëtan Gilbert I think the intended meaning is if you never explicitly required
You never wrote Require FooLib
also you don't need to mention the subject for it to be used, eg https://github.com/coq/coq/issues/15701
but maybe Require BarLib
which depends on FooLib
My impression is that #[global] is only safe if the hint also does not interfere with other hints, by making their failure slow for example. That is really hard to predict.
@Enrico Tassi so what heuristics for global
vs. export
do you recommend beyond what's in refman?
My understanding is that we should not use global at all ;-) In some sense by using global you lose control. With export you keep it.
@Gaëtan Gilbert with the above rules, having Permutation
declare Proper
for cons
definitely deserves at least #[export]
@Karl Palmskog another way to phrase it, which are the advantages of using global? That you don't need to write Import? It does not seem a big one.
@Enrico Tassi the advantage is getting the right settings even if you forget Import
.
in @Karl Palmskog 's example of Hint Mode
, a class without its modes is a terrible idea; and the modules you required explicitly might create goals using that class. Hint Opaque
can have the same problem.
Then my question is: "why being-a-class is #[global] ?"
yes, the example I have in mind is indeed:
Class Decision (P : Prop) := decide : {P} + {¬P}.
Global Hint Mode Decision ! : typeclass_instances.
I don't see why one would ever want to use that class without that hint mode...
Of course you want the scope of the class to be the same of the modes.
pseudo:
Inductive Decision := ...
#[export] Exising Class Decision.
#[export] Hint ...
but in this case, tons of people are using the class all over the place, possibly without exporting the module where Decision
resides
@Karl Palmskog agreed, and my only small counterpoint is that if I declare a Hint Mode
for Decision
, that one should be #[export]
.
I know this is not how things are today, but I don't think going toward global is the right path
I makes sense to mark Hint modes of a global class as global.
since we don't have any non-global notion of classes, that's pretty much the only sane thing
Again, except for orphan hint modes. If stdpp fixes the modes of a stdlib class, that should be export
.
right, in this case, the class is from base.v
in stdpp, which basically nobody exports, because the assumption is that you will import it yourself if you need it. But without the global, you are screwing over people who are transitive-only users of stdpp
One thing is the quickest fix to mess. I agree with that.
But the global/export thing seems to suggest that we want a system were logical objects are recursively loaded by require, while all non-logical properties are only available via import. Do we agree on this @Pierre-Marie Pédrot ?
@Karl Palmskog For a less abstract example, iris
changes the mode of a stdpp
class :wink:
@Enrico Tassi I'm not even convinced that we want logical objects to be loaded globally by default
(in an ideal world, that is.)
how do you keep type soundness otherwise?
I mean not in the kernel, but in the user-facing world.
so if A := B
, B
is not loaded, and I unfold A
, what happens?
Just like we have the Local
modifier for definitions, we should not make available internal definitions or at least not easily
local definitions are required/loaded, just not imported...
you get something like <internal>
and you can't write it with a name
(the kernel see the "kernel name", it has just no "user qualid" in implem parlance)
hm... that might be a separate discussion, except that "export classes" by itself is not enough.
@Enrico Tassi a problem with #[export] Class
is that there's almost nothing special about classes that matters for this discussion.
to be sure, that idea would help with my concerns, but I can run typeclasses eauto
for any goal and any database (like eauto
).
Yes, as I wrote up there I think all non-logical properties/objects should be export (and not global).
but there's no non-logical property needed...
"this is a TC" mostly means that _
will call typeclasses eauto
for you.
(or only?)
if you have an instance foo -> bar
it matters if foo is a class: if it is search gets called recursively, otherwise it stops there
I think we are mixing how you organize a library and the mechanisms for doing it.
good mechanisms let you do it easily, but it is not that things magically works.
if you define bar and you don't thing the users of your instances need to also use the instances for foo, then you designed your library badly
I mean, you can use Export for that, or something like that. I'm not saying we have the right tools/commands, but we don't ditch the "automagically pulls in all one may need" we will never manage to fix bugs like the one you posed earlier @Gaëtan Gilbert.
@Enrico Tassi I'm not sure I follow the last example
I'm saying that if I write a library about bar
and I find it useful to add a hint with a parameter foo
, I must also ensure that my users load the hints for foo
. Be it in the doc, or via Export WhereFooHintsAre
, or by some new mechanisms we don't have.
@Enrico Tassi but do you really propose: "export
everywhere right now, nearly no exceptions"? As a Coq library and plugin maintainer, I can't keep track of all design options and consequences, so I need some quite short slogan, and I think the current refman is too vague
I need some quite short slogan
"try stuff and see how it goes"
I don't think we fully understand export vs global yet
export is relatively new after all
and maintainers should try it in _new_ code before we start migration.
Enrico Tassi: I mean, you can use Export for that, or something like that. I'm not saying we have the right tools/commands, but we don't ditch the "automagically pulls in all one may need" we will never manage to fix bugs like the one you posed earlier @Gaëtan Gilbert.
@Enrico Tassi https://github.com/coq/coq/issues/15701 is not quite relevant, because it's a bug with #[export]
hints on explicit Import
.
OK, I'm prepared to try stuff and see how it goes in AAC Tactics (which uses global
nearly everywhere).
However, I was hoping that @Michael Soegtrop could weigh in on whether this is a good idea for the Platform in general (which explicitly wants to be dependable, reliable, etc.)
ideally, a working group in an imaginary "Coq Devs and Users Association" would have a marathon meeting which hammers out a set of slogans handed to maintainers, but we are apparently very long from there
It would be great if library maintainers were to start a Topic Working Group (https://github.com/coq/coq/wiki/Topic-Working-Groups) dedicated to experimenting and discussing such issues (with attendance from at least one member of the Coq dev team).
@Paolo Giarrusso if you put global it is even worse, since one may not be able to opt out (if you don't Import but the file is depended upon implicitly). Sure, these are not the kind of hints your were suggesting to make global...
@Théo Zimmermann unfortunately lib maintainers may not be able to reach any consensus that they even have a problem. The default state may be apathy here...
however, a Platform recommendation (to Platform projects) likely has more chance of getting through the inertia
The Platform recommendation should be based on experience, rather than arbitrary slogans, so if you can mobilize just a few library maintainers willing to experiment, that could help to reach a Platform recommendation. I think such maintainers can be found.
indeed, especially if Coq extensions are appropriate (as @Enrico Tassi suggested).
I could say what we do in mathcomp (we don't have TC, but some issues are similar), but that is horrible, so I would not make a slogan of it.
We require import all dependencies explicitly in the desired order. When we ported things to HB some metadata (like TC declarations) became "#[export] like" and we figured out were were missing a few deps, not too hard to fix, and nobody complained. But the headers are very ugly.
If we had to port to HB a development which was not using these explicit headers we would have cried more.
“Cry more”, or (1) write extra imports that depend on implementation details of my dependencies, and (2) suffer namespace pollution? “Require Export” can at least fix the first.
Karl Palmskog said:
ideally, a working group in an imaginary "Coq Devs and Users Association" would have a marathon meeting which hammers out a set of slogans handed to maintainers, but we are apparently very long from there
Actually I was think lately of having a special mailing list were important Coq Platform decisions are announced (and asked for opinions).
Regarding the export vs global topic: I must admit I haven't thought this through as yet - I guess I should.
About namespace pollution, it is again a matter of library design. In MC we use a patter of sub modules which are designed for not being imported and sub modules which are designed to be optionally imported. In some sense "Require Import foo" should work, it may add to your space a module Bar
you you are not supposed to import (so that you don't pollute), and a module Bar.ImportMe
that you can opt in. If you don't follow this discipline things don't work. It is not ideal, I just wanted to give an example of what I mean by "design the library", it is not just a matter of using the same scope attribute everywhere and it is a bit optimistic to hope it works no matter what the user does (forgets an import, does too many of them).
As an extra concern: "always use #[export]
" should also affect the implicit status of arguments — and not just those declared via Arguments
. So you'd basically need @Pierre-Marie Pédrot 's proposal of hiding non-imported constants...
But at least, you shouldn't get <internal>
, nor <internal> all_arguments
but containing_module.<internal>
, with the guarantee that Import containing_module
reveals all of foo args
.
this also means that without Import containing_module
, all arguments of containing_module.foo
are hidden, which probably has downsides.
@Enrico Tassi I agree that "anything works well" isn't reasonable. We just need solutions with good ergonomics to exist and to be documented.
(BTW, having to maintain import order explicitly is somewhat challenging, but that’s probably yet another topic)
Michael Soegtrop said:
Actually I was think lately of having a special mailing list were important Coq Platform decisions are announced (and asked for opinions).
I completely agree with the general idea, but I'd hope it will/would be based on Zulip or Discourse, rather than email...
@Karl Palmskog : let's discuss this in a separate thread. IMO a good old mailing list has advantages for low volume stuff. One should have both, Zulip to discuss things but also a mailing list to announce things. I imagine situations like we have to remove a package unless a new maintainer is found.
one step towards export
in the Platform: https://github.com/coq-community/aac-tactics/pull/110
universe unification issues with lists in AAC Tactics drive me nuts though... but seemingly unrelated to locality.
The patch looks good, instances were already contained in modules making the adoption of export pretty natural imo.
By the way, a few weeks ago I went through all of VST and converted almost everything (Hint Rewrite, Instance) to #[export]. Only a few things I had to leave as Global -- and those I could probably fix with more work. However, because I want to preserve compability with Coq 8.13 (for now), and because Coq 8.13 does not support locality annotations on certain things, I had to leave some of those as #[global] with a comment that they should be changed to #[export] as soon as VST abandons 8.13 compatibility.
In summary, I am strongly in favor of using #[export] instead of Global in Platform components.
Last updated: Oct 13 2024 at 01:02 UTC