sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat: Lake shared library (#5143)

Browse Source 
Fixes #2436 #5050

Next step: when libLake_shared is in stage 0, --load-dynlib it when
building stage 1 Lake
This commit is contained in:
Sebastian Ullrich
2024-09-09 11:05:54 +02:00
committed by GitHub
parent ec7ae59473
commit c2761dc270
6 changed files with 52 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
script/lib/update-stage0
View File

@@ -18,7 +18,7 @@ done
# special handling for Lake files due to its nested directory
# copy the README to ensure the `stage0/src/lake` directory is comitted
for f in $(git ls-files 'src/lake/Lake/*' src/lake/Lake.lean src/lake/README.md ':!:src/lakefile.toml'); do
for f in $(git ls-files 'src/lake/Lake/*' src/lake/Lake.lean src/lake/LakeMain.lean src/lake/README.md ':!:src/lakefile.toml'); do
if [[ $f == *.lean ]]; then
f=${f#src/lake}
f=${f%.lean}.c