feat: use leanc written in Lean for testing & distribution

building is still handled by a (minimal) Bash script for bootstrapping purposes

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 {

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)

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

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

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}"