Adding a delimiter for opening a scope only temporarily #14928

herbelin · 2021-09-24T08:33:29Z

Kind: feature

Reopening of #9123.

This adds a syntax term%_scope to tell to activate scope scope only for the immediate subterm. This allows for instance to define notations which activate type_scope only temporarily as in:

Notation "{ x  |  P }" := (sig (fun x => P%_type)) : type_scope.
Check fun P Q => { x : nat & P x * Q x }.

Note: We may want this to apply also to Arguments. Unfortunately, in Arguments, % has already the meaning of this new %_ so we add %_ as a synonym of % there and deprecate %. In a few versions we will make % in Arguments error and in the following version give it the same semantics as in terms.

Added / updated test-suite

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

Overlays to be merged before the PR

Overlays to be merged in sync with the PR

proux01 · 2021-09-24T08:38:22Z

@herbelin is the above text of the PR still current? it doesn't seem to reflect the state of the discussion in #9123

proux01 · 2021-09-24T08:38:53Z

@ejgallego do you still want to assign this one? Otherwise, I'll assign to myself.

herbelin · 2021-09-24T08:41:20Z

@proux01 : title was wrong. I fixed it. The PR needs maturation. Without time to work currently on it, I moved it to draft.

coqbot-app · 2021-09-24T09:11:12Z

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

coqbot-app · 2021-11-08T02:13:27Z

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 · 2021-11-08T08:08:10Z

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

coqbot-app · 2021-12-14T02:17:05Z

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 · 2022-01-13T02:20:48Z

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

proux01 · 2023-11-03T14:50:16Z

@Blaisorblade is it ok to merge this as it is or do you want it to be further discussed?

Blaisorblade · 2023-11-03T22:45:35Z

Thanks for clarifying, I understand the concern.

proux01 · 2023-11-04T11:56:50Z

Thanks, I'll merge next week if there are no other comments.

In order to avoid ambiguities between the `%<scope>` and the `%_<scope>` notations.

The notation is "term%_scope" (instead of "term%scope" for opening a scope applying to all iterated subterms).

Currently % in Arguments yield a deprecation warning. In a few version, we'll make it an error and in next version give it the same semantics as in terms (i.e., deep scope opening for all subterms rather than just temporary opening).

proux01 · 2023-11-10T08:01:09Z

@coqbot merge now

coqbot-app · 2023-11-10T08:01:14Z

@proux01: Please take care of the following overlays:

14928-herbelin-tmp-scope-delimiter.sh

Adapt to coq/coq#14928

Co-authored-by: Yishuai Li <liyishuai.lys@alibaba-inc.com>

proux01 · 2023-11-10T13:03:10Z

And another almost five years old PR merged

herbelin added kind: feature New user-facing feature request or implementation. part: notations The notation system. labels Sep 24, 2021

herbelin added this to the 8.15+rc1 milestone Sep 24, 2021

herbelin mentioned this pull request Sep 24, 2021

Adding a delimiter for opening a scope only temporarily + applications to notations for ex/sig/sigT #9123

Closed

3 tasks

herbelin changed the title ~~Master+tmp scope delimiter~~ Adding a delimiter for opening a scope only temporarily + applications to notations for ex/sig/sigT Sep 24, 2021

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 9, 2021

coqbot-app bot added the stale This PR will be closed unless it is rebased. label Nov 8, 2021

herbelin force-pushed the master+tmp-scope-delimiter branch from 2230b00 to 30a0dfb Compare November 8, 2021 07:31

coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Nov 8, 2021

SkySkimmer added the needs: fixing The proposed code change is broken. label Nov 8, 2021

SkySkimmer removed this from the 8.15+rc1 milestone Nov 8, 2021

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 11, 2021

coqbot-app bot added the stale This PR will be closed unless it is rebased. label Dec 14, 2021

coqbot-app bot closed this Jan 13, 2022

proux01 reopened this Oct 5, 2023

proux01 force-pushed the master+tmp-scope-delimiter branch from 30a0dfb to f749faf Compare October 5, 2023 15:50

proux01 force-pushed the master+tmp-scope-delimiter branch from f749faf to 71a7225 Compare October 5, 2023 15:55

proux01 added the needs: changelog entry This should be documented in doc/changelog. label Oct 6, 2023

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 6, 2023

liyishuai pushed a commit to proux01/QuickChick that referenced this pull request Nov 9, 2023

Adapt to coq/coq#14928

43a9f1c

proux01 added a commit to proux01/perennial that referenced this pull request Nov 9, 2023

https://github.com/coq/coq/pull/14928

589fc0e

proux01 mentioned this pull request Nov 9, 2023

Adapt to https://github.com/coq/coq/pull/14928 mit-pdos/perennial#55

Merged

RalfJung pushed a commit to mit-pdos/perennial that referenced this pull request Nov 9, 2023

https://github.com/coq/coq/pull/14928

343c081

proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 9, 2023

proux01 force-pushed the master+tmp-scope-delimiter branch from 37dbf3e to 24c2712 Compare November 9, 2023 12:38

coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Nov 9, 2023

proux01 and others added 6 commits November 9, 2023 13:39

Forbid scope names and delimiters to start with an underscore

8e950e3

In order to avoid ambiguities between the `%<scope>` and the `%_<scope>` notations.

Adding ability to use delimiters to set a scope only temporarily.

e6c7fd4

The notation is "term%_scope" (instead of "term%scope" for opening a scope applying to all iterated subterms).

Adding deprecation category for 8.19

606e106

Add overlays

a78923b

Add changelog

72509e0

proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 9, 2023

proux01 force-pushed the master+tmp-scope-delimiter branch from 24c2712 to 72509e0 Compare November 9, 2023 12:40

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 9, 2023

coqbot-app bot merged commit 04162a1 into coq:master Nov 10, 2023
8 checks passed

LasseBlaauwbroek added a commit to coq-tactician/coq-tactician that referenced this pull request Nov 10, 2023

Merge pull request #68 from proux01/coq_14928

2b25be7

Adapt to coq/coq#14928

ppedrot added a commit to coq-community/vscoq that referenced this pull request Nov 10, 2023

Merge pull request #681 from coq-community/coq_14928

907bed4

Adapt to coq/coq#14928

ppedrot added a commit to ejgallego/coq-serapi that referenced this pull request Nov 10, 2023

Merge pull request #366 from proux01/coq_14928

0fa1c72

Adapt to coq/coq#14928

liyishuai added a commit to QuickChick/QuickChick that referenced this pull request Nov 10, 2023

Adapt to coq/coq#14928 (#342)

7120bb5

Co-authored-by: Yishuai Li <liyishuai.lys@alibaba-inc.com>

zeldovich pushed a commit to mit-pdos/perennial that referenced this pull request Nov 10, 2023

https://github.com/coq/coq/pull/14928

5370109

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Adding a delimiter for opening a scope only temporarily #14928

Adding a delimiter for opening a scope only temporarily #14928

herbelin commented Sep 24, 2021 •

edited by proux01

proux01 commented Sep 24, 2021

proux01 commented Sep 24, 2021

herbelin commented Sep 24, 2021

coqbot-app bot commented Sep 24, 2021

coqbot-app bot commented Nov 8, 2021

coqbot-app bot commented Nov 8, 2021

coqbot-app bot commented Dec 14, 2021

coqbot-app bot commented Jan 13, 2022

proux01 commented Nov 3, 2023

Blaisorblade commented Nov 3, 2023

proux01 commented Nov 4, 2023

proux01 commented Nov 10, 2023

coqbot-app bot commented Nov 10, 2023

proux01 commented Nov 10, 2023

Adding a delimiter for opening a scope only temporarily #14928

Adding a delimiter for opening a scope only temporarily #14928

Conversation

herbelin commented Sep 24, 2021 • edited by proux01

Overlays to be merged before the PR

Overlays to be merged in sync with the PR

proux01 commented Sep 24, 2021

proux01 commented Sep 24, 2021

herbelin commented Sep 24, 2021

coqbot-app bot commented Sep 24, 2021

coqbot-app bot commented Nov 8, 2021

coqbot-app bot commented Nov 8, 2021

coqbot-app bot commented Dec 14, 2021

coqbot-app bot commented Jan 13, 2022

proux01 commented Nov 3, 2023

Blaisorblade commented Nov 3, 2023

proux01 commented Nov 4, 2023

proux01 commented Nov 10, 2023

coqbot-app bot commented Nov 10, 2023

proux01 commented Nov 10, 2023

herbelin commented Sep 24, 2021 •

edited by proux01