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

fix: lake: exe bad import errors & related touchups #4529

Merged
merged 1 commit into from
Jun 26, 2024
Merged

fix: lake: exe bad import errors & related touchups #4529

merged 1 commit into from
Jun 26, 2024

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Jun 21, 2024 •
edited
Loading

Fixes some issues with the executable build and bad imports.

Release notes:

  • A bad import in an executable no longer prevents the executable's root module from being built., This also fixes a problem where the location of a transitive bad import would not been shown.
  • The root module of the executable now respects nativeFacets.

Technical touchups:

  • Expanded and better documented tests/badImport.
  • Use ensureJob in recBuildDeps to catch import errors instead of individual try ... catch blocks.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 21, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 21, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4529
d3531f3
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 21, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4529
7bf46d0
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jun 21, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Jun 21, 2024 •
edited
Loading

Mathlib CI status (docs):

@tydeu tydeu added will-merge-soon …unless someone speaks up release-ci Enable all CI checks for a PR, like is done for releases labels Jun 22, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 22, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4529
09f74a3
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 22, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4529
8cea1d7
@tydeu tydeu enabled auto-merge June 25, 2024 16:27
@tydeu tydeu disabled auto-merge June 26, 2024 01:37
@tydeu tydeu enabled auto-merge June 26, 2024 01:37
@tydeu tydeu force-pushed the lake/exe-bad-import-fixes branch from e0b869b to bf0967b Compare June 26, 2024 01:38
@tydeu tydeu disabled auto-merge June 26, 2024 01:39
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 26, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4529
fa5c17c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 26, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4529
1f15a73
@tydeu tydeu added this pull request to the merge queue Jun 26, 2024
Merged via the queue into leanprover:master with commit 5e7d2c3 Jun 26, 2024
22 checks passed
@tydeu tydeu deleted the lake/exe-bad-import-fixes branch June 26, 2024 04:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@tydeu @leanprover-community-mathlib4-bot