This repository was archived by the owner on Jul 24, 2024. It is now read-only.
feat(lint): add priority test for instances that always apply#1625
Merged
mergify[bot] merged 8 commits intomasterfrom Nov 1, 2019
Merged
feat(lint): add priority test for instances that always apply#1625mergify[bot] merged 8 commits intomasterfrom
mergify[bot] merged 8 commits intomasterfrom
Conversation
fpvandoorn
added
awaiting-review
also move a defn from coinductive_predicates to expr also slightly refactor incorrect_def_lemma
Now they are run in the order specified by the doc
even when they are slow and is false
fpvandoorn
removed
the
blocked-by-other-PR
cipher1024
reviewed
Oct 28, 2019
cipher1024
reviewed
Oct 28, 2019
remove coinductive_predicates as import from some (but not all) files
Member
|
Cool, this seems really useful! Is there a reason for the default linter priorities? Or is it just the order they appear in the file? If there's a reason to order them a certain way, we should document it, but I suspect it's just arbitrary (which is fine). |
Member
robertylewis
left a comment
robertylewis
left a comment
There was a problem hiding this comment.
Only very very minor stylistic things.
robertylewis
added
awaiting-author
Member
Author
No, I currently just use the order it was in before and the order of the doc. (The place of this new linter is pretty arbitrary.) |
fpvandoorn
added
awaiting-review
robertylewis
approved these changes
Oct 31, 2019
robertylewis
added
ready-to-merge
7 tasks
butterthebuddha
pushed a commit
to butterthebuddha/mathlib
that referenced
this pull request
May 15, 2020
…over-community#1625) * feat(lint): add priority test for instances that always apply also move a defn from coinductive_predicates to expr also slightly refactor incorrect_def_lemma * update doc * add priorities to linters Now they are run in the order specified by the doc * always run tests in the extra set even when they are slow and is false * move some more declarations from coinductive_predicates to expr remove coinductive_predicates as import from some (but not all) files * reviewer comments * remove unsafe prefixes
This file contains hidden or 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
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
5 participants
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.
Built on top of feat(tactic/lint): silent linting #1580has_scalar ℝ (ℝ → ℝ)#1561. This is mainly useful for performance: it is more efficient to first apply the structural instances (that match on the type), and afterwards the forgetful instances (that always apply and change the class).coinductive_predicates.leantoexpr.lean, and everything aboutbinder(inexpr.lean) above the section onexpr.