Start a GoodDefaults file collecting recommended option settings.

[Zimmi48]

Follow-up of Zulip discussion at: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Better.20default.20options

Let's keep the momentum on this good idea. I've started populating this file with an easy one. What else should go in there and is not controversial? For instance, I saw Set Universe Polymorphism. being suggested in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Your.20favorite.20secret.20Coq.20option.3F, but is it already recommended for all users?

• Added changelog.
• Added / updated documentation.

[TheoWinterhalter]

Thanks for opening this!

I would say the relevant proposals are

• Primitive Projections
• Keyed Unification
• Asymmetric Patterns
• Uniform Inductive Parameters

For sure on the list should be the recommended config for type classes but I don't know it.

[Zimmi48]

If anyone disagrees with the proposed options, please voice your opinion.

BTW, @TheoWinterhalter, you may be able to push changes directly to this branch, in particular if you see the "Add more commits by pushing to the good-defaults branch on Zimmi48/coq." message above the CI status section.

[ppedrot]

I'm a bit wary of the Keyed Unification option, it's probably wildly undertested and thus very buggy.

[SkySkimmer]

We know primitive projections are pretty buggy too.

[Zimmi48]

OK. I advise that we avoid any controversial or insufficiently tested option. We could make a separate file ExperimentalGoodDefaults if we want to include potentially buggy options that we would still like to recommend in the long run.

[SkySkimmer]

I guess we should look through the deprecated warnings to see if any correspond to options that may be flipped.
For instance when we added export locality to hints we could have had an option to make it the default early, and enabled the option in gooddefaults.

[ppedrot]

But if we do that we need to version this file per release...

[Zimmi48]

But if we do that we need to version this file per release...

That's already the case here.

[SkySkimmer]

Versioning it is the whole point in fact. If we didn't version we may as well flip the global defaults.

[TheoWinterhalter]

Thanks @Zimmi48, but I actually don't want to push things, I'm merely listing options that might be worth adding, but I'm myself unsure whether they should, and I think it should be debated.

[proux01]

Since this is a draft, let's remove the milestone.

[Zimmi48]

There was a good reason for the milestone: the file has a version number. If it is not merged in this version, it should be renamed.

[proux01]

Then rename to 8.21 and put in 8.21+rc1 milestone.

[Zimmi48]

Why would I do that, exactly? The documented branching date for 8.20 is 2024-06-17. So if this PR is ready to merge before that date, it can still go in 8.20, no?

[proux01]

Sure

[TheoWinterhalter]

Coming back to this so it doesn't die. I think we would need have a flag to change default hint mode for typeclasses. Currently I think it's + for each argument, but it would be good to set it to ! iinstead. At least that's my understanding.
There is no way to change the default globally yet, correct?

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.

[TheoWinterhalter]

I see #19473 is relevant here.

[proux01]

