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: Lake shared library #5143

Merged
merged 15 commits into from
Sep 9, 2024
Merged

feat: Lake shared library #5143

merged 15 commits into from
Sep 9, 2024

Conversation

Kha
Copy link
Member

@Kha Kha commented Aug 23, 2024 •
edited
Loading

Fixes #2436 #5050

Next step: when libLake_shared is in stage 0, --load-dynlib it when building stage 1 Lake

@Kha Kha requested a review from tydeu as a code owner August 23, 2024 10:01
@Kha Kha added the release-ci Enable all CI checks for a PR, like is done for releases label Aug 23, 2024
@Kha
Copy link
Member Author

Kha commented Aug 23, 2024

@tydeu Moving Lake.Main out of Lake/ seemed like the easiest option to exclude it from the library outputs

@tydeu
Copy link
Member

tydeu commented Aug 24, 2024 •
edited
Loading

@Kha Sounds good to me! 😄 Style-wise. I would probably just name it Main.lean unless that is an issue. The reason being the file is already under src/lake and Main.lean is currently the standard naming convention used by executable templates. Functionally-wise, the TOML configurations need updating to point the lean_exe to the new module (i.e., in src/lake/lakefile.toml and src/lakefile.toml.in).

@Kha
Copy link
Member Author

Kha commented Aug 26, 2024

The reason being the file is already under src/lake

I was hoping it would not stay there :)

@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 Aug 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Aug 28, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5143
0768e48
@Kha Kha removed the release-ci Enable all CI checks for a PR, like is done for releases label Aug 29, 2024
@Kha Kha linked an issue Aug 29, 2024 that may be closed by this pull request
Broken Lake linking #5050
Closed
@Kha
Copy link
Member Author

Kha commented Aug 29, 2024

@tydeu I don't actively use the TOML files atm and don't want to touch them without testing, could you update them in a separate PR?

@Kha Kha enabled auto-merge August 29, 2024 11:03
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Aug 29, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5143
6665fee
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Aug 29, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5143
440e156
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Aug 29, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5143
9152944
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 2, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5143
aa08400
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 3, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5143
6a2750d
@Kha Kha added this pull request to the merge queue Sep 9, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 9, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5143
997395d
Merged via the queue into leanprover:master with commit c2761dc Sep 9, 2024
14 checks passed
@Kha Kha deleted the lake-linking branch September 9, 2024 09:41
tobiasgrosser pushed a commit to opencompl/lean4 that referenced this pull request Sep 16, 2024
@Kha @tobiasgrosser
feat: Lake shared library (leanprover#5143)
c20d71f 
Fixes leanprover#2436 leanprover#5050

Next step: when libLake_shared is in stage 0, --load-dynlib it when
building stage 1 Lake
@tydeu tydeu mentioned this pull request Sep 25, 2024
Merged
github-merge-queue bot pushed a commit that referenced this pull request Sep 25, 2024
@tydeu
chore: update src/lake/lakefie.toml (#5462)
7845a05 
Update the Lake-specific package configuration with the proper root for
the executable (after #5143).
@tydeu tydeu mentioned this pull request Oct 16, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

Assignees
No one assigned
Labels
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.

Broken Lake linking Lake native libraries include main symbol
2 participants
@Kha @tydeu