Provide an explicit primitive to raise non-zero Ltac failures. #15327
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ppedrot
added a commit
to ppedrot/aac-tactics
that referenced
this pull request
Dec 10, 2021
ppedrot
added a commit
to ppedrot/coq-elpi
that referenced
this pull request
Dec 10, 2021
ppedrot
added a commit
to ppedrot/Coq-Equations
that referenced
this pull request
Dec 10, 2021
ppedrot
added a commit
to ppedrot/unicoq
that referenced
this pull request
Dec 10, 2021
ppedrot
added a commit
to ppedrot/relation-algebra
that referenced
this pull request
Dec 10, 2021
ppedrot
force-pushed
the
split-tclfail-level
branch
from
e846c43
to
b20cacf
Compare
ppedrot
added a commit
to ppedrot/fiat
that referenced
this pull request
Dec 10, 2021
ppedrot
added a commit
to ppedrot/coqhammer
that referenced
this pull request
Dec 10, 2021
ppedrot
force-pushed
the
split-tclfail-level
branch
2 times, most recently
from
ad6f94b
to
6009ad5
Compare
The rationale is that non-zero level failing is an Ltac-specific feature. We have a few tacticals around that try to catch this level and reraise it with a lower level, but this hardly makes sense for ML tactics. Only Ltac programs should ever observe the level, and even there this feature is often used to work around deficiencies of the expressivity of Ltac. As a matter of fact, most ML callers of the tclFAIL primitive call it with a level set to 0, which clearly indicates an API issue. This PR removes the tclFAIL level argument, and provides a tclFAILn function to pass an arbitrary number when needed.
ppedrot
force-pushed
the
split-tclfail-level
branch
from
6009ad5
to
a6c1d80
Compare
SkySkimmer
approved these changes
Dec 11, 2021
|
@coqbot merge now |
|
@SkySkimmer: Please take care of the following overlays:
|
SkySkimmer
added a commit
to coq-community/aac-tactics
that referenced
this pull request
Dec 11, 2021
gares
added a commit
to LPCIC/coq-elpi
that referenced
this pull request
Dec 11, 2021
damien-pous
pushed a commit
to damien-pous/relation-algebra
that referenced
this pull request
Dec 11, 2021
Janno
added a commit
to unicoq/unicoq
that referenced
this pull request
Dec 11, 2021
ppedrot
added a commit
to mattam82/Coq-Equations
that referenced
this pull request
Dec 11, 2021
JasonGross
pushed a commit
to mit-plv/fiat
that referenced
this pull request
Dec 12, 2021
lukaszcz
pushed a commit
to lukaszcz/coqhammer
that referenced
this pull request
Dec 12, 2021
proux01
pushed a commit
to proux01/itauto
that referenced
this pull request
Mar 1, 2022
ppedrot
added a commit
to ppedrot/relation-algebra
that referenced
this pull request
Sep 14, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The rationale is that non-zero level failing is an Ltac-specific feature. We have a few tacticals around that try to catch this level and reraise it with a lower level, but this hardly makes sense for ML tactics. Only Ltac programs should ever observe the level, and even there this feature is often used to work around deficiencies of the expressivity of Ltac.
As a matter of fact, most ML callers of the tclFAIL primitive call it with a level set to 0, which clearly indicates an API issue.
This PR removes the tclFAIL level argument, and provides a tclFAILn function to pass an arbitrary number when needed.
Overlays: