Support for string constant tokens in notations #17123

herbelin · 2023-01-17T14:08:23Z

By uniformity with numerals, we allow string constant terminals in notations, as in:

Notation " ""I'm true"" " := true.
Check "I'm true".

It is unclear whether this would be really used in practice but the uniformity of treatment between numerals and strings is nice, and a step towards a more generic treatment of them.

Added / updated test-suite.
Added changelog
Added documentation

JasonGross

I'm a fan of this feature, though I agree it's unclear how often it'd be used in practice.

Certainly deserves a changelog

interp/notation.ml

jfehrle · 2023-01-18T21:29:57Z

Would you add some description in the documentation?

herbelin · 2023-01-18T21:38:02Z

Would you add some description in the documentation?

I will, once I have a confirmation from @JasonGross that my proposal to support both string constants with spaces and isolated double quotes is ok.

Zimmi48 · 2023-01-31T11:07:24Z

@herbelin I think you got the confirmation you wanted.

jfehrle

Wording suggestions

doc/sphinx/user-extensions/syntax-extensions.rst

doc/changelog/03-notations/17123-master+support-for-string-constant-tokens-in-notations.rst

jfehrle

more tweaks

jfehrle · 2023-02-04T23:55:17Z

doc/sphinx/user-extensions/syntax-extensions.rst

+   string, as e.g. in :g:`Notation "A ""an unended string B"`. What
+   would be correct is typically :g:`Notation "A ""an ended string"" B`.


Suggested change

string, as e.g. in :g:`Notation "A ""an unended string B"`. What

would be correct is typically :g:`Notation "A ""an ended string"" B`.

string, as e.g. in :g:`Notation "A ""an unended string B" := "x"`, for which the

user probably meant :g:`Notation "A ""an unended string"" B" := "x"`.

To give complete commands (though I omit the period...)

Would it be ok to use "may" rather than "probably", here and below?

Do the examples really help actually? They somehow look a bit artificial (and complicated).

"May", "probably", either one is fine. But I agree the examples are not so helpful.

I'd suggest using Reserved Notation instead of := "x", to make the examples slightly less artificial

Using Reserved adopted.

jfehrle · 2023-02-05T00:00:19Z

doc/sphinx/user-extensions/syntax-extensions.rst

+   :g:`Notation "A ""string""! B"` or `Notation "A ""string""!"" B"`.
+   What would be correct are typically :g:`Notation "A ""string"""" ! B`,
+   :g:`Notation "A ""string""""!"" B`, or :g:`Notation "A '""string""!' B`.


Suggested change

:g:`Notation "A ""string""! B"` or `Notation "A ""string""!"" B"`.

What would be correct are typically :g:`Notation "A ""string"""" ! B`,

:g:`Notation "A ""string""""!"" B`, or :g:`Notation "A '""string""!' B`.

:g:`Notation "A ""string""! B"` or `Notation "A ""string""!"" B"`, for which

the user probably meant :g:`Notation "A ""string"""" ! B`,

:g:`Notation "A ""string""""!"" B`, or :g:`Notation "A '""string""!' B`.

Ok (using "may").

jfehrle · 2023-02-05T22:14:16Z

doc/sphinx/user-extensions/syntax-extensions.rst

+   string, as e.g. in :g:`Notation "A ""an unended string B"`. What
+   would be correct is typically :g:`Notation "A ""an ended string"" B`.
+
+.. exn:: End of string not followed by a space in notation.


Suggested change

.. exn:: End of string not followed by a space in notation.

.. exn:: End of quoted string not followed by a space in notation.

Clearer, I think--your choice.

OK, adopted.

JasonGross

I haven't looked at the implementation this time, but I'm happy with the spec

JasonGross · 2023-03-22T14:14:14Z

doc/sphinx/user-extensions/syntax-extensions.rst

@@ -74,8 +75,21 @@ lose their role as parameters. For example:

   Notation "'IF' c1 'then' c2 'else' c3" := (c1 /\ c2 \/ ~ c1 /\ c3) (at level 200, right associativity).

