Scoped options

[ppedrot]

Before this patch, Set and Local Set behaved the same outside of a section,
i.e. they disappeared at module closing. Now, setting an option without a
qualifier allows to activate it whenever the module it lives in is imported.
This is a much saner behaviour that allows to scope options properly.

Fixing the Coq source files was a mere matter of systematically replacing
every Set / Unset invokations by a corresponding Local Set / Unset command.

[aspiwack]

What does Global Set do? Does it set the option at Require? (I wrote this code, but I don't remember what I did)

If so, why choose that path rather than limit Global Set to work only at Import? (which would be "more backwards compatible" so to speak). (please note that I'm not saying that limiting Global is the right option, but it should probably be discussed).

[silene]

I would prefer if the semantics of Local/Global were uniform across all the commands rather than the current mess. Making Global Set work only at Import would introduce yet some new semantics. So I would either choose the status quo or Pierre-Marie's patch. If we ever feel one day that we are missing some peculiar semantics, it would be better to add a new locality modifier rather than overload an existing one.

[aspiwack]

If I had to redo everything, without any backward compatibility constraints I would do the following: Local would take a enclosing region (module, section) name: Local(region) Command and would end with that region. Global would carry on at Import (I don't remember why options can be set with a simple Require but I'd assume that it's not a very good reason). Without a keyword would make things local to the current module (and we could have Local without a region as well, like now, to be local to the last open region).

But we have to live with what we have.

[ppedrot]

I think that Global options acting at require time are an antipattern, but they have their reasonable uses for smelly hacks. So it should be discouraged to use them (e.g. issuing a warning) but the feature has to exist nevertheless.

[JasonGross]

I think there is one legitimate use case for side effects of require, and one use case that currently has no good alternative:

1. When a constant is defined in the current module, it should be possible to make changes to this constant (argument scopes, implicit status, simpl behavior, etc) which follows Require.
2. There is not currently a good way to make project-global changes when using _CoqProject, e.g., setting universe polymorphism, fixing the bug that makes intuition mean intuition auto with *, etc.

[ppedrot]

Your first use case is appealing, but I fail to see why you couldn't use some project-local file that you import everywhere in the second case. It sounds as a rather good practice to me, as this is a widespread pattern in many languages.

[maximedenes]

We discussed this at the WG, but I'm not sure we reached a clear conclusion. @ppedrot @silene is it ok to merge this as it is?

[silene]

It cannot be merged as is anyway, due to the unwarranted changes to plugins/extraction/CHANGES.

That being said, I don't think we reached a conclusion either. In particular, I think that there was a consensus that it is the semantics of Global, rather than the default one, that should be changed. And if it was so, applying this patch would become pointless, if not counter-productive. But perhaps I am over-interpreting the discussions at the meeting.

[maximedenes]

My feeling is that we all had in mind a semantics close to the one @aspiwack described in his second message above. The problem is how to get there, and what to do w.r.t. compatibility. Your point about adding a new vernacular rather than changing the current semantics may be the way to go.

What was less clear, was whether we really want to keep support for some options that have effect on Require (without Import). It seemed during the discussion that @ppedrot was supporting it, which was a surprise to me.

[silene]

I think I will bitterly regret this suggestion in a few years, but what about Export Set foo.

[ppedrot]

@silene I prefer this PR to be closed rather than introducing yet another syntax that we will have to support for ages, as well as a discrepancy in the semantics of local modifiers. One of the goal of the PR was to bring the semantics of various Local / Nothing modifier closer.

@maximedenes I don't actively advocate for Global having an effect at Require time, I just witnessed that some people relied on that in a way that was very hard to provide otherwise. So I think its use should be discouraged but the feature shouldn't be removed either.

The point of this PR is that it separates two behaviours that are merged as of today. It does not change the semantics of Local Set.

[maximedenes]

@ppedrot Are you ok with postponing this until we make up a clear plan for the scoping of options?

[ppedrot]

Fine, but I'm a bit concerned by the fact we're promoting a worse solution as a currently working alternative (i.e. Require-time effects).

[ejgallego]

There seems to be many tricky situations wrt Require vs Import, maybe we should really do a CEP and first write down/document all the behavior wrt to Libobject hooks.

As the discussion we had yesterday in Gitter, there are many many surprising things wrt to preservation of effects, so maybe a wider cleanup is required.

[RalfJung]

We desperately need something like this for Iris.

When developing a library, it is sometimes necessary or at least useful to set some Coq option to something other than the default. However, one wants to do that without forcibly inflicting this non-default choice on all of ones dependencies. Currently, this is pretty much impossible to do in a convenient way: What you can do, of course, is copy-paste all the options you are interested in into every single file. That's obviously a bad idea. So, instead we want some file, say options.v, to to all the relevant Set This. Set That.. Then we want this file to be imported everywhere, in a way that the options have effect in our files, but do not have effect in other projects using our files.

Global Set is not suited for this because it also affects every user of Iris. Set/Local Set are not suited either because then the options won't propagate even from option.v to Iris itself. So, currently, we have the choice of either living with Coq's default, or inflicting our non-default choice onto every Iris user. I assume this is also what @JasonGross referred to above.

If I understand this PR correctly, it would fix this situation. So, please, having something like this for 8.8 would be much appreciated :)

[Zimmi48]

We should make sure that this PR gets discussed at the next WG. I'm going to add it to the wiki page.

[ejgallego]

I'm afraid Scope handling is one of the most delicate issues in the current system. Quoting @silene who IMHO is spot on:

I would prefer if the semantics of Local/Global were uniform across all the commands rather than the current mess. Making Global Set work only at Import would introduce yet some new semantics. So I would either choose the status quo or Pierre-Marie's patch. If we ever feel one day that we are missing some peculiar semantics, it would be better to add a new locality modifier rather than overload an existing one.

thus we are talking here about the future of the module code and of libobject and thus of sections #6254

Not an easy topic.

[ppedrot]

@Zimmi48 This PR is a seasnake, we already discussed it like twice, in a WG and at the implementors' workshop. I'm not sure discussing it again would make any progress, except if I take hostages.

[ejgallego]

Indeed we don't need to discuss this PR but discuss the whole story about scoping in Coq.

Personally, I don't agree with this change as I'd rather fix the scoping mess at once and have the users suffer pain only once.

[Zimmi48]

If this PR is still controversial, would it be OK to close it and to propose a more specific solution to the clearly expressed and legitimate user need of @RalfJung? We may even start by creating an issue for this.

[ejgallego]

IMVHO closing the PR is not the right thing to do, I feel that some chat in person with the people involved on this is the way to go for now.

[Zimmi48]

But something must happen. You discourage me from putting this PR as needing discussion at the WG but in the same time you need some IRL discussion is needed, and there is no planned talk at the WG about the scoping of options...

[ejgallego]

I am with Pierre-Marie here in the sense that discussion in the WG is not gonna get anywhere. This needs development discussion, with a laptop and a few people looking into the code, etc...

[ejgallego]

As for an issue, I think #6254 should be good to discuss scoping. In fact #6254 should be titled "future of the sections and module system" as AFAICS the two are too intimately linked as of today as to discuss separately.

[maximedenes]

I am with Pierre-Marie here in the sense that discussion in the WG is not gonna get anywhere. This needs development discussion, with a laptop and a few people looking into the code, etc...

What would you think of having developer sessions at the WG, in the sense of small groups of people working on a topic? We could announce the topics, people would sign up so that we balance the size of groups,etc.

[ejgallego]

What would you think of having developer sessions at the WG, in the sense of small groups of people working on a topic? We could announce the topics, people would sign up so that we balance the size of groups,etc.

This is badly needed IMO, that is to say, a Coq "Hackaton", where code is written, as opposed to the "plenary" WG, where all developers are present.

We could however make Coq Hackatons fully independent of the WG; maybe we could try hosting one at IRIF? @herbelin @mattam82 ? Are you familiar with similar events in the Haskell community ?
https://wiki.haskell.org/Hackathon

[Zimmi48]

What about the carbon footprint? ;-) I would rather make the WG longer rather than create more events that would require people to travel even more.

[ejgallego]

IMHO these are separate events, attracting different kind of people; of course nothing is preventing us from placing them in a temporally contiguous time-frame.

[ejgallego]

But I will organize a Coq Hackaton some day for sure, independent from the WG. It will be in Paris [obviously as I'm based here], and people is not required to travel, indeed, it will be more of an event for newcomers to the Coq world.

[Zimmi48]

I would be really glad to see some Coq hackaton happening online. I don't think it would help in the present issue where some careful design is needed but it would have lots of other benefits. Did you see that Atom now allowing to have collaborative coding sessions? (I think we are disgressing) maybe this should become an independent discussion.

[RalfJung]

This has "Milestone: 8.8", what is the status? We'd still like to experiment more with Coq options in our libraries, but really can't because that would inadvertently also affect all our users.

[maximedenes]

I'd like to discuss this again during the WG. I'll try to prepare the discussion.

[ejgallego]

Discussion didn't converge a lot. Everyone agrees that we want this in, however there are some semantics / uniformity issues. It is very likely that any change in this direction will break many 3rd party developments, it would be thus convenient to have a clear roadmap about uniform behavior on Require/Import before implementing this.

A wiki page recollecting the existing semantics has been started at:
https://github.com/coq/coq/wiki/Default-Locality-Behavior-of-Commands

Meanwhile, a non-optimal workaround to avoid boilerplate in large projects is to use Load to set options locally.

[RalfJung]

it would be thus convenient to have a clear roadmap about uniform behavior on Require/Import before implementing this.

How realistic is it to fix this short-term? Sounds like the perfect being the enemy of the good.

It is very likely that any change in this direction will break many 3rd party developments

If the command that performs "Set only when imported, not when required" uses syntax that is invalid today, how can there be compatibility problems?

Meanwhile, a non-optimal workaround to avoid boilerplate in large projects is to use Load to set options locally.

IIRC, I tried this and it doesn't work well for libraries -- the Loaded file pretty much has to be local to the project. If, say, LambdaRust wanted to explicitly opt-in to use Iris' options, that would not work. I couldn't get Load to work for files that are installed. (See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/45 for some more information.)

Also, we were warned by @ppedrot that Load is a horrible hack and we shouldn't use it.

[ejgallego]

Sounds like the perfect being the enemy of the good.

I am sorry but we have to be careful here. We are talking of forcing every project to add non-backwards compatible modifications. So we cannot get it wrong.

IIRC, I tried this and it doesn't work well for libraries -- the Loaded file pretty much has to be local to the project. If, say, LambdaRust wanted to explicitly opt-in to use Iris' options, that would not work. I couldn't get Load to work for files that are installed. (See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/45 for some more information.)

I see a few problems there but none of them are related to Load. Indeed, coqdep should be fixed if it doesn't recognize Load.

Also, we were warned by @ppedrot that Load is a horrible hack and we shouldn't use it.

It was broken for a while but the status in master is much better than before, so it is usable with the restrictions stated in the manual.

Note that using Load is a hack, but I'm afraid that unless someone can propose and implement a uniform semantics for objects soon there is nothing better :(

[RalfJung]

I am sorry but we have to be careful here. We are talking of forcing every project to add non-backwards compatible modifications. So we cannot get it wrong.

The modification is backwards-compatible in the sense that the projects would continue to work with old versions of Coq.

However, I agree that's still not nice. From what I gathered, there was the proposal to instead use new syntax to have "Import-only options" (@ppedrot mentioned Export Set ...); this is why I brought it up in my comment above. That would have zero compatibility issues as no existing code uses this. It's also not like this introduces a new semantics; we already have things (like notations and coercions) that are only brought into scope by Import, not by Require.

I see a few problems there but none of them are related to Load. Indeed, coqdep should be fixed if it doesn't recognize Load.

Does it support giving a qualified path? Load iris.options. and Load lrust.options. should load different files. Last time I checked, the grammar enforced an ident, so this is not even well-formed syntax. (I can't find the reference for the development version online.)

[ejgallego]

Does it support giving a qualified path? Load iris.options. and Load lrust.options. should load different files. Last time I checked, the grammar enforced an ident, so this is not even well-formed syntax. (I can't find the reference for the development version online.)

Load needs a relate file path, as in Load "../options/foo.v". Not the best I know. As for the Export workaround, well, that could work but it is not 100% clear AFAICS.

[ppedrot]

The Export Set feature is on its way. I'm trying to come up with a patch elegant enough so as not to mess with the grammar to much. Hopefully this will be done before the freeze, I'm on it.

[ppedrot]

Closing this PR as it has been superseded by #6923.