Controlling typing flags by SimonBoulier · Pull Request #9004 · rocq-prover/rocq

SimonBoulier · 2018-11-15T11:42:45Z

This PR allows to locally (with attributes) / globally (with Set/Unset commands) enable and disable:

the guard checking
the positivity checking
the check of universes (providing "type in type")

For this, the check_guarded typing flag is split into check_guarded and check_positive.

For the moment the syntax of commands is: Set Guard Checking, Unset Guard Checking, Set/Unset Positivity Checking, Set/Unset Universes Checking.
And for attributes: check_guarded, assume_guarded, check_positive, assume_positive, check_universes, type_in_type.

This PR also adds a Print Typing Flags command which prints the status of those three flags, and improves a bit the output of Print Assumptions.

E.g.

#[type_in_type] Definition T := let t := Type in (t : t).

Unset Guard Checking.
Fixpoint e (n : nat) : nat := e n.

Print Typing Flags.

Kind: feature

Added / updated test-suite

Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
Entry added in CHANGES.md.

Any comment welcome.

SkySkimmer · 2018-11-15T12:48:34Z

+
+let pr_typing_flags flags =
+  str "check_guarded: " ++ bool flags.check_guarded
+  ++ str "\ncheck_positive: " ++ bool flags.check_positive


Use an fnl() instead of \n.

Done. Thanks

Additionally, you can encapsulate the code into a box (e.g. a v 0 (...) to ensure that the fnl will align the next check exactly under the first check and not under the beginning of the box which encapsulates the call to pr_typing_flags (even if they probably coincide as the code is currently).

SkySkimmer · 2018-11-15T12:49:21Z

+Import b.
+(* Print Typing Flags. *)
+(* About T. *)
+(* Print Assumptions T. *)


Remove the comments or make this an output test.

SkySkimmer · 2018-11-15T12:55:51Z

    let evd = Evd.from_ctx ctx in
    Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
-      evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> Global.set_typing_flags original_typing_flag))


This seems quite fragile. Let's try to come up with a better model for how to do this kind of thing.

Maybe it should be handled more like how Program Mode is done.
OTOH

Require Import Program.Tactics. Program Lemma foo : Type. Proof. Test Program Mode. (* off *)

so that doesn't quite work.

In general attributes which act by setting a global option seem difficult to get right especially with proof-starting commands like Lemma.

Does it even make sense to have these typing flags in the global environment? Maybe we should pass them through the constant_entry/mind_entry/etc.This would mean handling them more like universe polymorphism, with an option which is used only to get the default value of the attribute. start_proof takes a goal_kind, if we put typing flags in there we may be able to make it work in the proof too.

Do other coq devs have any opinion?
Is it blocking or is it an "improvement request"?
Is goal_kind the right place for typing flags?

The right place will be in Declare.CInfo.t once #12372 is finished.

…ixpoints) and [check_positive] (for (co)inductive types).

Zimmi48 · 2018-11-19T21:08:24Z

      (see Section :ref:`positivity`). This condition ensures the soundness of
-      the inductive definition.
+      the inductive definition. The positivity checking can be disable using
+      the command :cmd:`Unset Positivity Checking` or the attribute


Suggested change

the command :cmd:`Unset Positivity Checking` or the attribute

the flag :flag:`Positivity Checking` or the attribute

Zimmi48 · 2018-11-19T21:09:03Z

-      the inductive definition.
+      the inductive definition. The positivity checking can be disable using
+      the command :cmd:`Unset Positivity Checking` or the attribute
+      ``assume_positive`` (see :ref:`gallina-attributes`).


Would be good to show a small example, which may also help explaining what the use cases are. Actually, since you have put this example in another section, a link to this section would also be fine (use .. seealso::).

Zimmi48 · 2018-11-19T21:12:10Z

+----------------------------
+
+.. cmd:: Set Guard Checking
+.. cmd:: Unset Guard Checking


You should instead document this as:

.. flag:: Guard Checking

Zimmi48 · 2018-11-19T21:12:35Z

