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

chore: go back to previous bootstrapping scheme where the stage N+1 stdlib is created using the stage N compiler

Browse Source
This commit is contained in:
Sebastian Ullrich
2020-09-23 14:47:46 +02:00
parent 308b4fc421
commit c54d51b0c9
9 changed files with 94 additions and 122 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
.github/workflows/ci.yml vendored
View File

@@ -86,23 +86,23 @@ jobs:
make -j4
# de-Nix-ify binary
- name: Patch
run: patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 --remove-rpath build/stage0.5/bin/lean
run: patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 --remove-rpath build/stage1/bin/lean
if: matrix.name == 'Linux release'
- name: Patch
run: |
for lib in $(otool -L build/stage0.5/bin/lean | tail -n +2 | cut -d' ' -f1); do
install_name_tool -change "$lib" "/usr/lib/$(basename $lib | sed 's/libc++\.1\.0/libc++.1/')" build/stage0.5/bin/lean
for lib in $(otool -L build/stage1/bin/lean | tail -n +2 | cut -d' ' -f1); do
install_name_tool -change "$lib" "/usr/lib/$(basename $lib | sed 's/libc++\.1\.0/libc++.1/')" build/stage1/bin/lean
done
if: matrix.name == 'macOS'
- name: Pack
run: cd build/stage0.5; cpack
run: cd build/stage1; cpack
- uses: actions/upload-artifact@v2
with:
name: build-${{ matrix.name }}
path: build/stage0.5/lean-*
path: build/stage1/lean-*
- name: Test
run: |
cd build/stage0.5
cd build/stage1
ctest -j4 --output-on-failure < /dev/null
- name: Build Stage 2
run: |
@@ -116,7 +116,7 @@ jobs:
if: matrix.check-stage3
- name: Test Speedcenter Benchmarks
run: |
export BUILD=$PWD/build PATH=$PWD/build/stage0.5/bin:$PATH
export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
cd tests/bench; temci exec --config speedcenter.yaml --included_blocks fast --runs 1
if: matrix.test-speedcenter
- name: Check rebootstrap

44
CMakeLists.txt
View File

