Skip to content

fix: lake: import-related bugs#8026

Merged
tydeu merged 4 commits intoleanprover:masterfrom
tydeu:lake/fix-badImport
Apr 19, 2025
Merged

fix: lake: import-related bugs#8026
tydeu merged 4 commits intoleanprover:masterfrom
tydeu:lake/fix-badImport

Conversation

@tydeu
Copy link
Copy Markdown
Member

@tydeu tydeu commented Apr 19, 2025

This PR fixes bugs in #7809 and #7909 that were not caught partially because the badImport test had been disabled.

Bugs Fixed:

  • Building by path no longer drops top-level logs.
  • "bad import" errors are once again printed.
  • Transitively imported precompiled modules are once again loaded during elaboration.

@tydeu tydeu added the changelog-lake Lake label Apr 19, 2025
@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 Apr 19, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 19, 2025
Update lean-toolchain for testing leanprover/lean4#8026
2d6ec2d
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 19, 2025
Update lean-toolchain for testing leanprover/lean4#8026
d5dd89b
@tydeu tydeu added the release-ci Enable all CI checks for a PR, like is done for releases label Apr 19, 2025
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 19, 2025
@ghost
Copy link
Copy Markdown

ghost commented Apr 19, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

@tydeu tydeu marked this pull request as ready for review April 19, 2025 20:22
@tydeu tydeu removed the release-ci Enable all CI checks for a PR, like is done for releases label Apr 19, 2025
@tydeu tydeu force-pushed the lake/fix-badImport branch from 75ac3a6 to a042ab7 Compare April 19, 2025 20:25
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 19, 2025
Trigger CI for leanprover/lean4#8026
99899c6
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 19, 2025
Trigger CI for leanprover/lean4#8026
df74a88
@tydeu tydeu added this pull request to the merge queue Apr 19, 2025
Merged via the queue into leanprover:master with commit 72e4f69 Apr 19, 2025
17 checks passed
@tydeu tydeu mentioned this pull request Apr 30, 2025
Merged
tydeu added a commit that referenced this pull request May 1, 2025
@tydeu
chore: lake: backport dynlib fixes (#8187)
6caaee8 
This PR backports fixes to dynamic library linking and loading in Lake
to `v4.19.0`.

Includes changes from #7809, #8026, #8152, and #8190.
@tydeu tydeu deleted the lake/fix-badImport branch May 17, 2025 00:12
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 changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@tydeu