max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: move bin/ and .oleans into build directory

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-06 11:33:59 +02:00
parent 73b4cf329d
commit 10253e89ea
19 changed files with 545 additions and 357 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
.gitignore vendored
View file

@ -1,8 +1,6 @@
*~
\#*
.#*
*.olean
*.depend
*.lock
build
GPATH
@ -12,9 +10,6 @@ GTAGS
.projectile
.lean_options
.vs
/src/stage1
/src/config.h
/stage0/src/config.h
compile_commands.json
*.idea
tasks.json
@ -24,4 +19,3 @@ settings.json
*.produced.out
CMakeSettings.json
CppProperties.json
/src/Makefile

9
bin/.gitignore vendored
View file

@ -1,9 +0,0 @@
lean
lean.exe
leanc
lean_stage0
lean_stage0.exe
lean_stage2
lean_stage2.exe
*.a
*.so

17
bin/lean_wrapped
View file

@ -1,17 +0,0 @@
#!/usr/bin/env bash
# Call `lean_stage0` when in src/Init; otherwise call `lean`.
bin=$(dirname $(realpath $0))
lib=$(dirname $bin)/src/Init
# use dir of input file, or pwd if stdin
if [[ "$*" == *--stdin* ]]; then
dir=$(pwd)
else
dir=$(dirname $(realpath ${@:$#}))
fi
# check if `dir` starts with `$lib`
if [[ ${dir##$lib} != $dir ]]; then
$bin/lean_stage0 $*
else
$bin/lean $*
fi

2
lean4-mode/lean4-settings.el
View file

@ -21,7 +21,7 @@
(defvar-local lean4-default-executable-name
(cl-case system-type
('windows-nt "lean.exe")
(t "lean_wrapped"))
(t "lean"))
"Default executable name of Lean")
(defcustom lean4-rootdir nil

3
shell.nix
View file

@ -14,9 +14,6 @@ let attribs = rec {
recipe = pkgs.writeText "recipe" ''
(lean4-mode :repo "leanprover/lean4" :fetcher github :files ("*.el"))
'';
patchPhase = ''
sed -i 's/lean_wrapped/lean/' *.el
'';
fileSpecs = [ "*.el" ];
};
emacs = pkgs.emacsWithPackages (epkgs:

91
src/CMakeLists.txt
View file

@ -459,8 +459,8 @@ if(USE_GITHASH)
get_git_head_revision(GIT_REFSPEC GIT_SHA1)
if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
message(STATUS "Failed to read git_sha1")
if(EXISTS "${LEAN_SOURCE_DIR}/../bin/package_version")
file(STRINGS "${LEAN_SOURCE_DIR}/../bin/package_version" LEAN_PACKAGE_VERSION)
if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
endif()
else()
@ -468,8 +468,8 @@ if(USE_GITHASH)
endif()
else()
set(GIT_SHA1 "GITDIR-NOTFOUND")
if(EXISTS "${LEAN_SOURCE_DIR}/../bin/package_version")
file(STRINGS "${LEAN_SOURCE_DIR}/../bin/package_version" LEAN_PACKAGE_VERSION)
if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
endif()
endif()
@ -483,14 +483,9 @@ endif ()
# Version
configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
# Remark: we did not put `config.h` in `${LEAN_BINARY_DIR}` because `leanc` depends on this file.
# Note that, `leanc` already had problems with multiple configurations before we added `config.h`.
# For example, it uses binary files located in the `bin` directory.
configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_SOURCE_DIR}/config.h")
install(FILES "${LEAN_SOURCE_DIR}/config.h" DESTINATION "${INCLUDE_DIR}")
if(NOT STAGE0)
configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_SOURCE_DIR}/Makefile")
endif()
configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/config.h")
install(FILES "${LEAN_SOURCE_DIR}/include/config.h" DESTINATION "${INCLUDE_DIR}")
configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_BINARY_DIR}/share/lean/Makefile")
include_directories("${LEAN_BINARY_DIR}")
add_subdirectory(runtime)
@ -515,7 +510,6 @@ add_subdirectory(initialize)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
if(STAGE0)
add_subdirectory(../stdlib stdlib)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:stage0>)
endif()
if(EMSCRIPTEN)
set(LEAN_LIBRARY_TYPE SHARED)
@ -534,7 +528,7 @@ if(NOT STAGE0)
-DCHECK_OLEAN_VERSION=${CHECK_OLEAN_VERSION}
"-DCMAKE_C_COMPILER=${CMAKE_C_COMPILER}"
"-DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}"
BUILD_COMMAND $(MAKE) lean # build executable only
BUILD_COMMAND $(MAKE) # build executable only
BUILD_ALWAYS ON # cmake doesn't auto-detect changes without a download method
INSTALL_COMMAND "" # skip install
)
@ -542,42 +536,36 @@ endif()
add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
target_link_libraries(leanstatic ${EXTRA_LIBS})
set_target_properties(leanstatic PROPERTIES ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib")
if(LLVM)
target_link_libraries(leanstatic ${llvm_libs})
endif()
if(NOT STAGE0)
if(STAGE0)
add_library(leanstdlib STATIC $<TARGET_OBJECTS:stage0>)
else()
add_library(leanstdlib STATIC IMPORTED)
ADD_CUSTOM_TARGET(bin_lib ALL
COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "$<TARGET_FILE:leanstdlib>" "$<TARGET_FILE:leanstatic>" "${LEAN_SOURCE_DIR}/../bin"
)
# Configure leanc
configure_file("${LEAN_SOURCE_DIR}/../bin/leanc.in" "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc")
file(COPY "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc"
DESTINATION "${LEAN_SOURCE_DIR}/../bin"
FILE_PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
install(FILES "${LEAN_SOURCE_DIR}/../bin/leanc"
DESTINATION bin
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
add_custom_target(bin ALL)
add_dependencies(bin bin_lib bin_lean)
endif()
# The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).
# For some strange reason, it contains a copy of pthread_equal.
# Remark: this problem does not happen when we generate the DLL using msys2 on Windows.
if (NOT("${CROSS_COMPILE}" MATCHES "ON"))
if ("${STATIC}" MATCHES "OFF")
add_library(leanshared SHARED shared/init.cpp)
# see `target_link_libraries(lean ...)`
target_link_libraries(leanshared leanstatic leanstdlib leanstatic leanstdlib)
install(TARGETS leanshared DESTINATION lib)
endif()
install(TARGETS leanstatic DESTINATION lib)
endif()
configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc")
install(FILES "${CMAKE_BINARY_DIR}/bin/leanc"
DESTINATION bin
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
# shared library deactivated until we figure out the leanstatic/leanstdlib story
# # The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).
# # For some strange reason, it contains a copy of pthread_equal.
# # Remark: this problem does not happen when we generate the DLL using msys2 on Windows.
# if (NOT("${CROSS_COMPILE}" MATCHES "ON"))
# if ("${STATIC}" MATCHES "OFF")
# add_library(leanshared SHARED shared/init.cpp)
# # see `target_link_libraries(lean ...)`
# target_link_libraries(leanshared leanstatic leanstdlib leanstatic leanstdlib)
# install(TARGETS leanshared DESTINATION lib)
# endif()
# install(TARGETS leanstatic DESTINATION lib)
# endif()
add_subdirectory(shell)
@ -618,24 +606,23 @@ add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cma
endif()
add_custom_target(clean-stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
COMMAND find . -name '*.olean' -delete
COMMAND find . -name '*.depend' -delete
COMMAND rm -rf ../stage1 "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true
)
COMMAND rm -rf "${CMAKE_BINARY_DIR}/lib" "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true)
add_custom_target(clean-olean
DEPENDS clean-stdlib)
install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}"
install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}/lean"
FILES_MATCHING
PATTERN "*.olean")
install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}/lean/src"
FILES_MATCHING
PATTERN "*.lean"
PATTERN "*.olean"
PATTERN "*.md")
install(DIRECTORY "${CMAKE_SOURCE_DIR}/runtime" DESTINATION "${INCLUDE_DIR}"
FILES_MATCHING
PATTERN "*.h")
add_custom_target(include_runtime ALL
COMMAND cmake -E copy_directory "${CMAKE_SOURCE_DIR}/runtime" "${CMAKE_BINARY_DIR}/include/runtime")
install(FILES "${CMAKE_SOURCE_DIR}/runtime/lean.h" DESTINATION "${INCLUDE_DIR}/runtime")
if("${INCLUDE_MSYS2_DLLS}" MATCHES "ON")
# TODO(Leo): do not use hardlinks to required DLLs.

47
src/Makefile.in
View file

@ -1,21 +1,15 @@
# Copyright (c) 2018 Simon Hudon. All rights reserved.
# Released under Apache 2.0 license as described in the file LICENSE.
# Authors: Simon Hudon, Sebastian Ullrich, Leonardo de Moura
LEAN ?= ../bin/lean
LEANC ?= ../bin/leanc
LEAN_ROOT ?= .
# Even though we copy the sources into a new directory for stage2/3, we
# read the list of files to compile from the original directory to avoid
# issues with stale copied files
SRCS = $(shell cd $(LEAN_ROOT); find . -name '*.lean')
DEPS = $(addprefix $(LEAN_ROOT)/,$(SRCS:.lean=.depend))
SRCS = $(shell find Init -name '*.lean')
DEPS = $(addprefix $(OUT)/temp/,$(SRCS:.lean=.depend))
OPTS = @LEAN_EXTRA_MAKE_OPTS@
STAGE0_DIR = ../stage0
C_OUT ?= .
ifndef OUT
$(error "`OUT` must be set (use cmake)")
endif
OBJS = $(SRCS:.lean=.olean)
export LEAN_PATH=Init=$(OUT)/lean/Init
OBJS = $(addprefix $(OUT)/lean/, $(SRCS:.lean=.olean))
# ensure deterministic ordering
CS_CORE=$(sort $(SRCS:.lean=.c))
@ -23,44 +17,49 @@ SHELL = /usr/bin/env bash -eo pipefail
.PHONY: all clean
all: $(OBJS)
all: $(OBJS) $(OUT)/libleanstdlib.a
depends: $(DEPS)
%.depend: %.lean
# use separate assignment to ensure failure propagation
@deps=`$(LEAN) --deps $< | python relative.py`; echo $(<:.lean=.olean): $$deps > $@
$(OUT)/lean/Init:
@mkdir -p "$@"
%.olean: %.lean %.depend $(MORE_DEPS)
$(OUT)/temp/%.depend: %.lean | $(OUT)/lean/Init
@mkdir -p "$(OUT)/temp/$(*D)"
# use separate assignment to ensure failure propagation
# convert file separators and newlines on Windows
@deps=`lean --deps $< | sed 's!\\\\!/!g;s/\\r//'`; echo $(OUT)/lean/$(<:.lean=.olean): $$deps > $@
$(OUT)/lean/%.olean: %.lean $(OUT)/temp/%.depend $(MORE_DEPS)
@echo "[ ] Building $<"
@mkdir -p $(C_OUT)/$(*D)
$(LEAN) $(OPTS) -o "$@" --c="$(C_OUT)/$*.c.tmp" $<
@mkdir -p $(OUT)/lean/$(*D)
lean $(OPTS) -o "$@" --c="$(OUT)/temp/$*.c.tmp" $<
# create the .c file atomically
mv "$(C_OUT)/$*.c.tmp" "$(C_OUT)/$*.c"
mv "$(OUT)/temp/$*.c.tmp" "$(OUT)/temp/$*.c"
# make sure the .olean file is newer than the .depend file to prevent infinite make cycles
@touch $@
$(C_OUT)/%.c: %.olean
$(OUT)/temp/%.c: $(OUT)/lean/%.olean
@
$(OUT)/%.o: $(C_OUT)/%.c
$(OUT)/temp/%.o: $(OUT)/temp/%.c
@echo "[ ] Building $<"
@mkdir -p "$(@D)"
$(LEANC) -c -o $@ $< $(LEANC_OPTS)
leanc -c -o $@ $< $(LEANC_OPTS)
$(OUT)/libleanstdlib.a: $(addprefix $(OUT)/,$(SRCS:.lean=.o))
$(OUT)/libleanstdlib.a: $(addprefix $(OUT)/temp/,$(SRCS:.lean=.o))
@rm -f $@
@ar rcs $@ $^
update-stage0:
-rm -r $(STAGE0_DIR)
-mkdir -p $(STAGE0_DIR)/stdlib
for f in $(SRCS:.lean=.c); do mkdir -p `dirname $(STAGE0_DIR)/stdlib/$$f`; cp $(C_OUT)/$$f $(STAGE0_DIR)/stdlib/$$f; done
for f in $(SRCS:.lean=.c); do mkdir -p `dirname $(STAGE0_DIR)/stdlib/$$f`; cp $(OUT)/$$f $(STAGE0_DIR)/stdlib/$$f; done
echo "add_library (stage0 OBJECT $(CS_CORE))" > $(STAGE0_DIR)/stdlib/CMakeLists.txt
# don't copy untracked crap
git ls-files -z . | xargs -0 -I '{}' bash -c 'mkdir -p `dirname ../stage0/src/{}` && cp {} ../stage0/src/{}'
-git add $(STAGE0_DIR)
.PRECIOUS: %.depend $(C_OUT)/%.c
.PRECIOUS: %.depend $(OUT)/temp/%.c
include $(DEPS)

0
bin/lean-gdb.py → src/bin/lean-gdb.py
View file

0
bin/leanc.in → src/bin/leanc.in Normal file → Executable file
View file

14
src/relative.py
View file

@ -1,14 +0,0 @@
# Copyright (c) 2018 Microsoft Corporation. All rights reserved.
# Released under Apache 2.0 license as described in the file LICENSE.
# Authors: Simon Hudon, Sebastian Ullrich
import sys
import os
import re
for x in sys.stdin:
# HACK: rewrite Windows path to mingw path
x = re.sub(r"^(\w):", lambda m: "/" + m[1].lower(), x).replace('\\', '/').strip()
curr = os.path.realpath(os.curdir)
curr = os.path.normpath(curr)
print(os.path.relpath(x, curr))

6
src/runtime/CMakeLists.txt
View file

@ -4,9 +4,3 @@ serializer.cpp stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp)
add_library(runtime OBJECT ${RUNTIME_OBJS})
add_library(leanruntime ${RUNTIME_OBJS})
ADD_CUSTOM_TARGET(bin_runtime ALL
COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/libleanruntime.a" "${LEAN_SOURCE_DIR}/../bin"
DEPENDS leanruntime
)

121
src/shell/CMakeLists.txt
View file

@ -1,75 +1,56 @@
if(NOT STAGE0)
add_executable(lean_stage0 IMPORTED)
set_target_properties(lean_stage0 PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage0/shell/lean${CMAKE_EXECUTABLE_SUFFIX}")
ADD_CUSTOM_TARGET(bin_lean_stage0
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean_stage0>" "${LEAN_SOURCE_DIR}/../bin/lean_stage0${CMAKE_EXECUTABLE_SUFFIX}"
DEPENDS stage0
)
string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
add_custom_target(make_stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=Init=Init" $(MAKE) "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
"LEAN=$<TARGET_FILE:lean_stage0>"
"LEANC_OPTS=${LEANC_OPTS}"
"OUT=${CMAKE_BINARY_DIR}/stage1"
# share .c files between different build configurations
"C_OUT=${LEAN_SOURCE_DIR}/stage1"
COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/stage0/bin:$$PATH $(MAKE) -f ${CMAKE_BINARY_DIR}/share/lean/Makefile OUT=${CMAKE_BINARY_DIR}/lib"
DEPENDS stage0)
set_target_properties(leanstdlib PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/libleanstdlib.a"
IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
add_dependencies(leanstdlib make_stdlib)
install(FILES "$<TARGET_FILE:leanstdlib>" DESTINATION lib)
set(PREV_LEAN "$<TARGET_FILE:lean>")
set(PREV_STAGE_DIR "${CMAKE_BINARY_DIR}")
set(PREV_STAGE_TARGET lean)
foreach(STAGE RANGE 2 3)
add_custom_target(make_stdlib_stage${STAGE}
COMMAND cd "${LEAN_SOURCE_DIR}" && find . '\(' -name Makefile -o -name relative.py -o -name '*.lean' '\)' -exec "${CMAKE_COMMAND}" -E copy_if_different '{}' ${CMAKE_BINARY_DIR}/stage${STAGE}/'{}' '\;'
COMMAND cd "${CMAKE_BINARY_DIR}/stage${STAGE}" && LEAN_PATH=Init=Init $(MAKE) ./libleanstdlib.a
"LEAN=${PREV_LEAN}"
"LEANC=${LEAN_SOURCE_DIR}/../bin/leanc"
"LEAN_ROOT=${LEAN_SOURCE_DIR}"
"LEANC_OPTS=${LEANC_OPTS}"
"OUT=."
# recreate everything if the previous compiler has changed
"MORE_DEPS=${PREV_LEAN}"
)
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
# recreate everything if the previous compiler has changed
COMMAND bash -c "PATH=${PREV_STAGE_DIR}/bin:$$PATH $(MAKE) -f ${CMAKE_BINARY_DIR}/share/lean/Makefile OUT=${CMAKE_BINARY_DIR}/stage${STAGE}/lib MORE_DEPS=${PREV_STAGE_DIR}/bin/lean"
DEPENDS ${PREV_STAGE_TARGET})
add_library(leanstdlib_stage${STAGE} STATIC IMPORTED)
set_target_properties(leanstdlib_stage${STAGE} PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/libleanstdlib.a"
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/lib/libleanstdlib.a"
IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
add_dependencies(leanstdlib_stage${STAGE} make_stdlib_stage${STAGE})
add_executable(lean_stage${STAGE} EXCLUDE_FROM_ALL lean.cpp)
# see `target_link_libraries(lean ...)` below
target_link_libraries(lean_stage${STAGE} leanstatic leanstdlib_stage${STAGE} leanstatic leanstdlib_stage${STAGE})
set(PREV_LEAN "$<TARGET_FILE:lean_stage${STAGE}>")
set(PREV_STAGE_DIR "${CMAKE_BINARY_DIR}/stage${STAGE}")
set(PREV_STAGE_TARGET lean_stage${STAGE})
endforeach()
add_custom_target(check-stage3
COMMAND diff "$<TARGET_FILE:lean_stage2>" "$<TARGET_FILE:lean_stage3>")
add_custom_target(update-stage0
COMMAND make update-stage0
"OUT=${CMAKE_BINARY_DIR}/stage1"
"C_OUT=${LEAN_SOURCE_DIR}/stage1"
COMMAND make update-stage0 -f ${CMAKE_BINARY_DIR}/share/lean/Makefile
"OUT=${CMAKE_BINARY_DIR}/lib"
DEPENDS leanstdlib
WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}")
endif()
add_executable(lean lean.cpp)
if(STAGE0)
target_link_libraries(lean leanstatic)
else()
# `leanstatic` and `leanstdlib` are cyclically dependent static libraries.
# We use the approach described at
# https://cmake.org/cmake/help/v3.3/command/target_link_libraries.html#cyclic-dependencies-of-static-libraries
# We don't want to add leanstdlib as a direct dependency of leanstatic since this is only true for stage 1.
target_link_libraries(lean leanstatic leanstdlib leanstatic leanstdlib)
endif()
set_target_properties(lean PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
# `leanstatic` and `leanstdlib` are cyclically dependent static libraries.
# We use the approach described at
# https://cmake.org/cmake/help/v3.3/command/target_link_libraries.html#cyclic-dependencies-of-static-libraries
# We don't want to add leanstdlib as a direct dependency of leanstatic since this is only true for stage 1.
target_link_libraries(lean leanstatic leanstdlib leanstatic leanstdlib)
# create import library on Windows to link plugins against
set_target_properties(lean PROPERTIES ENABLE_EXPORTS ON)
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
@ -78,23 +59,22 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
endif()
install(TARGETS lean DESTINATION bin)
if(NOT STAGE0)
if(${EMSCRIPTEN})
if(NOT STAGE0 AND EMSCRIPTEN)
set(NODE_JS "node --stack_size=8192")
file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path
"#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/.. ${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n")
execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path)
file(WRITE $<TARGET_FILE:lean>_with_path
"#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/.. ${NODE_JS} $<TARGET_FILE:lean>.js \"$@\"\n")
execute_process(COMMAND chmod +x $<TARGET_FILE:lean>_with_path)
ADD_CUSTOM_TARGET(bin_lean ALL
COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/lean_with_path" "${LEAN_SOURCE_DIR}/../bin/lean"
COMMAND "${CMAKE_COMMAND}" -E make_directory "${CMAKE_BINARY_DIR}/bin"
COMMAND "${CMAKE_COMMAND}" -E copy "$<TARGET_FILE:lean>_with_path" "${CMAKE_BINARY_DIR}/bin/lean"
DEPENDS lean
)
file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/lean
"#!/bin/sh\n${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n")
execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/lean)
file(WRITE $<TARGET_FILE:lean>
"#!/bin/sh\n${NODE_JS} $<TARGET_FILE:lean>.js \"$@\"\n")
execute_process(COMMAND chmod +x $<TARGET_FILE:lean>)
# legacy code for mkleanbook
# copy olean files from the library into build/emscripten/shell/library/...
@ -111,41 +91,24 @@ if(NOT STAGE0)
-s \"BINARYEN_METHOD='native-wasm,asmjs'\"")
add_dependencies(lean_js lean_js_library)
set_target_properties(lean_js PROPERTIES COMPILE_FLAGS --bind -s NO_EXIT_RUNTIME=1)
else()
if (MSVC)
ADD_CUSTOM_TARGET(bin_lean ALL
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_FILE_DIR:lean>/mpir.dll" "${LEAN_SOURCE_DIR}/../bin/"
DEPENDS bin_lean_stage0
)
else()
ADD_CUSTOM_TARGET(bin_lean ALL
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_LINKER_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
DEPENDS bin_lean_stage0
)
ADD_CUSTOM_TARGET(bin_lean_stage2
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean_stage2>" "${LEAN_SOURCE_DIR}/../bin/"
)
endif()
endif()
endif()
# add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
# add_test(lean_export ${CMAKE_CURRENT_BINARY_DIR}/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")
add_test(lean_help1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --help)
add_test(lean_help2 "${CMAKE_CURRENT_BINARY_DIR}/lean" -h)
add_test(lean_version1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --version)
# 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")
add_test(lean_help1 "${CMAKE_BINARY_DIR}/bin/lean" --help)
add_test(lean_help2 "${CMAKE_BINARY_DIR}/bin/lean" -h)
add_test(lean_version1 "${CMAKE_BINARY_DIR}/bin/lean" --version)
if (NOT ${EMSCRIPTEN})
add_test(lean_version2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --v)
add_test(lean_version2 "${CMAKE_BINARY_DIR}/bin/lean" --v)
endif()
add_test(lean_ghash1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -g)
add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
# add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
add_test(lean_ghash1 "${CMAKE_BINARY_DIR}/bin/lean" -g)
add_test(lean_ghash2 "${CMAKE_BINARY_DIR}/bin/lean" --githash)
# add_test(lean_new_frontend "${CMAKE_BINARY_DIR}/bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z")
add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean")
# 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 "${LEAN_SOURCE_DIR}/../bin")
string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
# LEAN TESTS
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")