@@ -12,8 +12,6 @@ endforeach()
include(ExternalProject)
project(LEAN CXX C)
# use the same library sources everywhere; this only important for stage 0 since the compiler source for it come from stage0/src
list(APPEND CL_ARGS "-DLIB_SOURCE_DIR=${LEAN_SOURCE_DIR}/src")
ExternalProject_add(stage0
SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
@@ -24,41 +22,21 @@ ExternalProject_add(stage0
BUILD_ALWAYS ON # cmake doesn't auto-detect changes without a download method
INSTALL_COMMAND "" # skip install
)
ExternalProject_add(stage0.5
SOURCE_DIR "${LEAN_SOURCE_DIR}"
SOURCE_SUBDIR src
BINARY_DIR stage0.5
CMAKE_ARGS -DSTAGE=0.5 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 ${CL_ARGS}
BUILD_ALWAYS ON
INSTALL_COMMAND ""
DEPENDS stage0
)
ExternalProject_add(stage1
SOURCE_DIR "${LEAN_SOURCE_DIR}"
SOURCE_SUBDIR src
BINARY_DIR stage1
# reuse libleancpp.a, which doesn't change
CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DLEANCPP="${CMAKE_BINARY_DIR}/stage0.5/lib/lean/libleancpp.a" ${CL_ARGS}
CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 ${CL_ARGS}
BUILD_ALWAYS ON
INSTALL_COMMAND ""
DEPENDS stage0 stage0.5
EXCLUDE_FROM_ALL ON
)
ExternalProject_add(stage1.5
SOURCE_DIR "${LEAN_SOURCE_DIR}"
SOURCE_SUBDIR src
BINARY_DIR stage1.5
CMAKE_ARGS -DSTAGE=1.5 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DLEANCPP="${CMAKE_BINARY_DIR}/stage0.5/lib/lean/libleancpp.a" ${CL_ARGS}
BUILD_ALWAYS ON
INSTALL_COMMAND ""
DEPENDS stage1
EXCLUDE_FROM_ALL ON
DEPENDS stage0
)
ExternalProject_add(stage2
SOURCE_DIR "${LEAN_SOURCE_DIR}"
SOURCE_SUBDIR src
BINARY_DIR stage2
CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DLEANCPP="${CMAKE_BINARY_DIR}/stage0.5/lib/lean/libleancpp.a" ${CL_ARGS}
# reuse libleancpp.a, which doesn't change
CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DLEANCPP="${CMAKE_BINARY_DIR}/stage1/lib/lean/libleancpp.a" ${CL_ARGS}
BUILD_ALWAYS ON
INSTALL_COMMAND ""
DEPENDS stage1
@@ -68,9 +46,7 @@ ExternalProject_add(stage3
SOURCE_DIR "${LEAN_SOURCE_DIR}"
SOURCE_SUBDIR src
BINARY_DIR stage3
CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DLEANCPP="${CMAKE_BINARY_DIR}/stage0.5/lib/lean/libleancpp.a" ${CL_ARGS}
# skip building library - if `lean` is the same as in stage2, the library will be as well
BUILD_COMMAND $(MAKE) lean
CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DLEANCPP="${CMAKE_BINARY_DIR}/stage1/lib/lean/libleancpp.a" ${CL_ARGS}
BUILD_ALWAYS ON
INSTALL_COMMAND ""
DEPENDS stage2
@@ -80,14 +56,14 @@ ExternalProject_add(stage3
# targets forwarded to appropriate stages
add_custom_target(update-stage0
COMMAND $(MAKE) -C stage0 update-stage0
DEPENDS stage0)
COMMAND $(MAKE) -C stage1 update-stage0
DEPENDS stage1)
add_custom_target(test
COMMAND $(MAKE) -C stage0.5 test
DEPENDS stage0.5)
COMMAND $(MAKE) -C stage1 test
DEPENDS stage1)
install(CODE "execute_process(COMMAND make -C stage0.5 install)")
install(CODE "execute_process(COMMAND make -C stage1 install)")
add_custom_target(check-stage3
COMMAND diff "stage2/bin/lean" "stage3/bin/lean"

94
doc/make/index.md
View File

@@ -39,7 +39,7 @@ cmake -D CMAKE_BUILD_TYPE=DEBUG ../..
make
```
This will compile the Lean library and binary into the `stage0.5` subfolder; see
This will compile the Lean library and binary into the `stage1` subfolder; see
below for details. Add `-jN` for an appropriate `N` to `make` for a parallel
build.
@@ -79,74 +79,72 @@ point. The build directory is organized in these stages:
```bash
stage0/
bin/
lean # the Lean compiler & server
leanc # a wrapper around a C compiler supplying search paths etc
leanmake # a wrapper around `make` supplying the Makefile below
lib/
lean/**/*.olean # the Lean library (incl. the compiler) compiled by `lean` above
temp/**/*.{c,o} # the library extracted to C and compiled by `leanc`
libInit.a # a static library of the Lean library
libleancpp.a # a static library of the C++ sources of Lean
# Bootstrap binary built from stage0/src/.
# We do not use any other files from this directory in further stages.
bin/lean
stage1/
include/
config.h # config variables used to build `lean` such as use allocator
runtime/lean.h # runtime headers, used by extracted C code, uses `config.h`
share/lean/
Makefile # used by `leanmake`
stage1/...
lib/
lean/**/*.olean # the Lean library (incl. the compiler) compiled by the previous stage's `lean`
temp/**/*.{c,o} # the library extracted to C and compiled by `leanc`
libInit.a libStd.a libLean.a # static libraries of the Lean library
libleancpp.a # a static library of the C++ sources of Lean
bin/
lean # the Lean compiler & server linked together from the above libraries
leanc # a wrapper around a C compiler supplying search paths etc
leanmake # a wrapper around `make` supplying the Makefile above
stage2/...
stage3/...
```
The build for each stage starts by assembling `bin/lean` from the `libInit.a` of
the preceding stage and `libleancpp.a` built from `src/`; in the case of stage 0,
which doesn't have a preceding stage, both libraries are instead assembled from
`stage0/src`, which contains the C++ and extracted C code of a previous commit of
Lean. This Lean binary is then used to compile the Lean library into .olean files
and ultimately a new `libInit.a`, which is then used by the next stage.
Stage 0 can be viewed as a blackbox since it does not depend on any local
changes and is equivalent to downloading a bootstrapping binary as done in other
compilers. The build for any other stage starts by building the runtime and
standard library from `src/`, using the `lean` binary from the previous stage in
the latter case, which are then assembled into a new `bin/lean` binary.
Each stage can be built by calling `make stageN` in the root build folder. It is
usually not necessary to compile all stages in order to test a change. Stage 3 in
fact should usually be identical to stage 2 and only exists as a sanity check,
which can be done via `make check-stage3`. Building stage 2 should only be
necessary for testing how changes in the compiler influence compilation of the
compiler itself, e.g. checking if an optimization speeds up (or breaks) the
compiler. Stage 1 is sufficient for testing changes on the library and test
programs. In fact, if the stage 0 library and the stage 1 are compatible (use the
same Lean ABI, so to speak), we can avoid even rebuilding the stage 1 library
using a special stage "0.5" that combines the stage 1 compiler with the stage 0
library. Most changes do not break this ABI, so running `make` by itself in the
root build folder will default to `make stage0.5`. There is also an analogous
stage 1.5, which should be sufficient for testing changes to *meta*programs on
the stdlib.
Each stage can be built by calling `make stageN` in the root build folder.
Running just `make` will default to stage 1, which is usually sufficient for
testing changes on the test suite or other files outside of the stdlib. However,
it might happen that the stage 1 compiler is not able to load its own stdlib,
e.g. when changing the .olean format: the stage 1 stdlib will use the format
generated by the stage 0 compiler, but the stage 1 compiler will expect the new
format. In this case, we should continue with building and testing stage 2
instead, which will both build and expect the new format. Note that this is only
possible because when building a stage's stdlib, we use the previous compiler
but never load the previous stdlib (since everything is `prelude`). We can also
use stage 2 to test changes in the compiler or other "meta" parts, i.e. changes
that affect the produced (.olean or .c) code, on the stdlib and compiler itself.
We are not aware of any "meta-meta" parts that influence more than two stages of
compilation, so stage 3 should always be identical to stage 2 and only exists as
a sanity check.
In summary, doing a standard build via `make` involves these steps:
1. compile the `stage0/src` archived sources into `stage0/bin/lean`
1. use it to compile the library (*including* your changes) into `stage0/lib`
1. link that and the *current* C++ code from `src/` into `stage1/bin/lean`
1. copy ("uplift") the Lean library from `stage0/lib` into `stage1/lib`
1. use it to compile the current library (*including* your changes) into `stage1/lib`
1. link that and the current C++ code from `src/` into `stage1/bin/lean`
You now have a Lean binary and library that include your changes, though their
own compilation was not influenced by them, that you can use to test your changes
on test programs whose compilation *will* be influenced by the changes.
own compilation was not influenced by them, that you can use to test your
changes on test programs whose compilation *will* be influenced by the changes.
Finally, when we want to use new language features in the library, we need to
update the stage 0 compiler, which can be done via `make -C stageN update-stage0`.
Note: you cannot do this for stage 0.5 because the extracted C files are not
copied over from stage 0 to that stage, so just use stage 0 instead.
`make update-stage0` without `-C` defaults to stage0 for this reason. If updating
stage 0 from stage 0 sounds wrong to you, just remember that the stage 0 build
directory contains the *output* of the stage 0 compiler!
`make update-stage0` without `-C` defaults to stage1.
Development Setup
-----------------
After building a stage, you can invoke `make -C stageN test` (or, even better,
`make -C stageN ARGS=-j` to make `ctest` parallel) to run the Lean test suite.
`make test` without `-C` defaults to stage 0.5. While the Lean tests
will automatically use that stage's corresponding Lean executables, for running
tests or compiling Lean programs manually, you need to put them into your `PATH`
`make test` without `-C` defaults to stage1. While the Lean tests will
automatically use that stage's corresponding Lean executables, for running tests
or compiling Lean programs manually, you need to put them into your `PATH`
yourself. A simple option for doing that is to use
[`elan`](https://github.com/Kha/elan), see the next section.
@@ -156,7 +154,7 @@ basic setup. You can set `lean4-rootdir` manually to tell it what stage to use:
# while editing the Lean library
M-x set-variable lean4-rootdir RET ".../build/release/stage0" RET
# while testing, using a Lean that includes your changes
M-x set-variable lean4-rootdir RET ".../build/release/stage0.5" RET
M-x set-variable lean4-rootdir RET ".../build/release/stage1" RET
```
but `elan` again makes it simple to do that automatically, see below.
@@ -175,12 +173,12 @@ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s
You can use `elan toolchain link` to give a specific stage build directory a
reference name, then use `elan override set` to associate such a name to the
current directory. We usually want to use `stage0` for editing files in `src`
and `stage0.5` for everything else (e.g. tests).
and `stage1` for everything else (e.g. tests).
```
# in the Lean rootdir
elan toolchain link lean4 build/release/stage0.5
elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0
# make `lean` etc. point to stage0.5 in the rootdir and subdirs
# make `lean` etc. point to stage1 in the rootdir and subdirs
elan override set lean4
cd src
# make `lean` etc. point to stage0 anywhere inside `src`

34
src/CMakeLists.txt
View File

@@ -533,25 +533,49 @@ else()
endif()
install(FILES ${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a DESTINATION lib/lean)
if(NOT(${STAGE} EQUAL 0))
# created by the previous stage
# make stdlib using previous stage
if(PREV_STAGE)
# MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${PREV_STAGE}/bin")
# ...and Make doesn't like absolute Windows paths either
# (also looks nicer in the build log)
file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
add_custom_target(make_stdlib ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
# The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
# for a parallelized nested build, but CMake doesn't let us do that.
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make)
add_library(Init STATIC IMPORTED)
set_target_properties(Init PROPERTIES
IMPORTED_LOCATION "${PREV_STAGE}/lib/lean/libInit.a")
IMPORTED_LOCATION ${CMAKE_BINARY_DIR}/lib/lean/libInit.a)
add_dependencies(Init make_stdlib)
add_library(Std STATIC IMPORTED)
set_target_properties(Std PROPERTIES
IMPORTED_LOCATION "${PREV_STAGE}/lib/lean/libStd.a")
IMPORTED_LOCATION ${CMAKE_BINARY_DIR}/lib/lean/libStd.a)
add_dependencies(Std make_stdlib)
add_library(Lean STATIC IMPORTED)
set_target_properties(Lean PROPERTIES
IMPORTED_LOCATION "${PREV_STAGE}/lib/lean/libLean.a")
IMPORTED_LOCATION ${CMAKE_BINARY_DIR}/lib/lean/libLean.a)
add_dependencies(Lean make_stdlib)
# leancpp and the Lean libs are cyclically dependent
target_link_libraries(Init INTERFACE leancpp)
target_link_libraries(Std INTERFACE leancpp Init)
target_link_libraries(Lean INTERFACE leancpp Std Init)
target_link_libraries(leancpp INTERFACE Init Std Lean)
add_custom_target(update-stage0
COMMAND cmake -E env LIB=${CMAKE_BINARY_DIR}/lib bash script/update-stage0
DEPENDS make_stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")
endif()
target_link_libraries(leancpp INTERFACE ${EXTRA_LIBS})

2
src/Lean/Server/lean4-lsp.el
View File

@@ -37,7 +37,7 @@
'(lean4-lsp-mode . "lean4"))
(defconst lean4-server-bin (concat lean4-home "/src/Lean/Server/build/bin/ServerBin"))
(defconst lean4-lib (concat lean4-home "/build/release/stage0.5/lib/lean/"))
(defconst lean4-lib (concat lean4-home "/build/release/stage1/lib/lean/"))
(lsp-register-client
(make-lsp-client :new-connection (lsp-stdio-connection lean4-server-bin)

21
src/shell/CMakeLists.txt
View File

@@ -10,27 +10,8 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
endif()
install(TARGETS lean DESTINATION bin)
string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
# MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
# use executable of current stage for tests
string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
# ...and Make doesn't like absolute Windows paths either
# (also looks nicer in the build log)
file(RELATIVE_PATH LIB ${LIB_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
add_custom_target(make_stdlib ALL
WORKING_DIRECTORY ${LIB_SOURCE_DIR}
# The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
# for a parallelized nested build, but CMake doesn't let us do that.
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make
DEPENDS lean)
add_custom_target(update-stage0
COMMAND cmake -E env LIB=${CMAKE_BINARY_DIR}/lib bash script/update-stage0
DEPENDS make_stdlib
WORKING_DIRECTORY "${LIB_SOURCE_DIR}/..")
# add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_BINARY_DIR}/bin/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
# add_test(lean_export ${CMAKE_BINARY_DIR}/bin/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")

7
src/stdlib.make.in
View File

@@ -10,14 +10,7 @@ LEANMAKE_OPTS+=\
CMAKE_LIKE_OUTPUT=1
stdlib:
ifeq ($(patsubst %.5,.5,${STAGE}), .5)
# In the case of stage n.5, we simply copy .olean files and libInit.a from stage n (but not libleancpp.a,
# which is different from stage 0).
mkdir -p "${LIB}/lean"
cp -rf $$(find "${PREV_STAGE}/lib/lean" -mindepth 1 -maxdepth 1 -not -name libleancpp.a) "${LIB}/lean"
else
# Use `+` to use the Make jobserver with `leanmake` for parallelized builds
+"${LEAN_BIN}/leanmake" lib PKG=Init $(LEANMAKE_OPTS)
+"${LEAN_BIN}/leanmake" lib PKG=Std $(LEANMAKE_OPTS)
+"${LEAN_BIN}/leanmake" lib PKG=Lean $(LEANMAKE_OPTS)
endif

BIN
stage0/src/CMakeLists.txt generated
View File

Binary file not shown.

BIN
stage0/src/shell/CMakeLists.txt generated
View File

Binary file not shown.