Stream: Coq Platform devs & users

Topic: Global vs. Export for Platform projects

Karl Palmskog (Mar 07 2022 at 08:25):

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?

Karl Palmskog (Mar 07 2022 at 08:26):

one obvious exception to export is for typeclass Hint Mode, where I think global should nearly always be used...

Karl Palmskog (Mar 07 2022 at 08:27):

why the locality thing may be more sensitive for Platform projects: we arguably risk breaking everyone's code by going from global to export

Paolo Giarrusso (Mar 07 2022 at 09:39):

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:

1. does the Hint Mode come in the same module as the class? Then it should be #[global] to be available wherever the class is used?
2. is it added by some other module or library? Then it should either be removed, be #[local], or be #[export].

Paolo Giarrusso (Mar 07 2022 at 09:43):

Ditto for other commands, like Arguments foo or Hint Opaque foo: there, you should check whether the command lives next to the foo constant.

Paolo Giarrusso (Mar 07 2022 at 09:48):

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.

Paolo Giarrusso (Mar 07 2022 at 09:59):

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.

• In Haskell, if elaboration of a term succeeds, it will give the same result regardless of context.
• Coq has other exceptions, but e.g. sections are local so they're easy to account for. The worst-case scenario is when a dependency adds a require, and your proofs break. However, global hints that live next to their subject seem to be safe: existing goals cannot mention the subject, so they should not be affected by the hint!

Enrico Tassi (Mar 07 2022 at 10:07):

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).

Paolo Giarrusso (Mar 07 2022 at 10:07):

(Added in a few corrections, sorry for the edits).

Paolo Giarrusso (Mar 07 2022 at 10:11):

@Enrico Tassi Thanks for the reminder; indeed, switching toexport will break FooLib.FooMod.subject.

Gaëtan Gilbert (Mar 07 2022 at 10:11):

even if you never required

no

Paolo Giarrusso (Mar 07 2022 at 10:11):

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.

Paolo Giarrusso (Mar 07 2022 at 10:12):

@Gaëtan Gilbert we can read that as "even if you never wrote an explicit Require yourself"

Pierre-Marie Pédrot (Mar 07 2022 at 10:12):

@Gaëtan Gilbert I think the intended meaning is if you never explicitly required

Enrico Tassi (Mar 07 2022 at 10:13):

You never wrote Require FooLib

Gaëtan Gilbert (Mar 07 2022 at 10:13):

also you don't need to mention the subject for it to be used, eg https://github.com/coq/coq/issues/15701

Enrico Tassi (Mar 07 2022 at 10:13):

but maybe Require BarLib which depends on FooLib

Enrico Tassi (Mar 07 2022 at 10:15):

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.

Karl Palmskog (Mar 07 2022 at 10:19):

@Enrico Tassi so what heuristics for global vs. export do you recommend beyond what's in refman?

Enrico Tassi (Mar 07 2022 at 10:21):

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.

Paolo Giarrusso (Mar 07 2022 at 10:22):

@Gaëtan Gilbert with the above rules, having Permutation declare Proper for cons definitely deserves at least #[export]

Enrico Tassi (Mar 07 2022 at 10:23):

@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.

Paolo Giarrusso (Mar 07 2022 at 10:23):

@Enrico Tassi the advantage is getting the right settings even if you forget Import.

Paolo Giarrusso (Mar 07 2022 at 10:24):

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.

Enrico Tassi (Mar 07 2022 at 10:25):

Then my question is: "why being-a-class is #[global] ?"

Karl Palmskog (Mar 07 2022 at 10:26):

yes, the example I have in mind is indeed:

Class Decision (P : Prop) := decide : {P} + {¬P}.
Global Hint Mode Decision ! : typeclass_instances.

Karl Palmskog (Mar 07 2022 at 10:26):

I don't see why one would ever want to use that class without that hint mode...

Enrico Tassi (Mar 07 2022 at 10:26):

Of course you want the scope of the class to be the same of the modes.

Enrico Tassi (Mar 07 2022 at 10:27):

pseudo:

Inductive Decision := ...
#[export] Exising Class Decision.
#[export] Hint ...

Karl Palmskog (Mar 07 2022 at 10:27):

but in this case, tons of people are using the class all over the place, possibly without exporting the module where Decision resides

Paolo Giarrusso (Mar 07 2022 at 10:27):

@Karl Palmskog agreed, and my only small counterpoint is that if I declare a Hint Mode for Decision, that one should be #[export].

Enrico Tassi (Mar 07 2022 at 10:27):

I know this is not how things are today, but I don't think going toward global is the right path

Pierre-Marie Pédrot (Mar 07 2022 at 10:28):

I makes sense to mark Hint modes of a global class as global.

Pierre-Marie Pédrot (Mar 07 2022 at 10:28):

since we don't have any non-global notion of classes, that's pretty much the only sane thing

Paolo Giarrusso (Mar 07 2022 at 10:30):

Again, except for orphan hint modes. If stdpp fixes the modes of a stdlib class, that should be export.

Karl Palmskog (Mar 07 2022 at 10:30):

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

Enrico Tassi (Mar 07 2022 at 10:30):

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 ?

Paolo Giarrusso (Mar 07 2022 at 10:31):

@Karl Palmskog For a less abstract example, iris changes the mode of a stdpp class :wink:

Pierre-Marie Pédrot (Mar 07 2022 at 10:31):

@Enrico Tassi I'm not even convinced that we want logical objects to be loaded globally by default

