Rename mlg grammar nonterminals to make documented and mlg grammars more consistent #13219

jfehrle · 2020-10-18T04:36:38Z

While updating the syntax in the documentation, we (primarily me and @Zimmi48) found that many of the mlg nonterminal names were not good enough for use in the documentation, so we chose better names. This PR updates the mlgs so that they use most of these names. This will make it less confusing for developers to relate the grammar in the manual to the mlg files. (I frequently got confused by the different names even though I'm acutely aware that there are differences in the names.)

There is no functional change here other than that the Print Grammar command output may show some of the changed names. Global variables for nonterminals defined in mli files that were renamed were made equal to the new variables and deprecated to avoid breaking external plugins that may rely on those variables.

Perhaps @herbelin is willing to do the review?

"A rose by any other name would smell as sweet"

jfehrle · 2020-10-25T22:43:07Z

Rebased. Do we need any others to review this?

herbelin · 2020-10-26T10:22:55Z

Do we need any others to review this?

I believe we can go. Merging tomorrow (if no comments by then and if I don't forget).

Zimmi48 · 2020-10-26T10:31:44Z

plugins/syntax/g_numeral.mlg

-  | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
-      ident(sc) numnotoption(o) ] ->
-
-    { warn_deprecated_numeral_notation ();
-      vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }


Wait a minute. This PR removes the deprecated Numeral Notation command but this command was only deprecated in 8.13, which is not released yet.

OK, waiting.

By the way, won't it be too much of a burden for users to change from Numeral to Number? (Or maybe the changes are already clearly accepted upstreams?)

By the way, won't it be too much of a burden for users to change from Numeral to Number? (Or maybe the changes are already clearly accepted upstreams?)

That's a fair question. There has been a bit of a debate after the PR changing this was merged. See #12979 (comment). IMHO for this kind of cosmetic change, the solution is to make the deprecation period sufficiently long (a bit like the Ocaml vs OCaml value for Extraction Language which was changed and deprecated in 8.8 but only removed in 8.13).

Yes, this is somehow the question. Is the added value of the change worth the burden (but again, if the change is already validated by the users, it does not matter)?

My mistake during rebasing, now fixed.

Zimmi48 · 2020-10-26T12:12:09Z

The PR otherwise looks good to me (I reviewed the changes to the refman in particular).

jfehrle · 2020-10-26T20:47:11Z

Ah, I realize that changing numnotoption to numeral_modifier will be visible in the Tactic Notation command. Any use of numnotoption will be broken. (All of the 141 nonterminals with an ARGUMENT EXTEND are accessible in Tactic Notation.) I can handle this 3 ways, in order of my preference:

Do nothing. This aspect of Tactic Notation has been undocumented and probably the symbol hasn't been used.
Drop the old symbol, but print an error message giving the new name (as done recently for dropping var)
Add a true deprecation warning and keep both symbols around for a while.

herbelin · 2020-10-26T21:01:57Z

I believe that the probability that this undocumented symbol was used is close to 0. So, option 1 seems reasonable to me.

jfehrle · 2020-10-26T21:15:47Z

OK. I'm making one more small fix, should be done shortly.

coqbot-app · 2020-10-27T04:07:21Z

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

JasonGross · 2020-10-27T04:23:37Z

It seems like the f-c-l job should have been restarted automatically?

Fetching changes with git depth set to 10...
fatal: remote origin already exists.
From https://gitlab.com/coq/coq
 * [new ref]                   refs/pipelines/207965281 -> refs/pipelines/207965281
 + 7b73021ea2a1...916454000687 pr-13219                 -> origin/pr-13219  (forced update)
Auto packing the repository in background for optimum performance.
See "git help gc" for manual housekeeping.
fatal: Unable to create '/builds/coq/coq/.git/gc.pid.lock': File exists.
Another git process seems to be running in this repository, e.g.
an editor opened by 'git commit'. Please make sure all processes
are terminated then try again. If it still fails, a git process
may have crashed in this repository earlier:
remove the file manually to continue.
Checking out 91645400 as pr-13219...
Skipping Git submodules setup
Downloading artifacts for build:edge+flambda (813372045)...
04:14
ERROR: Downloading artifacts from coordinator... error couldn't execute GET against https://gitlab.com/api/v4/jobs/813372045/artifacts: Get https://gitlab.com/api/v4/jobs/813372045/artifacts: dial tcp [2606:4700:90:0:f22e:fbec:5bed:a9b9]:443: connect: cannot assign requested address  id=813372045 token=B1UC8-6q
WARNING: Retrying...                               
ERROR: Downloading artifacts from coordinator... error  error=read tcp 172.17.0.2:33698->172.65.251.78:443: read: connection reset by peer id=813372045 responseStatus=200 OK token=B1UC8-6q
WARNING: Retrying...                               
ERROR: Downloading artifacts from coordinator... error couldn't execute GET against https://gitlab.com/api/v4/jobs/813372045/artifacts: Get https://gitlab.com/api/v4/jobs/813372045/artifacts: dial tcp [2606:4700:90:0:f22e:fbec:5bed:a9b9]:443: connect: cannot assign requested address  id=813372045 token=B1UC8-6q
FATAL: invalid argument                            
Uploading artifacts...
00:11
WARNING: _build_ci: no matching files              
ERROR: No files to upload                          
ERROR: Job failed: exit code 1

cc @Zimmi48 ?

jfehrle · 2020-10-27T05:25:48Z

OK, made my little fix (using ARGUMENT EXTEND ltac2_expr instead of ARGUMENT EXTEND tac2expr. I think the library:ci-fiat_crypto_legacy failure is unrelated--just that uploading artifacts failed at the end of the job. 3 other jobs still pending. Unless one of those breaks in an important way., I think this is ready to go.

Zimmi48 · 2020-10-27T09:01:37Z

Indeed, like @JasonGross said (thanks for reporting BTW), this is an unrelated failure that should have been restarted automatically (I have identified the issue). Just to be sure, I'm manually restarted the job.

typ_param -> ltac2_typevar, tac2expr -> ltac2_expr

jfehrle · 2020-10-27T19:24:32Z

Rebased.

herbelin · 2020-10-27T21:12:35Z

dpdgraph error related to pending overlay merge for #13073

@coqbot: merge now

jfehrle · 2020-10-27T21:35:25Z

Thank you, sir!

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

jfehrle force-pushed the rename_nts2 branch 2 times, most recently from 2de10a1 to c1d0472 Compare October 18, 2020 05:07

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

jfehrle force-pushed the rename_nts2 branch from c1d0472 to f3109b9 Compare October 18, 2020 05:09

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 19, 2020

This comment has been minimized.

Sign in to view

jfehrle force-pushed the rename_nts2 branch 2 times, most recently from f477ac7 to 6850f7c Compare October 20, 2020 04:42

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

jfehrle force-pushed the rename_nts2 branch from 6850f7c to f3f59a3 Compare October 20, 2020 07:02

jfehrle changed the title ~~Testing...~~ Rename grammar terminals to make documented grammar and mlg grammar more consistent Oct 20, 2020

jfehrle added the kind: cleanup Code removal, deprecation, refactorings, etc. label Oct 20, 2020

jfehrle added this to the 8.13+beta1 milestone Oct 20, 2020

jfehrle requested a review from herbelin October 20, 2020 07:20

jfehrle changed the title ~~Rename grammar terminals to make documented grammar and mlg grammar more consistent~~ Rename mlg grammar nonterminals to make documented and mlg grammars more consistent Oct 20, 2020

jfehrle marked this pull request as ready for review October 20, 2020 07:27

jfehrle requested review from a team as code owners October 20, 2020 07:27

jfehrle removed request for a team October 20, 2020 07:27

jfehrle force-pushed the rename_nts2 branch from 5d1984c to 06923d0 Compare October 25, 2020 22:40

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

jfehrle force-pushed the rename_nts2 branch from 06923d0 to 075ed65 Compare October 26, 2020 08:42

herbelin self-assigned this Oct 26, 2020

Zimmi48 requested changes Oct 26, 2020

View reviewed changes

jfehrle force-pushed the rename_nts2 branch from 075ed65 to 2dee0f8 Compare October 26, 2020 19:11

jfehrle force-pushed the rename_nts2 branch from dc5e5d3 to 3070290 Compare October 27, 2020 03:31

Zimmi48 approved these changes Oct 27, 2020

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 Oct 27, 2020

jfehrle added 5 commits October 27, 2020 12:15

Rename operconstr -> term

b402adc

Rename tactic_expr -> ltac_expr

ede77b7

Rename misc nonterminals

41b0780

Rename tac2type -> ltac2_type,

6620c74

typ_param -> ltac2_typevar, tac2expr -> ltac2_expr

Change a few nonterminal names in mlgs and update doc to match

480d34f

jfehrle force-pushed the rename_nts2 branch from 3070290 to 480d34f Compare October 27, 2020 19:17

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

coqbot-app bot merged commit c8110e1 into coq:master Oct 27, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rename mlg grammar nonterminals to make documented and mlg grammars more consistent #13219

Rename mlg grammar nonterminals to make documented and mlg grammars more consistent #13219

jfehrle commented Oct 18, 2020 •

edited

This comment has been minimized.

jfehrle commented Oct 25, 2020

herbelin commented Oct 26, 2020

Zimmi48 Oct 26, 2020

herbelin Oct 26, 2020 •

edited

Zimmi48 Oct 26, 2020

herbelin Oct 26, 2020

jfehrle Oct 26, 2020

Zimmi48 commented Oct 26, 2020

jfehrle commented Oct 26, 2020

herbelin commented Oct 26, 2020

jfehrle commented Oct 26, 2020

coqbot-app bot commented Oct 27, 2020

JasonGross commented Oct 27, 2020

jfehrle commented Oct 27, 2020

Zimmi48 commented Oct 27, 2020

jfehrle commented Oct 27, 2020

herbelin commented Oct 27, 2020

jfehrle commented Oct 27, 2020

Rename mlg grammar nonterminals to make documented and mlg grammars more consistent #13219

Rename mlg grammar nonterminals to make documented and mlg grammars more consistent #13219

Conversation

jfehrle commented Oct 18, 2020 • edited

This comment has been minimized.

jfehrle commented Oct 25, 2020

herbelin commented Oct 26, 2020

Zimmi48 Oct 26, 2020

Choose a reason for hiding this comment

herbelin Oct 26, 2020 • edited

Choose a reason for hiding this comment

Zimmi48 Oct 26, 2020

Choose a reason for hiding this comment

herbelin Oct 26, 2020

Choose a reason for hiding this comment

jfehrle Oct 26, 2020

Choose a reason for hiding this comment

Zimmi48 commented Oct 26, 2020

jfehrle commented Oct 26, 2020

herbelin commented Oct 26, 2020

jfehrle commented Oct 26, 2020

coqbot-app bot commented Oct 27, 2020

JasonGross commented Oct 27, 2020

jfehrle commented Oct 27, 2020

Zimmi48 commented Oct 27, 2020

jfehrle commented Oct 27, 2020

herbelin commented Oct 27, 2020

jfehrle commented Oct 27, 2020

jfehrle commented Oct 18, 2020 •

edited

herbelin Oct 26, 2020 •

edited