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

feat: detect default target on runLinter #811

Open
wants to merge 15 commits into
base: main
Choose a base branch
from
Open

feat: detect default target on runLinter #811

wants to merge 15 commits into from
+78 −16

Conversation

austinletson
Copy link
Contributor

@austinletson austinletson commented May 26, 2024 •
edited
Loading

Now runLinter will try to detect all root modules of the default build targets of type lean_exe or lean_lib in Lake's environment using the same resolveDefaultPackageTarget function as lake build.

Closes #795

@austinletson austinletson force-pushed the runLinter-default-module-detection branch from 128dc05 to 05c6ecd Compare May 26, 2024 13:55
@austinletson
feat: detect the first default target lean lib on runLinter
a9fd06a 
Previously, the default behavior for `runLinter` was to lint
`Batteries`.
Now `runLinter` will try to detect the either
the first lean_exe or first lean_lib
in Lake's environment which is also a default_target
@austinletson austinletson force-pushed the runLinter-default-module-detection branch from 05c6ecd to a9fd06a Compare May 26, 2024 13:56
@austinletson austinletson changed the title feat: detect the first default target lean lib on runLinter feat: detect default target on runLinter May 26, 2024
@austinletson austinletson mentioned this pull request May 26, 2024
Open
digama0
digama0 reviewed May 26, 2024
View reviewed changes
scripts/runLinter.lean Outdated Show resolved Hide resolved
@austinletson austinletson mentioned this pull request May 29, 2024
Closed
@austinletson austinletson marked this pull request as ready for review May 29, 2024 22:21
@austinletson
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label May 29, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Jul 17, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Jul 24, 2024
@kim-em
Copy link
Collaborator

kim-em commented Jul 26, 2024

I'm a bit worried about adding a Lake import after seeing the troubles described at leanprover-community/import-graph#20

@austinletson
Copy link
Contributor Author

austinletson commented Jul 29, 2024 •
edited
Loading

I'm a bit worried about adding a Lake import after seeing the troubles described at leanprover-community/import-graph#20

Hmm, this does seem like it could cause the same issue. Is there an example of a safe way to access Lake's internal API? I based this PR on this zulip thread about accessing Lake dependencies in for Mathlibs lake exe mk_all.

Another thought, does the fact that runLinter.lean is built separately from the rest of std as a lean_exe help us out at all?

@austinletson
Copy link
Contributor Author

austinletson commented Jul 29, 2024 •
edited
Loading

Related to this, I created a Zulip thread asking about a Lake command that would provide module and dependency information so we wouldn't have to use Lake's internals in cases such as these. (link)

@tydeu
Copy link
Collaborator

tydeu commented Jul 30, 2024

@semorrison

I'm a bit worried about adding a Lake import after seeing the troubles described at leanprover-community/import-graph#20

The problem there just appears to be that a shared library for Lake is not included in the currently Lean distro. That seems like it could be remedied relatively easily if necessary.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Aug 5, 2024
@kim-em
Copy link
Collaborator

kim-em commented Aug 5, 2024

@semorrison

I'm a bit worried about adding a Lake import after seeing the troubles described at leanprover-community/import-graph#20

The problem there just appears to be that a shared library for Lake is not included in the currently Lean distro. That seems like it could be remedied relatively easily if necessary.

@tydeu, yes please.

@tydeu
Copy link
Collaborator

tydeu commented Oct 16, 2024

FYI, a Lake shared library is now part of the standard Lean 4 release (since leanprover/lean4#5143, which is in v4.13.0),

@kim-em
Copy link
Collaborator

kim-em commented Oct 25, 2024

@austinletson, given @tydeu's comment above, I'm now happy to proceed with this. Would you mind sorting out the merge conflict? After that we can merge.

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 2, 2024
@leanprover-community-mathlib4-bot
Update Batteries branch for testing leanprover-community/batteries#811
b62ef15
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 2, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#811
0d82e3e
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 2, 2024 •
edited
Loading

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 2, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#811
2e83cfd
@austinletson
Copy link
Contributor Author

@kim-em I have fixed the merge conflict and improved the proposed changes' readability by moving the main linting code into a new runLinterOnModule function, which main calls for each module to lint.

Let me know if there is anything else needed to get this merged.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Nov 2, 2024
tydeu
tydeu reviewed Nov 2, 2024
View reviewed changes
scripts/runLinter.lean Outdated Show resolved Hide resolved
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 4, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover-community/batteries#811
79d3734
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 digama0 left review comments

@tydeu tydeu tydeu left review comments

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

runLinter should determine the target module by asking Lake
6 participants
@austinletson @kim-em @tydeu @leanprover-community-bot @digama0 @leanprover-community-mathlib4-bot