Pierre-Marie Pédrot (Mar 07 2022 at 10:31):

(in an ideal world, that is.)

Paolo Giarrusso (Mar 07 2022 at 10:32):

how do you keep type soundness otherwise?

Pierre-Marie Pédrot (Mar 07 2022 at 10:32):

I mean not in the kernel, but in the user-facing world.

Paolo Giarrusso (Mar 07 2022 at 10:33):

so if A := B, B is not loaded, and I unfold A, what happens?

Pierre-Marie Pédrot (Mar 07 2022 at 10:33):

Just like we have the Local modifier for definitions, we should not make available internal definitions or at least not easily

Paolo Giarrusso (Mar 07 2022 at 10:33):

local definitions are required/loaded, just not imported...

Pierre-Marie Pédrot (Mar 07 2022 at 10:33):

you get something like <internal> and you can't write it with a name

Pierre-Marie Pédrot (Mar 07 2022 at 10:34):

(the kernel see the "kernel name", it has just no "user qualid" in implem parlance)

Paolo Giarrusso (Mar 07 2022 at 10:34):

hm... that might be a separate discussion, except that "export classes" by itself is not enough.

Paolo Giarrusso (Mar 07 2022 at 10:35):

@Enrico Tassi a problem with #[export] Class is that there's almost nothing special about classes that matters for this discussion.

Paolo Giarrusso (Mar 07 2022 at 10:35):

to be sure, that idea would help with my concerns, but I can run typeclasses eauto for any goal and any database (like eauto).

Enrico Tassi (Mar 07 2022 at 10:35):

Yes, as I wrote up there I think all non-logical properties/objects should be export (and not global).

Paolo Giarrusso (Mar 07 2022 at 10:36):

but there's no non-logical property needed...

Paolo Giarrusso (Mar 07 2022 at 10:36):

"this is a TC" mostly means that _ will call typeclasses eauto for you.

Paolo Giarrusso (Mar 07 2022 at 10:36):

(or only?)

Gaëtan Gilbert (Mar 07 2022 at 10:37):

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

Enrico Tassi (Mar 07 2022 at 10:38):

I think we are mixing how you organize a library and the mechanisms for doing it.

Enrico Tassi (Mar 07 2022 at 10:38):

good mechanisms let you do it easily, but it is not that things magically works.

Enrico Tassi (Mar 07 2022 at 10:39):

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

Enrico Tassi (Mar 07 2022 at 10:42):

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.

Paolo Giarrusso (Mar 07 2022 at 10:42):

@Enrico Tassi I'm not sure I follow the last example

Enrico Tassi (Mar 07 2022 at 10:44):

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.

Karl Palmskog (Mar 07 2022 at 10:46):

@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

Gaëtan Gilbert (Mar 07 2022 at 10:48):

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

Paolo Giarrusso (Mar 07 2022 at 10:49):

and maintainers should try it in _new_ code before we start migration.

Paolo Giarrusso (Mar 07 2022 at 10:50):

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.

Karl Palmskog (Mar 07 2022 at 10:52):

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.)

Karl Palmskog (Mar 07 2022 at 10:54):

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

Théo Zimmermann (Mar 07 2022 at 10:55):

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).

Enrico Tassi (Mar 07 2022 at 10:56):

@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...

Karl Palmskog (Mar 07 2022 at 10:57):

@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...

Karl Palmskog (Mar 07 2022 at 10:58):

however, a Platform recommendation (to Platform projects) likely has more chance of getting through the inertia

Théo Zimmermann (Mar 07 2022 at 10:59):

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.

Paolo Giarrusso (Mar 07 2022 at 11:01):

indeed, especially if Coq extensions are appropriate (as @Enrico Tassi suggested).

Enrico Tassi (Mar 07 2022 at 11:04):

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.

Enrico Tassi (Mar 07 2022 at 11:05):

If we had to port to HB a development which was not using these explicit headers we would have cried more.

Paolo Giarrusso (Mar 07 2022 at 11:20):

“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.

Michael Soegtrop (Mar 07 2022 at 11:22):

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.

Enrico Tassi (Mar 07 2022 at 11:29):

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).

Paolo Giarrusso (Mar 07 2022 at 11:29):

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...

Paolo Giarrusso (Mar 07 2022 at 11:31):

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.

Paolo Giarrusso (Mar 07 2022 at 11:33):

this also means that without Import containing_module, all arguments of containing_module.foo are hidden, which probably has downsides.

Paolo Giarrusso (Mar 07 2022 at 11:34):

@Enrico Tassi I agree that "anything works well" isn't reasonable. We just need solutions with good ergonomics to exist and to be documented.

Paolo Giarrusso (Mar 07 2022 at 11:40):

(BTW, having to maintain import order explicitly is somewhat challenging, but that’s probably yet another topic)

Karl Palmskog (Mar 07 2022 at 12:03):

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...

Michael Soegtrop (Mar 07 2022 at 12:32):

@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.

Karl Palmskog (Mar 07 2022 at 22:11):

one step towards export in the Platform: https://github.com/coq-community/aac-tactics/pull/110

Karl Palmskog (Mar 07 2022 at 22:12):

universe unification issues with lists in AAC Tactics drive me nuts though... but seemingly unrelated to locality.

Enrico Tassi (Mar 08 2022 at 06:38):

The patch looks good, instances were already contained in modules making the adoption of export pretty natural imo.

Andrew Appel (Mar 15 2022 at 12:51):

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