91
stage0/src/CMakeLists.txt
View file

@ -459,8 +459,8 @@ if(USE_GITHASH)
get_git_head_revision(GIT_REFSPEC GIT_SHA1)
if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
message(STATUS "Failed to read git_sha1")
if(EXISTS "${LEAN_SOURCE_DIR}/../bin/package_version")
file(STRINGS "${LEAN_SOURCE_DIR}/../bin/package_version" LEAN_PACKAGE_VERSION)
if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
endif()
else()
@ -468,8 +468,8 @@ if(USE_GITHASH)
endif()
else()
set(GIT_SHA1 "GITDIR-NOTFOUND")
if(EXISTS "${LEAN_SOURCE_DIR}/../bin/package_version")
file(STRINGS "${LEAN_SOURCE_DIR}/../bin/package_version" LEAN_PACKAGE_VERSION)
if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
endif()
endif()
@ -483,14 +483,9 @@ endif ()
# Version
configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/version.h")
# Remark: we did not put `config.h` in `${LEAN_BINARY_DIR}` because `leanc` depends on this file.
# Note that, `leanc` already had problems with multiple configurations before we added `config.h`.
# For example, it uses binary files located in the `bin` directory.
configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_SOURCE_DIR}/config.h")
install(FILES "${LEAN_SOURCE_DIR}/config.h" DESTINATION "${INCLUDE_DIR}")
if(NOT STAGE0)
configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_SOURCE_DIR}/Makefile")
endif()
configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/config.h")
install(FILES "${LEAN_SOURCE_DIR}/include/config.h" DESTINATION "${INCLUDE_DIR}")
configure_file("${LEAN_SOURCE_DIR}/Makefile.in" "${LEAN_BINARY_DIR}/share/lean/Makefile")
include_directories("${LEAN_BINARY_DIR}")
add_subdirectory(runtime)
@ -515,7 +510,6 @@ add_subdirectory(initialize)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
if(STAGE0)
add_subdirectory(../stdlib stdlib)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:stage0>)
endif()
if(EMSCRIPTEN)
set(LEAN_LIBRARY_TYPE SHARED)
@ -534,7 +528,7 @@ if(NOT STAGE0)
-DCHECK_OLEAN_VERSION=${CHECK_OLEAN_VERSION}
"-DCMAKE_C_COMPILER=${CMAKE_C_COMPILER}"
"-DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}"
BUILD_COMMAND $(MAKE) lean # build executable only
BUILD_COMMAND $(MAKE) # build executable only
BUILD_ALWAYS ON # cmake doesn't auto-detect changes without a download method
INSTALL_COMMAND "" # skip install
)
@ -542,42 +536,36 @@ endif()
add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
target_link_libraries(leanstatic ${EXTRA_LIBS})
set_target_properties(leanstatic PROPERTIES ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib")
if(LLVM)
target_link_libraries(leanstatic ${llvm_libs})
endif()
if(NOT STAGE0)
if(STAGE0)
add_library(leanstdlib STATIC $<TARGET_OBJECTS:stage0>)
else()
add_library(leanstdlib STATIC IMPORTED)
ADD_CUSTOM_TARGET(bin_lib ALL
COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "$<TARGET_FILE:leanstdlib>" "$<TARGET_FILE:leanstatic>" "${LEAN_SOURCE_DIR}/../bin"
)
# Configure leanc
configure_file("${LEAN_SOURCE_DIR}/../bin/leanc.in" "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc")
file(COPY "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc"
DESTINATION "${LEAN_SOURCE_DIR}/../bin"
FILE_PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
install(FILES "${LEAN_SOURCE_DIR}/../bin/leanc"
DESTINATION bin
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
add_custom_target(bin ALL)
add_dependencies(bin bin_lib bin_lean)
endif()
# The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).
# For some strange reason, it contains a copy of pthread_equal.
# Remark: this problem does not happen when we generate the DLL using msys2 on Windows.
if (NOT("${CROSS_COMPILE}" MATCHES "ON"))
if ("${STATIC}" MATCHES "OFF")
add_library(leanshared SHARED shared/init.cpp)
# see `target_link_libraries(lean ...)`
target_link_libraries(leanshared leanstatic leanstdlib leanstatic leanstdlib)
install(TARGETS leanshared DESTINATION lib)
endif()
install(TARGETS leanstatic DESTINATION lib)
endif()
configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc")
install(FILES "${CMAKE_BINARY_DIR}/bin/leanc"
DESTINATION bin
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
# shared library deactivated until we figure out the leanstatic/leanstdlib story
# # The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).
# # For some strange reason, it contains a copy of pthread_equal.
# # Remark: this problem does not happen when we generate the DLL using msys2 on Windows.
# if (NOT("${CROSS_COMPILE}" MATCHES "ON"))
# if ("${STATIC}" MATCHES "OFF")
# add_library(leanshared SHARED shared/init.cpp)
# # see `target_link_libraries(lean ...)`
# target_link_libraries(leanshared leanstatic leanstdlib leanstatic leanstdlib)
# install(TARGETS leanshared DESTINATION lib)
# endif()
# install(TARGETS leanstatic DESTINATION lib)
# endif()
add_subdirectory(shell)
@ -618,24 +606,23 @@ add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cma
endif()
add_custom_target(clean-stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
COMMAND find . -name '*.olean' -delete
COMMAND find . -name '*.depend' -delete
COMMAND rm -rf ../stage1 "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true
)
COMMAND rm -rf "${CMAKE_BINARY_DIR}/lib" "${CMAKE_BINARY_DIR}/stage2" "${CMAKE_BINARY_DIR}/stage3" || true)
add_custom_target(clean-olean
DEPENDS clean-stdlib)
install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}"
install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}/lean"
FILES_MATCHING
PATTERN "*.olean")
install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION "${LIBRARY_DIR}/lean/src"
FILES_MATCHING
PATTERN "*.lean"
PATTERN "*.olean"
PATTERN "*.md")
install(DIRECTORY "${CMAKE_SOURCE_DIR}/runtime" DESTINATION "${INCLUDE_DIR}"
FILES_MATCHING
PATTERN "*.h")
add_custom_target(include_runtime ALL
COMMAND cmake -E copy_directory "${CMAKE_SOURCE_DIR}/runtime" "${CMAKE_BINARY_DIR}/include/runtime")
install(FILES "${CMAKE_SOURCE_DIR}/runtime/lean.h" DESTINATION "${INCLUDE_DIR}/runtime")
if("${INCLUDE_MSYS2_DLLS}" MATCHES "ON")
# TODO(Leo): do not use hardlinks to required DLLs.

