Stream: Coq Platform devs & users

Topic: Global vs. Export for Platform projects


view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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].

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:07):

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

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:11):

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

view this post on Zulip Gaëtan Gilbert (Mar 07 2022 at 10:11):

even if you never required

no

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Pierre-Marie Pédrot (Mar 07 2022 at 10:12):

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

view this post on Zulip Enrico Tassi (Mar 07 2022 at 10:13):

You never wrote Require FooLib

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Mar 07 2022 at 10:13):

but maybe Require BarLib which depends on FooLib

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:23):

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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Mar 07 2022 at 10:25):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Enrico Tassi (Mar 07 2022 at 10:26):

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

view this post on Zulip Enrico Tassi (Mar 07 2022 at 10:27):

pseudo:

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

view this post on Zulip 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

view this post on Zulip 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].

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 07 2022 at 10:28):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:31):

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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 07 2022 at 10:31):

(in an ideal world, that is.)

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:32):

how do you keep type soundness otherwise?

view this post on Zulip Pierre-Marie Pédrot (Mar 07 2022 at 10:32):

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

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:33):

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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:33):

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

view this post on Zulip Pierre-Marie Pédrot (Mar 07 2022 at 10:33):

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

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:34):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:36):

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

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:36):

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

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:36):

(or only?)

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Mar 07 2022 at 10:38):

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

view this post on Zulip Enrico Tassi (Mar 07 2022 at 10:38):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:42):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 10:49):

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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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...

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (Mar 07 2022 at 10:58):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 07 2022 at 11:01):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Mar 07 2022 at 22:11):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 30 2023 at 11:03 UTC