Skip to content

Start a GoodDefaults file collecting recommended option settings. #19117

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Zimmi48 wants to merge 1 commit into from
Closed

Start a GoodDefaults file collecting recommended option settings. #19117

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions doc/changelog/11-corelib/19117-good-defaults-Added.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
- **Added:**
A GoodDefaults_2025 module setting various options to their recommended value,
see :ref:`the doc <good_defaults>` for more details
(`#19117 <https://github.com/rocq-prover/rocq/pull/19117>`_,
by Théo Zimmermann and Théo Winterhalter).
2 changes: 2 additions & 0 deletions doc/corelib/index-list.html.template
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,13 +163,15 @@ through the <tt>Require Import</tt> command.</p>

<dt id="Compat"> <a href="#Compat"><b>Compat</b></a>:
Compatibility wrappers for previous versions of Coq
and recommended options at the time of a given Rocq release
</dt>
<dd>
theories/Corelib/Compat/Coq818.v
theories/Corelib/Compat/Coq819.v
theories/Corelib/Compat/Coq820.v
theories/Corelib/Compat/Rocq90.v
theories/Corelib/Compat/Rocq91.v
theories/Corelib/Compat/GoodDefaults_2025.v
theories/Ltac2/Compat/Coq818.v
theories/Ltac2/Compat/Coq819.v
</dd>
Expand Down
14 changes: 14 additions & 0 deletions doc/sphinx/language/core/basic.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -400,6 +400,20 @@ The :term:`flag`, :term:`option` and :term:`table`
mechanisms are used to modify the behavior of Rocq more globally in a
document or project.

.. _good_defaults:

The default value of some settings is not the one that would be recommended
today for compatibility reasons. We provide a *good default* file in the Corelib
which can be imported as follows:

.. rocqtop:: in

From Corelib Require Import GoodDefaults_2025.

This file is versioned to account for the changes in recommendations as the Rocq

@jfehrle jfehrle Jun 26, 2025

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you expect these recommendations will over time become the default settings? If changes in the defaults are manageable for users, maybe that would be simpler.

@TheoWinterhalter TheoWinterhalter Jun 27, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be great, but it is much more work, as it can break things on the user side. For now it's what we recommend for new users / files.

practice evolves. The 2025 edition will remain available without change after
future versions are released.

.. _attributes:

Attributes
Expand Down
42 changes: 42 additions & 0 deletions theories/Corelib/Compat/GoodDefaults_2025.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)

(** * Good defaults 2025

File exporting recommended option settings at the time of releasing Rocq v9.1

*)

#[ export ] Set Default Goal Selector "!".

@proux01 proux01 Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 TheoWinterhalter Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 SkySkimmer Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@TheoWinterhalter TheoWinterhalter Mar 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 proux01 Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@TheoWinterhalter TheoWinterhalter Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@proux01 proux01 Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Again, the reverse

@SkySkimmer SkySkimmer Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@TheoWinterhalter TheoWinterhalter Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 proux01 Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


#[ export ] Set Asymmetric Patterns.

#[ export ] Set Keyed Unification.

(** The following affect people using [Universe Polymorphism]. *)

#[ export ] Set Polymorphic Inductive Cumulativity.

#[ export ] Set Typeclasses Default Mode "!".
Hint Constants Opaque : typeclass_instances.

Ltac Tauto.intuition_solver ::= auto with core.

(** Makes the behavior of [injection] consistent with the rest of standard
tactics.
*)

#[ export ] Set Structural Injection.

(** These three affect pepole that set [Implicit Arguments]. *)

#[ export ] Set Strongly Strict Implicit.
#[ export ] Set Maximal Implicit Insertion.

@Zimmi48 Zimmi48 Jul 7, 2025

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@anton-trunov seemed to defend the current default in his answer on Stack Overflow back in 2016: https://stackoverflow.com/questions/37211899/purpose-of-maximal-vs-non-maximal-implicit-arguments

That being said, I don't think the issue of having to add @ when you want to refer to a non-partially-applied constant is such a pain.

And on the other hand, the same @anton-trunov supported in 2021 the switch to maximally implicit arguments for lists (which didn't land) in #13069.

@proux01 proux01 Jul 7, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, 2016 is old

#[ export ] Set Contextual Implicit.
Loading