-Symbols that start with a single quote with 3 or more characters must be single quoted.
-For example, the symbol `'ab` is represented by `''ab'` in the notation string.
+Symbols that start with a single quote and followed by at least 2


Suggested change

Symbols that start with a single quote and followed by at least 2

Symbols that start with a single quote followed by at least 2

or

Suggested change

Symbols that start with a single quote and followed by at least 2

Symbols that start with a single quote and are followed by at least 2

OK, first variant adopted.

JasonGross · 2023-03-22T14:17:04Z

doc/sphinx/user-extensions/syntax-extensions.rst

+double quotes without being strings themselves (as e.g. in symbol :g:`|"|`) but notations with such symbols can be
+used only for printing (see :ref:`Use of notations for printing <UseOfNotationsForPrinting>`).
+In this case, no spaces are allowed in the symbol.  Also, if the
+symbol starts with a double quote, it should be surrounded with single


Suggested change

symbol starts with a double quote, it should be surrounded with single

symbol starts with a double quote, it must be surrounded with single

? Or else describe when it's permitted, or be clear that the confusion will only occur on the part of the users, etc.

JasonGross · 2023-03-22T14:20:05Z

doc/sphinx/user-extensions/syntax-extensions.rst

+   string, as e.g. in :g:`Notation "A ""an unended string B"`. What
+   would be correct is typically :g:`Notation "A ""an ended string"" B`.


I'd suggest using Reserved Notation instead of := "x", to make the examples slightly less artificial

coqbot-app · 2023-04-24T02:18:29Z

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 · 2023-05-24T02:20:05Z

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

herbelin · 2023-07-07T18:37:07Z

Rebased, suggestions applied and test-suite fixed.

We follow the same principle as numbers: - string constants can be used as part of notations - if parsing articulation points, string constants can be set as keywords Note that isolated double quotes, as in ``Notation "a "" b" := ...'' are (still) not permitted (they would be considered as the start of an unterminated string by the lexer). Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

proux01 · 2023-07-16T07:32:00Z

@coqbot merge now

herbelin added part: notations The notation system. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. labels Jan 17, 2023

herbelin added this to the 8.18+rc1 milestone Jan 17, 2023

herbelin requested review from a team as code owners January 17, 2023 14:08

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jan 17, 2023

herbelin force-pushed the master+support-for-string-constant-tokens-in-notations branch from abe6804 to a302351 Compare January 17, 2023 14:18

herbelin requested a review from a team as a code owner January 17, 2023 14:18

JasonGross requested changes Jan 17, 2023

View reviewed changes

interp/notation.ml Outdated Show resolved Hide resolved

interp/notation.ml Show resolved Hide resolved

interp/notation.ml Show resolved Hide resolved

JasonGross reviewed Jan 17, 2023

View reviewed changes

interp/notation.ml Show resolved Hide resolved

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

herbelin force-pushed the master+support-for-string-constant-tokens-in-notations branch from a302351 to f828223 Compare January 18, 2023 21:05

coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jan 18, 2023

jfehrle added the needs: changelog entry This should be documented in doc/changelog. label Jan 18, 2023

herbelin added a commit to herbelin/github-coq that referenced this pull request Feb 3, 2023

Adding change log for coq#17123

288c157

herbelin force-pushed the master+support-for-string-constant-tokens-in-notations branch from f828223 to 288c157 Compare February 3, 2023 21:41

herbelin added a commit to herbelin/github-coq that referenced this pull request Feb 4, 2023

Adding change log for coq#17123

0d8080c

herbelin force-pushed the master+support-for-string-constant-tokens-in-notations branch from 288c157 to 0d8080c Compare February 4, 2023 11:06

herbelin added a commit to herbelin/github-coq that referenced this pull request Feb 4, 2023

Adding change log for coq#17123

f814576

herbelin force-pushed the master+support-for-string-constant-tokens-in-notations branch from 0d8080c to f814576 Compare February 4, 2023 14:31

jfehrle reviewed Feb 4, 2023

View reviewed changes

herbelin force-pushed the master+support-for-string-constant-tokens-in-notations branch from c3c4784 to 843318d Compare February 4, 2023 23:13