+.. cmd:: Set Guard Checking
+.. cmd:: Unset Guard Checking
+
+   Enable/Disable the guard checking of fixpoints. Warning: this can break the


Flag to control...

Use .. warning::

Zimmi48 · 2018-11-19T21:13:49Z

+.. cmd:: Print Typing Flags
+
+   Print the status of the three typing flags: check of guard, check of positivity
+   and check of universes.


This command is not necessary as it redoes the job of Test Universe Checking, Test Positivity Checking, Test Guard Checking.

Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>

SimonBoulier · 2019-12-03T18:28:30Z

The part without attributes has been merged.

We use the new `Declare.Info` structure to uniformly add properties to the handling of constants. In this case, per-constant typing flags. The internal code may want to see some further refactoring, including pushing the flags down to `Safe_typing.add_constant` , but the changes in the interface should be definitive. This will allow rocq-prover#12539 and rocq-prover#9004 using attributes.

ejgallego · 2020-10-15T15:00:29Z

Rest implemented in #12586

We use the new `Declare.Info` structure to uniformly add properties to the handling of constants. In this case, per-constant typing flags. The internal code may want to see some further refactoring, including pushing the flags down to `Safe_typing.add_constant` , but the changes in the interface should be definitive. This will allow rocq-prover#12539 and rocq-prover#9004 using attributes.

We use the new `Declare.Info` structure to uniformly add properties to the handling of constants. In this case, per-constant typing flags. The internal code may want to see some further refactoring, including pushing the flags down to `Safe_typing.add_constant` , but the changes in the interface should be definitive. This will allow rocq-prover#12539 and rocq-prover#9004 using attributes. (cherry picked from commit b531ef3)

SimonBoulier requested review from a team, herbelin, mattam82, maximedenes, ppedrot and silene as code owners November 15, 2018 11:42

coqbot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 15, 2018

SimonBoulier mentioned this pull request Nov 15, 2018

[Work and discussion in progress] Add Unguarded syntax for (co)fixpoints and Assumed Positive for (co)inductive types. #7651

Closed

2 tasks

SkySkimmer reviewed Nov 15, 2018

View reviewed changes

SkySkimmer requested changes Nov 15, 2018

View reviewed changes

SimonBoulier force-pushed the typing_flags2 branch from 53f39ee to d1068bc Compare November 19, 2018 12:44

SimonBoulier requested a review from gares as a code owner November 19, 2018 12:44

SimonBoulier added 7 commits November 19, 2018 13:47

Split the [check_guarded] typing_flag into [check_guarded] (for (co)f…

04f278b

…ixpoints) and [check_positive] (for (co)inductive types).

Add [Print Typing Flags] command.

ef45cf8

Add guarded/positivity/universes attributes.

8a7d8d2

Set/Unset commands for typing flags

5000fb1

Fix Print Assumptions for Type In Type.

79c76ea

Add a file for typing_flags in the test-suite.

7977e0f

Add documentation for typing flags.

55a987d

SimonBoulier force-pushed the typing_flags2 branch from d1068bc to 55a987d Compare November 19, 2018 12:47

Zimmi48 added the kind: feature New user-facing feature request or implementation. label Nov 19, 2018

Zimmi48 requested changes Nov 19, 2018

View reviewed changes

Update doc/sphinx/language/gallina-specification-language.rst

738eb14

Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>

SimonBoulier mentioned this pull request Jun 3, 2019

Controlling typing flags with commands (no attribute) #10291

Merged

3 tasks

SimonBoulier closed this Dec 3, 2019

This was referenced Jun 18, 2020

RFC: Introduce the guard/unguard attributes for Fixpoint #12539

Closed

[declare] Refactor constant information into a record. #12372

Merged

ejgallego mentioned this pull request Jun 25, 2020

[declare] Allow custom typing flags when declaring constants. #12586

Merged

	the command :cmd:`Unset Positivity Checking` or the attribute
	the flag :flag:`Positivity Checking` or the attribute

Uh oh!

Conversation

SimonBoulier commented Nov 15, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

SimonBoulier commented Dec 3, 2019

Uh oh!

ejgallego commented Oct 15, 2020

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants