Controlling typing flags with commands (no attribute) #10291

SimonBoulier · 2019-06-03T15:19:56Z

This PR allows to enable and disable:

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

with some Set/Unset commands.

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

The syntax of commands is: Set Guard Checking, Unset Guard Checking, Set/Unset Positivity Checking, Set/Unset Universe Checking.

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.

This PR is #9004 without the attributes part which is trickier.

Kind: feature

Added / updated test-suite

Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).
Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

Zimmi48 · 2019-06-03T15:48:17Z

Note that you based this PR on an outdated branch.

SimonBoulier · 2019-06-04T14:47:32Z

@Zimmi48 Thanks, this is corrected

SkySkimmer

Seems OK barring the Print Assumptions related comment.

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

doc/sphinx/proof-engine/vernacular-commands.rst

printing/printer.ml

doc/sphinx/proof-engine/vernacular-commands.rst

SimonBoulier · 2019-06-06T14:47:59Z

Should be ok now.

SkySkimmer · 2019-06-06T15:09:49Z

The test suite fails as the checker doesn't take into account the typing flags associated to a constant/inductive.

SimonBoulier · 2019-06-07T12:19:23Z

Should be fixed :-)

checker/check_stat.ml

checker/checkInductive.ml

SimonBoulier · 2019-06-13T14:52:41Z

@ppedrot @SkySkimmer Can we merge this ?

SkySkimmer · 2019-06-13T15:20:44Z

The checker using local typing flags means it also tries to use native compile / VM (and fails in native compile in the test suite)
We don't want the checker using either AFAIK

SimonBoulier · 2019-06-20T14:22:44Z

Should be ok!

doc/sphinx/proof-engine/vernacular-commands.rst

Zimmi48 · 2019-06-20T15:08:23Z

Note that this PR is still missing a changelog entry (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for instructions).

SimonBoulier · 2019-06-20T15:38:56Z

I added the changelog, thanks for your advice @Zimmi48

SkySkimmer · 2019-07-02T13:00:17Z

checker/mod_checking.ml

+  (* Locally set typing flags for further typechecking *)
+  let orig_flags = env.env_typing_flags in
+  let cb_flags = cb.const_typing_flags in
+  let env = Environ.set_typing_flags {orig_flags with check_guarded = cb_flags.check_guarded;


This should be in the let env', such that you don't need to reset typing flags.

This is still todo

Indeed. Sorry for having missing that.

In fact I don't understand the lines 27-29:

let poly, env' = match cb.const_universes with | Monomorphic ctx -> false, env

Why is the env not enriched in the monomorphic case? Are the universes declared in the definition supposed to be yet here?
If so, why do we take env' instead of env in line 61?

let env = if poly then add_constant kn cb env else add_constant kn cb env'

This should be in the let env', such that you don't need to reset typing flags.

Actually never mind, we already do this resetting manipulation before the PR for the oracle so I'll clean it up in a follow up.

SkySkimmer

Needs rebasing due to conflict

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

type-in-type universes

Now all relevant typing_flags are taken in account by the checker. The different forms of assumptions are now printed by the checker.

SimonBoulier · 2019-08-16T16:19:28Z

@SkySkimmer I'm back and I rebased!

SkySkimmer · 2019-08-19T12:19:57Z

checker/mod_checking.ml

+  (* Locally set typing flags for further typechecking *)
+  let orig_flags = env.env_typing_flags in
+  let cb_flags = cb.const_typing_flags in
+  let env = Environ.set_typing_flags {orig_flags with check_guarded = cb_flags.check_guarded;


This is still todo

SkySkimmer

Considering this has been open for months and the changes don't look especially dangerous I'm going to assume other kernel/checker maintainers have nothing to say and merge without further delay.

SkySkimmer · 2019-08-20T10:48:00Z

checker/mod_checking.ml

+  (* Locally set typing flags for further typechecking *)
+  let orig_flags = env.env_typing_flags in
+  let cb_flags = cb.const_typing_flags in
+  let env = Environ.set_typing_flags {orig_flags with check_guarded = cb_flags.check_guarded;


This should be in the let env', such that you don't need to reset typing flags.

Actually never mind, we already do this resetting manipulation before the PR for the oracle so I'll clean it up in a follow up.

…ute) Reviewed-by: SkySkimmer Reviewed-by: Zimmi48

…d sized_typing plugin that did the same thing.

SimonBoulier requested review from herbelin, mattam82, maximedenes, ppedrot, silene and a team as code owners June 3, 2019 15:19

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

Zimmi48 added the kind: feature New user-facing feature request or implementation. label Jun 3, 2019

SimonBoulier force-pushed the typing_flags3 branch from b6c5dd0 to b870df1 Compare June 4, 2019 14:46

coqbot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 4, 2019

SkySkimmer requested changes Jun 4, 2019

View reviewed changes

Zimmi48 reviewed Jun 4, 2019

View reviewed changes

doc/sphinx/proof-engine/vernacular-commands.rst Outdated Show resolved Hide resolved

Zimmi48 added the needs: changelog entry This should be documented in doc/changelog. label Jun 4, 2019

SimonBoulier force-pushed the typing_flags3 branch from 393d598 to df9c390 Compare June 6, 2019 09:13

SkySkimmer added the needs: fixing The proposed code change is broken. label Jun 6, 2019

SkySkimmer reviewed Jun 7, 2019

View reviewed changes

checker/check_stat.ml Outdated Show resolved Hide resolved

SkySkimmer reviewed Jun 7, 2019

View reviewed changes

checker/checkInductive.ml Outdated Show resolved Hide resolved

SimonBoulier force-pushed the typing_flags3 branch from 8276314 to 7c44c10 Compare June 7, 2019 12:44

SimonBoulier force-pushed the typing_flags3 branch from 7c44c10 to da200a7 Compare June 19, 2019 14:26

Zimmi48 approved these changes Jun 20, 2019

View reviewed changes

doc/sphinx/proof-engine/vernacular-commands.rst Show resolved Hide resolved

doc/sphinx/proof-engine/vernacular-commands.rst Show resolved Hide resolved

SkySkimmer added part: kernel part: vernac High level command interpretation. labels Jul 2, 2019

SkySkimmer reviewed Jul 2, 2019

View reviewed changes

SkySkimmer self-requested a review July 2, 2019 13:06

SkySkimmer mentioned this pull request Aug 1, 2019

Fix #9294: critical bug with template polymorphism #9918

Merged

SimonBoulier added 9 commits August 16, 2019 11:43

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

bc4560f

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

Add [Print Typing Flags] command.

33f7877

Set/Unset commands for typing flags

abab878

Improve [Print Assumptions] for type-in-type and assumed positive.

889603e

Add a file for typing_flags in the test-suite.

6414a2a

Add documentation for typing flags.

de02e40

Universe Checking instead of Universes Checking

2470194

Fix Print Assumptions: Inductive types can have unsafe fixpoints or

3ae2b23

type-in-type universes

Fix typing_flags in the checker

d6d8229

Now all relevant typing_flags are taken in account by the checker. The different forms of assumptions are now printed by the checker.

SimonBoulier force-pushed the typing_flags3 branch from ac7ec74 to d6d8229 Compare August 16, 2019 09:54

coqbot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 16, 2019

SkySkimmer requested changes Aug 19, 2019

View reviewed changes

SkySkimmer self-assigned this Aug 20, 2019

SkySkimmer added this to the 8.11+beta1 milestone Aug 20, 2019

SkySkimmer approved these changes Aug 20, 2019

View reviewed changes

SkySkimmer added a commit to SkySkimmer/coq that referenced this pull request Aug 20, 2019

Merge PR coq#10291: Controlling typing flags with commands (no attrib…

9e1f800

…ute) Reviewed-by: SkySkimmer Reviewed-by: Zimmi48

SkySkimmer merged commit d6d8229 into coq:master Aug 20, 2019

ionathanch pushed a commit to ionathanch/coq that referenced this pull request Aug 28, 2019

Added typing flag for sized typing similar to issue coq#10291; remove…

1fb5e69

…d sized_typing plugin that did the same thing.

wilbowma pushed a commit to wilbowma/coq that referenced this pull request Aug 28, 2019

Added typing flag for sized typing similar to issue coq#10291; remove…

f276ea2

…d sized_typing plugin that did the same thing.

ionathanch pushed a commit to ionathanch/coq that referenced this pull request Aug 30, 2019

Added typing flag for sized typing similar to issue coq#10291; remove…

bcdcd0c

…d sized_typing plugin that did the same thing.

ionathanch pushed a commit to ionathanch/coq that referenced this pull request Sep 6, 2019

Added typing flag for sized typing similar to issue coq#10291; remove…

ed0d7f0

…d sized_typing plugin that did the same thing.

clarus mentioned this pull request Nov 1, 2019

TypingFlags as an OPAM package SimonBoulier/TypingFlags#1

Closed

ppedrot mentioned this pull request Feb 3, 2020

User-syntax for disabling positivity checking #5695

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Controlling typing flags with commands (no attribute) #10291

Controlling typing flags with commands (no attribute) #10291

SimonBoulier commented Jun 3, 2019 •

edited

Zimmi48 commented Jun 3, 2019

SimonBoulier commented Jun 4, 2019

SkySkimmer left a comment

SimonBoulier commented Jun 6, 2019 •

edited

SkySkimmer commented Jun 6, 2019 •

edited

SimonBoulier commented Jun 7, 2019

SimonBoulier commented Jun 13, 2019

SkySkimmer commented Jun 13, 2019

SimonBoulier commented Jun 20, 2019

Zimmi48 commented Jun 20, 2019

SimonBoulier commented Jun 20, 2019

SkySkimmer Jul 2, 2019

SkySkimmer Aug 19, 2019

SimonBoulier Aug 19, 2019

SkySkimmer Aug 20, 2019

SkySkimmer left a comment

SimonBoulier commented Aug 16, 2019

SkySkimmer Aug 19, 2019

SkySkimmer left a comment

SkySkimmer Aug 20, 2019

Controlling typing flags with commands (no attribute) #10291

Controlling typing flags with commands (no attribute) #10291

Conversation

SimonBoulier commented Jun 3, 2019 • edited

Zimmi48 commented Jun 3, 2019

SimonBoulier commented Jun 4, 2019

SkySkimmer left a comment

Choose a reason for hiding this comment

SimonBoulier commented Jun 6, 2019 • edited

SkySkimmer commented Jun 6, 2019 • edited

SimonBoulier commented Jun 7, 2019

SimonBoulier commented Jun 13, 2019

SkySkimmer commented Jun 13, 2019

SimonBoulier commented Jun 20, 2019

Zimmi48 commented Jun 20, 2019

SimonBoulier commented Jun 20, 2019

SkySkimmer Jul 2, 2019

Choose a reason for hiding this comment

SkySkimmer Aug 19, 2019

Choose a reason for hiding this comment

SimonBoulier Aug 19, 2019

Choose a reason for hiding this comment

SkySkimmer Aug 20, 2019

Choose a reason for hiding this comment

SkySkimmer left a comment

Choose a reason for hiding this comment

SimonBoulier commented Aug 16, 2019

SkySkimmer Aug 19, 2019

Choose a reason for hiding this comment

SkySkimmer left a comment

Choose a reason for hiding this comment

SkySkimmer Aug 20, 2019

Choose a reason for hiding this comment

SimonBoulier commented Jun 3, 2019 •

edited

SimonBoulier commented Jun 6, 2019 •

edited

SkySkimmer commented Jun 6, 2019 •

edited