323
stage0/src/bin/lean-gdb.py Normal file
View file

@ -0,0 +1,323 @@
# -*- coding: utf-8 -*-
#
# Copyright (c) 2016 Microsoft Corporation. All rights reserved.
# Released under Apache 2.0 license as described in the file LICENSE.
#
# Authors: Sebastian Ullrich, Gabriel Ebner
#
import gdb
import gdb.printing
def is_scalar(o):
return o.cast(gdb.lookup_type('uintptr_t')) & 1 == 1
def box(n):
return gdb.Value(n << 1 | 1).cast(gdb.lookup_type('lean_object').pointer())
def unbox(o):
return o.cast(gdb.lookup_type('uintptr_t')) >> 1
def to_cnstr(o):
return o.cast(gdb.lookup_type('lean_ctor_object').pointer())
def get_tag(header):
return header >> (32 + 8 + 8 + 8)
def get_cnstr_tag(o):
return get_tag(int(o.cast(gdb.lookup_type('lean_ctor_object').pointer()).dereference()['m_header']['m_header']))
def get_num_objs(header):
return (header >> (32 + 8 + 8)) & 0xFF
def get_mem_kind(header):
return (header >> (32 + 8)) & 0xFF
def get_rc(header):
return header & 0xFFFFFFFF
char_p = gdb.lookup_type('char').pointer()
def get_cnstr_obj_arg(o, i):
return o.cast(gdb.lookup_type('lean_ctor_object').pointer()).dereference()['m_objs'][i]
def get_closure_arg(o, i):
return o.cast(gdb.lookup_type('lean_closure_object').pointer()).dereference()['m_objs'][i]
def get_c_str(o):
return o.cast(gdb.lookup_type('lean_string_object').pointer()).dereference()['m_data'].reference_value().cast(char_p)
class LeanObjectPrinter:
"""Print a lean_object object."""
kinds = [
# 244, ...
('ctor', []),
('closure', ['m_arity', 'm_fun', 'm_num_fixed']),
('array', ['m_size', 'm_capacity']),
('sarray', ['m_size', 'm_capacity']),
('sarray', ['m_size', 'm_capacity']),
('string', ['m_size', 'm_capacity', 'm_length']),
('mpz', ['m_value']),
('thunk', ['m_value', 'm_closure']),
('task', ['m_value', 'm_imp']),
('ref', ['m_value']),
('external', ['m_class', 'm_data']),
]
lean_max_ctor_tag = 244
def __init__(self, val):
self.val = val.address
if not is_scalar(self.val):
self.header = int(self.val.dereference()['m_header'])
self.kind = max(0, get_tag(self.header) - LeanObjectPrinter.lean_max_ctor_tag)
def to_string(self):
if is_scalar(self.val):
return unbox(self.val)
else:
k = get_mem_kind(self.header)
return "{} ({})".format(LeanObjectPrinter.kinds[self.kind][0],
get_rc(self.header) if k == 0 else
get_rc(self.header) + "/MT" if k == 1 else
"PERSIST")
def children(self):
if is_scalar(self.val):
return
if self.kind >= len(LeanObjectPrinter.kinds):
return
typ, fields = LeanObjectPrinter.kinds[self.kind]
val = self.val.cast(gdb.lookup_type("lean_" + typ + "_object").pointer()).dereference()
for f in fields:
yield (f, val[f])
if typ == 'ctor':
for i in range(get_num_objs(self.header)):
yield ('', val['m_objs'][i].cast(gdb.lookup_type('lean_object').pointer()))
elif typ == 'array':
for i in range(val['m_size']):
yield ('', val['m_data'][i].cast(gdb.lookup_type('lean_object').pointer()))
elif typ == 'closure':
for i in range(val['m_num_fixed']):
yield ('', val['m_objs'][i].cast(gdb.lookup_type('lean_object').pointer()))
elif typ == 'string':
yield ('', val['m_data'].reference_value().cast(char_p))
class LeanOptionalPrinter:
"""Print a lean::optional object."""
def __init__(self, val):
self.val = val
def get_val(self):
if hasattr(self.val, 'm_some'):
if not self.val['m_some']:
return None
elif not self.val['m_value'].cast(gdb.lookup_type('char').pointer()):
return None
return self.val['m_value']
def children(self):
val = self.get_val()
return [('', val)] if val else []
def to_string(self):
return str(self.val.type)
class LeanNamePrinter:
"""Print a lean::name object."""
def __init__(self, val):
self.val = val
def to_string(self):
def rec(o):
prefix = get_cnstr_obj_arg(o, 0)
part = get_cnstr_obj_arg(o, 1)
s = ("'%s'" % get_c_str(part).string()) if get_cnstr_tag(o) == 1 else str(unbox(part))
if not is_scalar(prefix):
return "%s.%s" % (rec(prefix), s)
else:
return s
if is_scalar(self.val['m_obj']):
return ""
else:
return rec(self.val['m_obj'])
class LeanExprPrinter:
"""Print a lean::expr object."""
expr_kinds = [
('bvar', [('idx', 'nat')]),
('fvar', ['name']),
('mvar', ['name', ('type', 'expr')]),
('sort', ['level']),
('const', ['name', ('levels', 'list_ref<lean::level>')]),
('app', [('fn', 'expr'), ('arg', 'expr')]),
('lam', ['name', ('type', 'expr'), ('body', 'expr')]),
('pi', ['name', ('type', 'expr'), ('body', 'expr')]),
('let', ['name', ('type', 'expr'), ('val', 'expr'), ('body', 'expr')]),
('lit', ['literal']),
('mdata', ['kvmap', 'expr']),
('proj', ['name', 'nat', 'expr']),
('elet', ['name', 'name', 'expr']),
]
def __init__(self, val):
self.val = val
def to_string(self):
return 'lean::expr[{}]'.format(LeanExprPrinter.expr_kinds[get_cnstr_tag(self.val['m_obj'])][0])
def children(self):
_, fields = LeanExprPrinter.expr_kinds[get_cnstr_tag(self.val['m_obj'])]
for i, f in enumerate(fields):
if isinstance(f, tuple):
name, typ = f
else:
name, typ = f, f
yield (name, get_cnstr_obj_arg(self.val['m_obj'], i).cast(gdb.lookup_type('lean::' + typ)))
class LeanLevelPrinter:
"""Print a lean::level object."""
level_kinds = [
('lean::level_cell', 'zero', []),
('lean::level_succ', 'succ', ['m_l']),
('lean::level_max_core', 'max', ['m_lhs', 'm_rhs']),
('lean::level_max_core', 'imax', ['m_lhs', 'm_rhs']),
('lean::level_param_core', 'param', ['m_id']),
('lean::level_param_core', 'meta', ['m_id']),
]
def __init__(self, val):
self.val = val
def to_string(self):
kind = int(self.val['m_obj']['m_kind'])
(subtype, name, fields) = LeanLevelPrinter.level_kinds[kind]
subtype = gdb.lookup_type(subtype)
val = self.val['m_obj'].cast(subtype.pointer()).dereference()
return "({})".format(" ".join([name] + [str(val[field]) for field in fields]))
class LeanListPrinter:
"""Print a lean::list object."""
def __init__(self, val):
self.val = val
def children(self):
l = self.val
i = 0
while l['m_obj']:
cell = l['m_obj'].dereference()
yield ('[%s]' % i, cell['m_head'])
l = cell['m_tail']
i += 1
def to_string(self):
return str(self.val.type)
def display_hint(self):
return 'array'
class LeanBufferPrinter:
"""Print a lean::buffer object."""
def __init__(self, val):
self.val = val
def children(self):
p = self.val['m_buffer']
for i in range(int(self.val['m_pos'])):
yield ('[%s]' % i, p.dereference())
p += 1
def to_string(self):
return str(self.val.type)
def display_hint(self):
return 'array'
class LeanListRefPrinter:
"""Print a lean::list_ref object."""
def __init__(self, val):
self.val = val
def children(self):
l = self.val['m_obj']
i = 0
while not is_scalar(l):
yield ('[%s]' % i, get_cnstr_obj_arg(l, 0).cast(self.val.type.template_argument(0)))
l = get_cnstr_obj_arg(l, 1)
i += 1
def to_string(self):
return str(self.val.type)
def display_hint(self):
return 'array'
class LeanRBTreePrinter:
"""Print a lean::rb_tree object."""
def __init__(self, val):
self.val = val
def children(self):
def rec(node):
if node['m_ptr']:
cell = node['m_ptr'].dereference()
for i in rec(cell['m_left']): yield i
yield ('', cell['m_value'])
for i in rec(cell['m_right']): yield i
return rec(self.val['m_root'])
def to_string(self):
return 'lean::rb_tree' # full type is way too verbose
def display_hint(self):
return 'array'
class LeanRBMapPrinter:
"""Print a lean::rb_map object."""
def __init__(self, val):
self.val = val
def children(self):
for (_, child) in LeanRBTreePrinter(self.val['m_map']).children():
yield ('', child['first'])
yield ('', child['second'])
def to_string(self):
return 'lean::rb_map' # full type is way too verbose
def display_hint(self):
return 'map'
def build_pretty_printer():
pp = gdb.printing.RegexpCollectionPrettyPrinter("lean")
pp.add_printer('object', '^lean(_|::)object$', LeanObjectPrinter)
pp.add_printer('optional', '^lean::optional', LeanOptionalPrinter)
pp.add_printer('name', '^lean::name$', LeanNamePrinter)
pp.add_printer('expr', '^lean::expr$', LeanExprPrinter)
#pp.add_printer('level', '^lean::level$', LeanLevelPrinter)
#pp.add_printer('list', '^lean::list', LeanListPrinter)
pp.add_printer('buffer', '^lean::buffer', LeanBufferPrinter)
pp.add_printer('list_ref', '^lean::list_ref', LeanListRefPrinter)
pp.add_printer('rb_tree', '^lean::rb_tree', LeanRBTreePrinter)
pp.add_printer('rb_map', '^lean::rb_map', LeanRBMapPrinter)
return pp
def register():
gdb.printing.register_pretty_printer(
gdb.current_objfile(),
build_pretty_printer(),
replace=True)
register()