I fear, this also means more chances to just remained ignored or simply unknown :(

[Zimmi48]

Sure, but this is a better middle ground to doing nothing, which has been what has been done for years for many of these defaults. There were even attempts at changing some of these defaults, which failed (e.g., #17811).

[proux01]

We have a better CI contract now, maybe that would help?

[TheoWinterhalter]

Now that #20820 is merged, I removed the corresponding line in the file.
I also added Set Keyed Unification to please @ppedrot.

[ppedrot]

I would also vouch to set the TC database opaque by default, see #20786.

[TheoWinterhalter]

Done.

[Zimmi48]

This should probably get merged. Then, we will have until the 9.2 release to nitpick the settings / improve the Good Defaults 2025 file before it is frozen forever.

[TheoWinterhalter]

Is there anything we can do to have this PR accepted?
I was thinking maybe the name could be Recommended2025 or RecommendedSettings2025 but I'd prefer it to be merged over bikeshedding (which we can do after, with other PRs).

[thomas-lamiaux]

@TheoWinterhalter concerning you ask to discuss this at Rocq Call

1. I want to stay I think it would be great.
2. imo GoodDefaults2025 or GooDefault9.1 would be a much better name when doing the import
3. have you tried it out ? Because for instance, I have tried importing the good default in List.v of the stdlib and I get the following bug that is very unclear to me. I guess some change with the typeclass 🤷 Whatever, the reason, I believe we should try to port the stdlib or a repo like that to ensure the GoodDefault actually works in practice. We don't want people to start a project only to realise mid-way they have to change back to the legacy cause the "good one" is bad
4. It is alright merging the good default with one less flag on or off, if it means merging sth that is works well
5. I am not expert in configuring project but how do you make it the default for your whole project ? Do you need to import it in every file ? Ideally, on the long run, this file should become the default, and people would need to import LegacyDefault9.1 to get the legacy default.

[SkySkimmer]

I guess that error is either from Set Keyed Unification. or from Hint Constants Opaque : typeclass_instances.
Probably the second one since @mattam82 had to do some corelib and some stdlib fixes when experimenting with it in #20786

[TheoWinterhalter]

I'm not sure passing the Stdlib with it is mandatory since those are breaking changes, hence why they're not already default I gather.

Also, I'm waiting for the Rocq call page of next week to be created to add the topic.

[SkySkimmer]

I think Hint Constants Opaque may not be a good idea because it will override any transparency hints from code before the import.

[thomas-lamiaux]

I'm not sure passing the Stdlib with it is mandatory since those are breaking changes, hence why they're not already default I gather.

I agree, I am just saying it is a good test to see what would have to change, for instance, I was not expecting the example above to fail, and I guess it probably should not ?

[andres-erbsen]

I do think we should hold any potential set of recommended settings to at least the written standard for changing the defaults -- having tried it on a few representative developments and still endorsing it. I have prematurely adopted "recommended" settings before and it was a colossal waste of time chasing down new issues they caused/surfaced (and now that file is almost empty).

In that spirit, I worry that the current Hint Mode options do not exactly inspire confidence #18078 (comment).

Having recently learned of Hint Constants Opaque : rewrite, I am hesitant to recommend it, but it seems at least to be intended to provide a less surprising behavior. I hear the concern about Hint Constants Opaque : typeclass_instances, and I wonder whether overriding per-constant configuration is indeed a good meaning for that flag & whether making these settings actual defaults would avoid that issue. But really, is the current behavior of this option ever desired?

More personally, I find Asymmetric Patterns and Default Goal Selector "!" to be inconvenient enough to turn them off, even though at least for the latter I get why it is desired and enforce similar restrictions manually on checked-in code.

[TheoWinterhalter]

After the Rocq call today it was decided that good defaults should be actual defaults and then use the compatibility layer to preserve backwards compatibility for a time.

In practice I suppose this means that none of the proposed options will become defaults and nothing will change but well, prove me wrong. 😉

[proux01]

In practice I suppose this means that none of the proposed options will become defaults and nothing will change but well, prove me wrong. 😉

We really should rely on the CI contract and let project authors do the porting here (and have an efficient assignee) otherwise the overlay cost will indeed be a definitive deterrent.

[andres-erbsen]

And we should do our part of the CI contract and actually validate the defaults we push on representative users on the CI (not necessarily all of it). The deterrent is there for a reason, to prevent unfortunate "off-by-default-but-recommended" additions like primitive projections or universe polymorphism.

Let's use Structural Injection as a test of this workflow. I've started local CI on #21766 but I'm not sure I'll get to going through stdlib and such any time soon.

[andres-erbsen]

...and trying out Set Asymmetric Patterns in corelib we find that it sometimes makes you need more patterns #21769

[proux01]

FWIW Asymmetric Patterns is used in the whole mathcomp ecosystem (mathcomp, Analysis, ssprove, jasmin, MetaRocq,...) for more than a decade so I guess we can consider it tested at scale, at least in that context (maybe often more math than PL oriented). (of course, corelib should still be ported)

[proux01]

I would strongly oppose making this the default since it forces the use of focusing which is considered a broken feature by many users. I agree we should make progress on proof-scripts structure checking but this isn't a satisfactory solution.

[TheoWinterhalter]

I don't understand this comment? How is it broken? To me Rocq is unusable without this option and I don't consider a Rocq script robust if it doesn't work without this option.

I think this shouldn't even be an option and should be enforced.

[SkySkimmer]

mathcomp people use Set Bullet Behavior "None". so they have no way to focus

[TheoWinterhalter]

Yes, using this flag should be paired with a different option for default goal selector. Although I still believe it's the wrong behaviour.

Technically they still have a way to focus with 1:{ }. But I agree you don't want to enforce that.

[proux01]

That's the point, the current semantics of bullets is broken, for bad historical reasons.

[TheoWinterhalter]

But isn't that only broken if you use Set Bullet Behavior "None".?

[proux01]

Again, the reverse

[SkySkimmer]

It's not broken, you just don't like it.

[TheoWinterhalter]

No? If you do not have any bullet behaviour, bullets are just like comments. So they are counterproductive because they give you the fake impression that they carry meaning. Sure they contain intention but that's it.
Worse, the interface then always shows you all goals, which is a nightmare. (And coq-lsp perpetuates this nightmare even when you use focusing.) You essentially get lost in the structure of the proof.

When bullets are meaningful and the default goal selector is none, then they work as they should and force you to write robust proof scripts. And structure is ensured by the system. I've used it for years, and I teach my students to use it.

[proux01]

Well, it broke a large existing code base by reusing its syntax with an incompatible semantics, it's hard not to call that broken.
And again, no need to convince me that a proof script structure checking is a desirable thing.