Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fixes #14124: forbid empty strings in Ltac notations #14378

Merged
merged 2 commits into from May 25, 2021
Merged

Fixes #14124: forbid empty strings in Ltac notations #14378

merged 2 commits into from May 25, 2021

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented May 24, 2021 •
edited

Kind: bug fix

Fixes / closes #14124

  • Added / updated test-suite
  • Entry added in the changelog

@herbelin herbelin added kind: fix This fixes a bug or incorrect documentation. part: ltac Issues and PRs related to the Ltac tactic language. part: notations The notation system. labels May 24, 2021
@herbelin herbelin added this to the 8.13.3 milestone May 24, 2021
@herbelin herbelin requested a review from a team as a code owner May 24, 2021 13:07
herbelin added a commit to herbelin/github-coq that referenced this pull request May 24, 2021
@herbelin
Add change log for PR coq#14378.
82b8319
@herbelin herbelin mentioned this pull request May 24, 2021
Closed
herbelin added a commit to herbelin/github-coq that referenced this pull request May 24, 2021
@herbelin
Add change log for PR coq#14378.
108dc5d
@herbelin herbelin force-pushed the master+fix14124-check-empty-string-ltac-notation branch from 82b8319 to 108dc5d Compare May 24, 2021 13:52
@coqbot-app
Copy link
Contributor

coqbot-app bot commented May 24, 2021

Hey, I have detected that there were CI failures at commit 108dc5d without any failure in the test-suite.
I checked that the corresponding jobs for the base commit ce69cf0 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following target: ci-coq_tools.

@ppedrot ppedrot self-assigned this May 24, 2021
@coqbot-app
Copy link
Contributor

coqbot-app bot commented May 24, 2021

Hey, I have detected that there were CI failures at commit 108dc5d without any failure in the test-suite.
I checked that the corresponding jobs for the base commit ce69cf0 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following target: ci-coq_tools.

1 similar comment
@coqbot-app
Copy link
Contributor

coqbot-app bot commented May 24, 2021

Hey, I have detected that there were CI failures at commit 108dc5d without any failure in the test-suite.
I checked that the corresponding jobs for the base commit ce69cf0 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following target: ci-coq_tools.

ppedrot
ppedrot reviewed May 25, 2021
View reviewed changes
plugins/ltac/g_ltac.mlg Outdated Show resolved Hide resolved
@herbelin herbelin force-pushed the master+fix14124-check-empty-string-ltac-notation branch from 108dc5d to c43c95e Compare May 25, 2021 07:40
@ppedrot
Copy link
Member

ppedrot commented May 25, 2021

Adding a test is probably a good idea before I merge though.

@herbelin
Copy link
Member Author

Adding a test is probably a good idea before I merge though.

The problem is that I don't think we have a way to test parsing errors (they are not caught by Fail).

@ppedrot
Copy link
Member

ppedrot commented May 25, 2021

Oh, right. You could always write a misc test but it could legitimately be considered overblown. Let's merge as-is then.

@coqbot-app coqbot-app bot added this to Request 8.13.3 inclusion in Coq 8.13 May 25, 2021
@ppedrot ppedrot merged commit 367b44e into coq:master May 25, 2021
@Zimmi48 Zimmi48 modified the milestones: 8.13.3, 8.14+rc1 Jun 9, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: fix This fixes a bug or incorrect documentation. part: ltac Issues and PRs related to the Ltac tactic language. part: notations The notation system.
Projects
None yet
Milestone
8.14+rc1
Development

Successfully merging this pull request may close these issues.

Tactic Notation: Anomaly: Uncaught exception Failure("empty token.").
3 participants
@herbelin @ppedrot @Zimmi48