29
stage0/src/bin/leanc.in Executable file
View file

@ -0,0 +1,29 @@
#!/usr/bin/env bash
# Lean compiler
#
# A simple wrapper around a C compiler. Defaults to the compiler Lean was built with,
# which can be overridden with the environment variable `LEAN_CC`. All parameters are passed
# as-is to the wrapped compiler.
#
# Interesting options:
# * `-U LEAN_MULTI_THREAD` can be used to optimize programs not making use of multi-threading
set -e
bindir=$(dirname $0)
# link to C++ part of Lean, Lean part of Lean, C++ stdlib, C math library (`sin` etc.)
# NOTE: leanstatic and leanstdlib are cyclically dependent
linker_flags="-lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lstdc++ -lm"
for arg in "$@"; do
[[ $arg == "-shared" ]] && linker_flags="$linker_flags @LEANC_SHARED_LINKER_FLAGS@"
done
# Check C compiler
for cc in $LEAN_CC @CMAKE_C_COMPILER@ /usr/bin/gcc; do
if [ -f $cc ] || command -v $cc; then
export LEAN_CC=$cc && break
fi
done
[ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!"
@CMAKE_C_COMPILER_LAUNCHER@ $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument

6
stage0/src/runtime/CMakeLists.txt
View file

@ -4,9 +4,3 @@ serializer.cpp stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp)
add_library(runtime OBJECT ${RUNTIME_OBJS})
add_library(leanruntime ${RUNTIME_OBJS})
ADD_CUSTOM_TARGET(bin_runtime ALL
COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/libleanruntime.a" "${LEAN_SOURCE_DIR}/../bin"
DEPENDS leanruntime
)

133
stage0/src/shell/CMakeLists.txt
View file

@ -1,75 +1,54 @@
if(NOT STAGE0)
add_executable(lean_stage0 IMPORTED)
set_target_properties(lean_stage0 PROPERTIES IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage0/shell/lean${CMAKE_EXECUTABLE_SUFFIX}")
ADD_CUSTOM_TARGET(bin_lean_stage0
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean_stage0>" "${LEAN_SOURCE_DIR}/../bin/lean_stage0${CMAKE_EXECUTABLE_SUFFIX}"
DEPENDS stage0
)
string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
add_custom_target(make_stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}"
COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=Init=Init" $(MAKE) "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
"LEAN=$<TARGET_FILE:lean_stage0>"
"LEANC_OPTS=${LEANC_OPTS}"
"OUT=${CMAKE_BINARY_DIR}/stage1"
# share .c files between different build configurations
"C_OUT=${LEAN_SOURCE_DIR}/stage1"
COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/stage0/bin:$$PATH $(MAKE) -f ${CMAKE_BINARY_DIR}/share/lean/Makefile OUT=${CMAKE_BINARY_DIR}/lib"
DEPENDS stage0)
set_target_properties(leanstdlib PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/libleanstdlib.a"
IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
add_dependencies(leanstdlib make_stdlib)
install(FILES "$<TARGET_FILE:leanstdlib>" DESTINATION lib)
set(PREV_LEAN "$<TARGET_FILE:lean>")
set(PREV_STAGE_DIR "${CMAKE_BINARY_DIR}")
foreach(STAGE RANGE 2 3)
add_custom_target(make_stdlib_stage${STAGE}
COMMAND cd "${LEAN_SOURCE_DIR}" && find . '\(' -name Makefile -o -name relative.py -o -name '*.lean' '\)' -exec "${CMAKE_COMMAND}" -E copy_if_different '{}' ${CMAKE_BINARY_DIR}/stage${STAGE}/'{}' '\;'
COMMAND cd "${CMAKE_BINARY_DIR}/stage${STAGE}" && LEAN_PATH=Init=Init $(MAKE) ./libleanstdlib.a
"LEAN=${PREV_LEAN}"
"LEANC=${LEAN_SOURCE_DIR}/../bin/leanc"
"LEAN_ROOT=${LEAN_SOURCE_DIR}"
"LEANC_OPTS=${LEANC_OPTS}"
"OUT=."
# recreate everything if the previous compiler has changed
"MORE_DEPS=${PREV_LEAN}"
)
# recreate everything if the previous compiler has changed
COMMAND bash -c "PATH=${PREV_STAGE}/bin:$$PATH $(MAKE) -f ${CMAKE_BINARY_DIR}/share/lean/Makefile OUT=${CMAKE_BINARY_DIR}/stage${STAGE}/lib MORE_DEPS=${PREV_STAGE}/bin/lean"
DEPENDS lean_stage${PREV_STAGE})
add_library(leanstdlib_stage${STAGE} STATIC IMPORTED)
set_target_properties(leanstdlib_stage${STAGE} PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/libleanstdlib.a"
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage${STAGE}/lib/libleanstdlib.a"
IMPORTED_LINK_INTERFACE_LIBRARIES leanstatic)
add_dependencies(leanstdlib_stage${STAGE} make_stdlib_stage${STAGE})
add_executable(lean_stage${STAGE} EXCLUDE_FROM_ALL lean.cpp)
# see `target_link_libraries(lean ...)` below
target_link_libraries(lean_stage${STAGE} leanstatic leanstdlib_stage${STAGE} leanstatic leanstdlib_stage${STAGE})
set(PREV_LEAN "$<TARGET_FILE:lean_stage${STAGE}>")
set(PREV_STAGE ${STAGE})
set(PREV_STAGE_DIR "${CMAKE_BINARY_DIR}/stage${STAGE}")
endforeach()
add_custom_target(check-stage3
COMMAND diff "$<TARGET_FILE:lean_stage2>" "$<TARGET_FILE:lean_stage3>")
add_custom_target(update-stage0
COMMAND make update-stage0
"OUT=${CMAKE_BINARY_DIR}/stage1"
"C_OUT=${LEAN_SOURCE_DIR}/stage1"
COMMAND make update-stage0 -f ${CMAKE_BINARY_DIR}/share/lean/Makefile
"OUT=${CMAKE_BINARY_DIR}/lib"
DEPENDS leanstdlib
WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}")
endif()
add_executable(lean lean.cpp)
if(STAGE0)
target_link_libraries(lean leanstatic)
else()
# `leanstatic` and `leanstdlib` are cyclically dependent static libraries.
# We use the approach described at
# https://cmake.org/cmake/help/v3.3/command/target_link_libraries.html#cyclic-dependencies-of-static-libraries
# We don't want to add leanstdlib as a direct dependency of leanstatic since this is only true for stage 1.
target_link_libraries(lean leanstatic leanstdlib leanstatic leanstdlib)
endif()
set_target_properties(lean PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
# `leanstatic` and `leanstdlib` are cyclically dependent static libraries.
# We use the approach described at
# https://cmake.org/cmake/help/v3.3/command/target_link_libraries.html#cyclic-dependencies-of-static-libraries
# We don't want to add leanstdlib as a direct dependency of leanstatic since this is only true for stage 1.
target_link_libraries(lean leanstatic leanstdlib leanstatic leanstdlib)
# create import library on Windows to link plugins against
set_target_properties(lean PROPERTIES ENABLE_EXPORTS ON)
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
@ -78,23 +57,22 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
endif()
install(TARGETS lean DESTINATION bin)
if(NOT STAGE0)
if(${EMSCRIPTEN})
if(NOT STAGE0 AND EMSCRIPTEN)
set(NODE_JS "node --stack_size=8192")
file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path
"#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/.. ${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n")
execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/lean_with_path)
file(WRITE $<TARGET_FILE:lean>_with_path
"#!/bin/sh\nLEAN_PATH=Init=${CMAKE_CURRENT_SOURCE_DIR}/.. ${NODE_JS} $<TARGET_FILE:lean>.js \"$@\"\n")
execute_process(COMMAND chmod +x $<TARGET_FILE:lean>_with_path)
ADD_CUSTOM_TARGET(bin_lean ALL
COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/lean_with_path" "${LEAN_SOURCE_DIR}/../bin/lean"
COMMAND "${CMAKE_COMMAND}" -E make_directory "${CMAKE_BINARY_DIR}/bin"
COMMAND "${CMAKE_COMMAND}" -E copy "$<TARGET_FILE:lean>_with_path" "${CMAKE_BINARY_DIR}/bin/lean"
DEPENDS lean
)
file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/lean
"#!/bin/sh\n${NODE_JS} ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n")
execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/lean)
file(WRITE $<TARGET_FILE:lean>
"#!/bin/sh\n${NODE_JS} $<TARGET_FILE:lean>.js \"$@\"\n")
execute_process(COMMAND chmod +x $<TARGET_FILE:lean>)
# legacy code for mkleanbook
# copy olean files from the library into build/emscripten/shell/library/...
@ -111,38 +89,21 @@ if(NOT STAGE0)
-s \"BINARYEN_METHOD='native-wasm,asmjs'\"")
add_dependencies(lean_js lean_js_library)
set_target_properties(lean_js PROPERTIES COMPILE_FLAGS --bind -s NO_EXIT_RUNTIME=1)
else()
if (MSVC)
ADD_CUSTOM_TARGET(bin_lean ALL
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_FILE_DIR:lean>/mpir.dll" "${LEAN_SOURCE_DIR}/../bin/"
DEPENDS bin_lean_stage0
)
else()
ADD_CUSTOM_TARGET(bin_lean ALL
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_LINKER_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
DEPENDS bin_lean_stage0
)
ADD_CUSTOM_TARGET(bin_lean_stage2
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean_stage2>" "${LEAN_SOURCE_DIR}/../bin/"
)
endif()
endif()
endif()
# add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean")
# add_test(lean_export ${CMAKE_CURRENT_BINARY_DIR}/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean")
add_test(lean_help1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --help)
add_test(lean_help2 "${CMAKE_CURRENT_BINARY_DIR}/lean" -h)
add_test(lean_version1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --version)
# 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")
add_test(lean_help1 "${CMAKE_BINARY_DIR}/bin/lean" --help)
add_test(lean_help2 "${CMAKE_BINARY_DIR}/bin/lean" -h)
add_test(lean_version1 "${CMAKE_BINARY_DIR}/bin/lean" --version)
if (NOT ${EMSCRIPTEN})
add_test(lean_version2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --v)
add_test(lean_version2 "${CMAKE_BINARY_DIR}/bin/lean" --v)
endif()
add_test(lean_ghash1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -g)
add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
# add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
add_test(lean_ghash1 "${CMAKE_BINARY_DIR}/bin/lean" -g)
add_test(lean_ghash2 "${CMAKE_BINARY_DIR}/bin/lean" --githash)
# add_test(lean_new_frontend "${CMAKE_BINARY_DIR}/bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z")
add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean")
# LEAN TESTS
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
@ -151,7 +112,7 @@ FOREACH(T ${LEANTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leantest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
endif()
ENDFOREACH(T)
@ -162,7 +123,7 @@ FOREACH(T ${LEANRUNTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanruntest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
endif()
ENDFOREACH(T)
@ -173,7 +134,7 @@ FOREACH(T ${LEANNEWFRONTENDTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leannewfrontendtest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/newfrontend"
COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
endif()
ENDFOREACH(T)
@ -183,7 +144,7 @@ FOREACH(T ${LEANCOMPTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leancomptest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
ENDFOREACH(T)
# LEAN INTERPRETER TESTS
@ -193,7 +154,7 @@ FOREACH(T ${LEANINTERPTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leaninterptest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single_interpret.sh ${T_NAME}")
COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single_interpret.sh ${T_NAME}")
endif()
ENDFOREACH(T)
@ -205,7 +166,7 @@ FOREACH(T_OUT ${LEANBENCHTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanbenchtest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench"
COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
ENDFOREACH(T_OUT)
# LEAN PLUGIN TESTS
@ -214,7 +175,7 @@ FOREACH(T ${LEANINTERPTESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanplugintest_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin"
COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
ENDFOREACH(T)
# LEAN TESTS using --trust=0
@ -223,5 +184,5 @@ FOREACH(T ${LEANT0TESTS})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leant0test_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0"
COMMAND bash -c "PATH=${LEAN_SOURCE_DIR}/../bin:$PATH ./test_single.sh ${T_NAME}")
COMMAND bash -c "PATH=${CMAKE_BINARY_DIR}/bin:$PATH ./test_single.sh ${T_NAME}")
ENDFOREACH(T)

1
tests/.gitignore vendored Normal file
View file

@ -0,0 +1 @@
*.olean

3
tests/lean/ctor_layout.lean
View file

@ -3,8 +3,7 @@ open Lean
open Lean.IR
def tst : IO Unit :=
do initSearchPath "Init=../../src/Init";
env ← importModules [{module := `Init.Lean.Compiler.IR.Basic}];
do env ← importModules [{module := `Init.Lean.Compiler.IR.Basic}];
ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse;
ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
IO.println "---";