From e6927253cf7c719940b1847851d40eb3be640632 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 24 Sep 2021 16:17:52 +0200 Subject: [PATCH] feat: use `leanc` written in Lean for testing & distribution building is still handled by a (minimal) Bash script for bootstrapping purposes --- nix/bootstrap.nix | 19 +++++++++-------- src/CMakeLists.txt | 12 ++++++++++- src/Leanc.lean | 50 +++++++++++++++++++++++++++++++++++++++++++++ src/bin/leanc.in | 51 +++------------------------------------------- src/stdlib.make.in | 10 ++++++--- 5 files changed, 82 insertions(+), 60 deletions(-) create mode 100644 src/Leanc.lean diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 77ed9cb57c..6ed9707bb6 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -20,15 +20,19 @@ rec { }); lean-bin-tools-unwrapped = buildCMake { name = "lean-bin-tools"; - realSrc = lib.sourceByRegex ../src [ "CMakeLists\.txt" "bin.*" "include.*" ".*\.in" ]; + outputs = [ "out" "leanc_src" ]; + realSrc = lib.sourceByRegex ../src [ "CMakeLists\.txt" "bin.*" "include.*" ".*\.in" "Leanc\.lean" ]; preConfigure = '' touch empty.cpp sed -i 's/find_package.*//;s/add_subdirectory.*//;s/set(LEAN_OBJS.*/set(LEAN_OBJS empty.cpp)/' CMakeLists.txt ''; dontBuild = true; installPhase = '' - mkdir $out + mkdir $out $leanc_src mv bin/ include/ share/ $out/ + mv leanc.sh $out/bin/leanc + mv leanc/Leanc.lean $leanc_src/ + substituteInPlace $out/bin/leanc --replace '$root' "$out" substituteInPlace $out/bin/leanmake --replace "make" "${gnumake}/bin/make" substituteInPlace $out/share/lean/lean.mk --replace "/usr/bin/env bash" "${bash}/bin/bash" ''; @@ -90,6 +94,7 @@ rec { stdlib = [ Init Std Lean ]; Leanpkg = build { name = "Leanpkg"; deps = stdlib; linkFlags = ["-L${gmp}/lib -L${leanshared}"]; }; extlib = stdlib ++ [ Leanpkg ]; + Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; linkFlags = ["-L${gmp}/lib -L${leanshared}"]; }; stdlibLinkFlags = "-L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean"; leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; } '' mkdir $out @@ -100,7 +105,7 @@ rec { ''; mods = Init.mods // Std.mods // Lean.mods; leanc = writeShellScriptBin "leanc" '' - LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc ${stdlibLinkFlags} -L${leanshared} "$@" + LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable.withSharedStdlib}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${leanshared} "$@" ''; lean = runCommand "lean" {} '' mkdir -p $out/bin @@ -114,11 +119,9 @@ rec { mkdir -p $out/bin $out/lib/lean ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList extlib)} $out/lib/lean/ # put everything in a single final derivation so `IO.appDir` references work - cp ${lean}/bin/lean ${leanpkg}/bin/leanpkg $out/bin - # NOTE: first `bin/leanc` wins in case of `lndir` - for i in ${leanc} ${lean-bin-tools-unwrapped}; do - ${lndir}/bin/lndir -silent $i $out - done + cp ${lean}/bin/lean ${leanpkg}/bin/leanpkg ${leanc}/bin/leanc $out/bin + # NOTE: `lndir` will not override existing `bin/leanc` + ${lndir}/bin/lndir -silent ${lean-bin-tools-unwrapped} $out ''; }); test = buildCMake { diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d6ef685bd8..65cfaf77f5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -475,7 +475,17 @@ if(PREV_STAGE) WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..") endif() -configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc" @ONLY) +# use Bash version for building, use Lean version in bin/ for tests & distribution +configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/leanc.sh" @ONLY) +if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean) + configure_file("${LEAN_SOURCE_DIR}/Leanc.lean" "${CMAKE_BINARY_DIR}/leanc/Leanc.lean" @ONLY) + add_custom_target(leanc ALL + WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc + DEPENDS leanshared + COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Leanc + VERBATIM) +endif() + file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin) install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin) diff --git a/src/Leanc.lean b/src/Leanc.lean new file mode 100644 index 0000000000..9f77933528 --- /dev/null +++ b/src/Leanc.lean @@ -0,0 +1,50 @@ +def main (args : List String) : IO UInt32 := do + if args.isEmpty then + IO.println "Lean C compiler + +A simple wrapper around a C compiler. Defaults to `@LEANC_CC@`, +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 +* `--print-cflags`: print C compiler flags necessary for building against the Lean runtime and exit +* `--print-ldlags`: print C compiler flags necessary for statically linking against the Lean library and exit +* Set the `LEANC_GMP` environment variable to a path to `libgmp.a` (or `-l:libgmp.a` on Linux) to link GMP statically. +Beware of the licensing consequences since GMP is LGPL." + return 1 + + let binDir ← IO.appDir + -- Zig gets confused by relative include paths on Windows + let binDir ← IO.FS.realPath binDir + let root := binDir.parent.get! + -- We assume that the CMake variables do not contain escaped spaces + let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn + let mut ldflags := ["-L", (root / "lib").toString, "-L", (root / "lib" / "lean").toString, (← IO.getEnv "LEANC_GMP").getD "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn + let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn + + for arg in args do + match arg with + | "-shared" => + -- switch to shared linker flags + ldflagsExt := "@LEANC_SHARED_LINKER_FLAGS@".trim.splitOn + | "-c" => + ldflags := [] + ldflagsExt := [] + | "--print-cflags" => + IO.println <| " ".intercalate cflags + return 0 + | "--print-ldflags" => + IO.println <| " ".intercalate (cflags ++ ldflagsExt ++ ldflags) + return 0 + | _ => () + + let mut cc := (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@" + if cc.startsWith "." then + cc := (binDir / cc).toString + + let args := cflags ++ args ++ ldflagsExt ++ ldflags ++ ["-Wno-unused-command-line-argument"] + if args.contains "-v" then + IO.eprintln s!"{cc} {" ".intercalate args}" + let child ← IO.Process.spawn { cmd := cc, args := args.toArray } + child.wait diff --git a/src/bin/leanc.in b/src/bin/leanc.in index 66b3f3e0fb..2ea0aaf2ab 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -1,49 +1,4 @@ #!/usr/bin/env bash -# Lean compiler -# -# A simple wrapper around a C compiler. Defaults to `@LEANC_CC@`, -# 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 -# * `--print-cflags`: print C compiler flags necessary for building against the Lean runtime and exit -# * `--print-ldlags`: print C compiler flags necessary for statically linking against the Lean library and exit -# * Set the `LEANC_GMP` environment variable to a path to `libgmp.a` (or `-l:libgmp.a` on Linux) to link GMP statically. -# Beware of the licensing consequences since GMP is LGPL. - -set -e -bindir=$(dirname $0) - -cflags=("-I$bindir/../include" @LEANC_EXTRA_FLAGS@) -ldflags=("-L$bindir/../lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) -ldflags_ext=(@LEANC_STATIC_LINKER_FLAGS@) -args=("$@") -for arg in "$@"; do - case $arg in - -shared) - # switch to shared linker flags - ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@) - ;; - -lleanshared | *libleanshared.*) - # linking against libleanshared explicitly (or linking libleanshared itself) ~> do not link against static stdlib - ldflags_ext=() - ;; - -c) - ldflags=() - ldflags_ext=() - ;; - --print-cflags) - echo "${cflags[@]}" - exit - ;; - --print-ldflags) - echo "${cflags[@]} ${ldflags_ext[@]} ${ldflags[@]}" - exit - ;; - esac -done - -[ -n "$LEAN_CC" ] || LEAN_CC="@LEANC_CC@" - -$LEAN_CC "${cflags[@]}" "${args[@]}" "${ldflags_ext[@]}" "${ldflags[@]}" -Wno-unused-command-line-argument +# used only for building Lean itself +root=$(dirname $0) +${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ "$@" "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@ -Wno-unused-command-line-argument diff --git a/src/stdlib.make.in b/src/stdlib.make.in index eca7dfe723..c5eacb6b89 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -8,7 +8,8 @@ export LEANC_GMP=${GMP_LIBRARIES} # LEAN_OPTS: don't use native code (except for primitives) since it is from the previous stage # MORE_DEPS: rebuild the stdlib whenever the compiler has changed LEANMAKE_OPTS=\ - LEAN="${CMAKE_CROSSCOMPILING_EMULATOR} ${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\ + LEAN="${CMAKE_CROSSCOMPILING_EMULATOR} ${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\ + LEANC="${CMAKE_BINARY_DIR}/leanc.sh"\ OUT="${LIB}"\ LIB_OUT="${LIB}/lean"\ OLEAN_OUT="${LIB}/lean"\ @@ -41,7 +42,7 @@ Lean: Init Std # we specify the precise file names here to avoid rebuilds ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${LIB}/lean/libStd.a ${LIB}/lean/libLean.a ${LIB}/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a @echo "[ ] Building $@" - "${LEAN_BIN}/leanc" -shared -o $@ ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS} + "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS} leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} @@ -50,6 +51,9 @@ Leanpkg: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} $(LEAN_SHELL) @echo "[ ] Building $@" - ${LEAN_BIN}/leanc $(LEAN_SHELL) -lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} -o $@ + "${CMAKE_BINARY_DIR}/leanc.sh" $(LEAN_SHELL) -lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} -o $@ lean: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX} + +Leanc: + +"${LEAN_BIN}/leanmake" bin PKG=Leanc BIN_NAME=leanc${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="${CMAKE_BINARY_DIR}" OLEAN_OUT="${CMAKE_BINARY_DIR}"