[Merged by Bors] - fix(lint-style): parse linter options and load environment extensions correctly#29513
[Merged by Bors] - fix(lint-style): parse linter options and load environment extensions correctly#29513grunweg wants to merge 10 commits intoleanprover-community:masterfrom
Conversation
PR summary 14871d5175Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic.Polyrith | 1 | 45 | +44 (+4400.00%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Tactic.Polyrith |
44 |
Declarations diff
+ instance : ToExpr LinterSets := inferInstanceAs <| ToExpr (NameMap _)
+ instance [ToExpr α] : ToExpr (NameMap α)
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
grunweg
left a comment
There was a problem hiding this comment.
These are nice fixes, thank you!
Can/should the doc-string for Lean.withImportModules be updated to mention that this does not load environment extensions? Just from the docs alone, that is only obvious by implicit comparison with Lean.importModules (and it's not clear if that's an intentional difference or just different levels of details, etc).
|
With the commits I just pushed, |
This should have been documented in the first place, but the CI check for this was broken. leanprover-community#29513 fixes the check (hence discovered this issue).
This should have been documented in the first place, but the CI check for this was broken. leanprover-community#29513 fixes the check (hence discovered this issue).
Discovered by leanprover-community#29513, which fixes the CI check enforcing these.
Discovered by leanprover-community#29513, which fixes the CI check enforcing these.
This should have been documented in the first place, but the CI check for this was broken. leanprover-community#29513 fixes the check (hence discovered this issue).
41b2fa1 to
075258b
Compare
|
Let's rebase, that hopefully fixes the unrelated lint-style failure. |
This should have been documented in the first place, but the CI check for this was broken. leanprover-community#29513 fixes the check (hence discovered this issue).
Discovered by #29513, which fixes the CI check enforcing these. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
This should have been documented in the first place, but the CI check for this was broken. #29513 fixes the check (hence discovered this issue). Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
|
This PR/issue depends on: |
This fixes two issues: We never called the `toOptions` function that parses Lakefile options into a `Lean.Options` structure: the function we use instead is only meant for command-line options and doesn't handle the `weak.` prefix correctly. The way we load linter sets was incorrect: `withImportModules` doesn't update any environment extensions, and that is exactly what we use to store linter sets. We can replace it with `importModules` instead, but that is a bit less safe. It would be great if we had some sort of macro that can give us the environment at the point of elaboration instead.
bf0eea6 to
1d48b0d
Compare
|
@Vierkantor Oh no, seems I did a major rebase blunder and force-pushed away your last commit. I'm so sorry. (I have no idea how or why this happened.) Do you mind re-doing it...? |
|
(At least the link to xxx in "... force-pushed from xxx to yyy" shows the last commit's diff, so you just need to manually make a commit with that again.) |
…#29584) This should have been documented in the first place, but the CI check for this was broken. leanprover-community#29513 fixes the check (hence discovered this issue). Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Issue is passing the right linter options... how to do this?
|
I just added a stub test file, but am not sure how to call it in a test. Help is appreciated! |
|
I just merged master and fixed another two violations. Can we get this in? Having this stay in perpetual limbo is not helpful for anybody. |
| instance : ToExpr LinterSets := inferInstanceAs <| ToExpr (NameMap _) | ||
|
|
||
| /-- Return the linter sets defined at this point of elaborating the current file. -/ | ||
| elab "linter_sets%" : term => do |
There was a problem hiding this comment.
I'm having issues with my computer, so I cannot really open this file. However, does it make sense to test this term elaborator? Maybe just partly by checking that the resulting term contains something that is more stable than all of its output? E.g. check that it contains the header linter option?
There was a problem hiding this comment.
How about: we check that any option is enabled, and fail otherwise? That is also helpful for debugging downstream usages of this script that may not have the header requirement like Mathlib does.
There was a problem hiding this comment.
Hmm. But deciding whether a specific linter is enabled happens inside that linter. So we would not be able to read out this information easily from outside. I'll add something like your test instead!
|
Thanks for adding the new self-tests: I like how they work. (You can probably delete |
|
Thanks! 🐙 bors merge |
… correctly (#29513) Parse options and load linter set extension correctly. This fixes two issues: - We never called the `toOptions` function that parses Lakefile options into a `Lean.Options` structure: the function we use instead is only meant for command-line options and doesn't handle the `weak.` prefix correctly. - The way we load linter sets was incorrect: `withImportModules` stopped updating environment extensions since [lean4#6325](leanprover/lean4#6325), and that is exactly what we use to store linter sets. At the time of writing, `importModules` might be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
This file as added in leanprover-community#29513, but never hooked up to the unit tests. It is thus unused; delete it.
|
#30497 deletes |
This file as added in #29513, but never hooked up to the unit tests. It is thus unused; delete it.
… correctly (leanprover-community#29513) Parse options and load linter set extension correctly. This fixes two issues: - We never called the `toOptions` function that parses Lakefile options into a `Lean.Options` structure: the function we use instead is only meant for command-line options and doesn't handle the `weak.` prefix correctly. - The way we load linter sets was incorrect: `withImportModules` stopped updating environment extensions since [lean4#6325](leanprover/lean4#6325), and that is exactly what we use to store linter sets. At the time of writing, `importModules` might be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
This file as added in leanprover-community#29513, but never hooked up to the unit tests. It is thus unused; delete it.
Parse options and load linter set extension correctly.
This fixes two issues:
toOptionsfunction that parses Lakefile options into aLean.Optionsstructure: the function we use instead is only meant for command-line options and doesn't handle theweak.prefix correctly.withImportModulesstopped updating environment extensions since lean4#6325, and that is exactly what we use to store linter sets. At the time of writing,importModulesmight be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead.downstream_dashboard.py#29584Mathlib.Initas such #29586