jfehrle reviewed Feb 5, 2023

View reviewed changes

herbelin force-pushed the master+support-for-string-constant-tokens-in-notations branch from 9b48b54 to 843318d Compare February 5, 2023 19:32

jfehrle reviewed Feb 5, 2023

View reviewed changes

coqbot-app bot removed this from the 8.18+rc1 milestone Mar 13, 2023

herbelin reopened this Mar 13, 2023

ppedrot removed the needs: changelog entry This should be documented in doc/changelog. label Mar 22, 2023

ppedrot requested a review from JasonGross March 22, 2023 12:00

JasonGross approved these changes Mar 22, 2023

View reviewed changes

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

coqbot-app bot added the stale This PR will be closed unless it is rebased. label Apr 24, 2023

coqbot-app bot closed this May 24, 2023

herbelin reopened this Jul 7, 2023

herbelin added 2 commits July 7, 2023 19:40

In passing, using String.plural when possible in notation.ml.

13aff42

Adding a function to quote strings according to Coq convention.

18a8da3

herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 7, 2023

herbelin added a commit to herbelin/github-coq that referenced this pull request Jul 7, 2023

Adding change log for coq#17123

01d2b25

herbelin force-pushed the master+support-for-string-constant-tokens-in-notations branch from 5fa615a to 03c2357 Compare July 7, 2023 18:34

herbelin and others added 2 commits July 15, 2023 18:54

Adding change log for coq#17123

71738f3

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

proux01 force-pushed the master+support-for-string-constant-tokens-in-notations branch from 03c2357 to 71738f3 Compare July 15, 2023 16:55

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 15, 2023

proux01 removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 15, 2023

proux01 added this to the 8.19+rc1 milestone Jul 15, 2023

proux01 self-assigned this Jul 16, 2023

coqbot-app bot merged commit 9809956 into coq:master Jul 16, 2023
5 of 6 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support for string constant tokens in notations #17123

Support for string constant tokens in notations #17123

herbelin commented Jan 17, 2023 •

edited

JasonGross left a comment

jfehrle commented Jan 18, 2023

herbelin commented Jan 18, 2023

Zimmi48 commented Jan 31, 2023

jfehrle left a comment

jfehrle left a comment

jfehrle Feb 4, 2023

herbelin Feb 5, 2023

jfehrle Feb 5, 2023

JasonGross Mar 22, 2023

herbelin Jul 7, 2023

jfehrle Feb 5, 2023

herbelin Jul 7, 2023

jfehrle Feb 5, 2023

herbelin Jul 7, 2023

JasonGross left a comment

JasonGross Mar 22, 2023

herbelin Jul 7, 2023

JasonGross Mar 22, 2023

herbelin Jul 7, 2023

JasonGross Mar 22, 2023

coqbot-app bot commented Apr 24, 2023

coqbot-app bot commented May 24, 2023

herbelin commented Jul 7, 2023

proux01 commented Jul 16, 2023

		string, as e.g. in :g:`Notation "A ""an unended string B"`. What
		would be correct is typically :g:`Notation "A ""an ended string"" B`.

	.. exn:: End of string not followed by a space in notation.
	.. exn:: End of quoted string not followed by a space in notation.

	Symbols that start with a single quote and followed by at least 2
	Symbols that start with a single quote followed by at least 2

	symbol starts with a double quote, it should be surrounded with single
	symbol starts with a double quote, it must be surrounded with single

Support for string constant tokens in notations #17123

Support for string constant tokens in notations #17123

Conversation

herbelin commented Jan 17, 2023 • edited

JasonGross left a comment

Choose a reason for hiding this comment

jfehrle commented Jan 18, 2023

herbelin commented Jan 18, 2023

Zimmi48 commented Jan 31, 2023

jfehrle left a comment

Choose a reason for hiding this comment

jfehrle left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

JasonGross left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

coqbot-app bot commented Apr 24, 2023

coqbot-app bot commented May 24, 2023

herbelin commented Jul 7, 2023

proux01 commented Jul 16, 2023

herbelin commented Jan 17, 2023 •

edited