Self-contained native toolchain

Stream: lean4

[Sebastian Ullrich]

There's now a "release candidate" for a self-contained LLVM toolchain bundled with Lean at https://github.com/Kha/lean4/releases/tag/v4.0.0-bundle-rc (PR: https://github.com/leanprover/lean4/pull/795). What this means is that this Lean release should contain everything necessary to compile Lean into native shared libraries or executables. In particular, it is an important step towards automatically compiling e.g. mathlib tactics into native code during building and editing without the user having to set up a compiler, linker, headers, ... first.

I would be grateful if people could try and test-drive the release on various machines. You could for example try to build the Lake binary with it:

elan self update  # needs at least 1.3.0
git clone https://github.com/leanprover/lake.git
cd lake
lake +Kha/lean4:v4.0.0-bundle-rc build
./build/bin/lake

While you should not need to install any further dependencies (and ideally have as few development dependencies already installed as possible), these are the system dependencies I am aware of:

• Linux: glibc >= 2.27 (e.g. Ubuntu >= 18.04), should be the same as current Lean 4
• Windows: >= 10
• macOS: >= 10.15 I think... so should be fine. M1 with Rosetta seems to just work as well.
• NixOS: https://nixpk.gs/pr-tracker.html?pr=146162

[Yakov Pechersky]

elan self update
info: checking for self-updates
info: downloading self-update
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download file from 'https://github.com/Kha/elan/releases/download/v1.3.1/elan-x86_64-unknown-linux-musl.tar.gz' to '/tmp/elan-update.dNmYPBGPZL8a/elan-x86_64-unknown-linux-musl.tar.gz'
info: caused by: http request returned an unsuccessful status code: 404

On WSL Windows 10

[Alex J. Best]

Looks like it works for me:

git clone https://github.com/leanprover/lake.git
cd lake
lake +Kha/lean4:v4.0.0-bundle-rc build
./build/bin/lake
info: checking for self-updates
Cloning into 'lake'...
remote: Enumerating objects: 2179, done.
remote: Counting objects: 100% (2179/2179), done.
remote: Compressing objects: 100% (1346/1346), done.
remote: Total 2179 (delta 1496), reused 1423 (delta 746), pack-reused 0
Receiving objects: 100% (2179/2179), 340.66 KiB | 2.52 MiB/s, done.
Resolving deltas: 100% (1496/1496), done.
info: downloading component 'lean'
106.3 MiB / 106.3 MiB (100 %)   3.2 MiB/s ETA:   0 s
info: installing component 'lean'
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/LeanVersion.olean -c ./build/ir/Lake/LeanVersion.c ././Lake/LeanVersion.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Build/Trace.olean -c ./build/ir/Lake/Build/Trace.c ././Lake/Build/Trace.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Util/Async.olean -c ./build/ir/Lake/Util/Async.c ././Lake/Util/Async.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Util/LogT.olean -c ./build/ir/Lake/Util/LogT.c ././Lake/Util/LogT.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Config/InstallPath.olean -c ./build/ir/Lake/Config/InstallPath.c ././Lake/Config/InstallPath.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Config/OpaquePackage.olean -c ./build/ir/Lake/Config/OpaquePackage.c ././Lake/Config/OpaquePackage.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Config/Workspace.olean -c ./build/ir/Lake/Config/Workspace.c ././Lake/Config/Workspace.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Config/Glob.olean -c ./build/ir/Lake/Config/Glob.c ././Lake/Config/Glob.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Config/Script.olean -c ./build/ir/Lake/Config/Script.c ././Lake/Config/Script.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Build/Recursive.olean -c ./build/ir/Lake/Build/Recursive.c ././Lake/Build/Recursive.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/DSL/Attributes.olean -c ./build/ir/Lake/DSL/Attributes.c ././Lake/DSL/Attributes.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Util/MainM.olean -c ./build/ir/Lake/Util/MainM.c ././Lake/Util/MainM.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Util/CliT.olean -c ./build/ir/Lake/Util/CliT.c ././Lake/Util/CliT.lean
> /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/leanc -c -o ./build/ir/Lake/Config/OpaquePackage.o ./build/ir/Lake/Config/OpaquePackage.c -O3 -DNDEBUG
> /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/leanc -c -o ./build/ir/Lake/LeanVersion.o ./build/ir/Lake/LeanVersion.c -O3 -DNDEBUG
> /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/leanc -c -o ./build/ir/Lake/Config/Script.o ./build/ir/Lake/Config/Script.c -O3 -DNDEBUG
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Util/Git.olean -c ./build/ir/Lake/Util/Git.c ././Lake/Util/Git.lean
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Version.olean -c ./build/ir/Lake/Version.c ././Lake/Version.lean
> /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/leanc -c -o ./build/ir/Lake/Config/Workspace.o ./build/ir/Lake/Config/Workspace.c -O3 -DNDEBUG
> /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/leanc -c -o ./build/ir/Lake/DSL/Attributes.o ./build/ir/Lake/DSL/Attributes.c -O3 -DNDEBUG
> /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/leanc -c -o ./build/ir/Lake/Util/LogT.o ./build/ir/Lake/Util/LogT.c -O3 -DNDEBUG
> LEAN_PATH=./build/lib /home/alex/.elan/toolchains/Kha--lean4---v4.0.0-bundle-rc/bin/lean -R ./. -o ./build/lib/Lake/Build/MonadCore.olean -c ./build/ir/Lake/Build/MonadCore.c ././Lake/Build/MonadCore.lean
<SNIP>
./build/ir/Lake/Config/InstallPath.o ./build/ir/Lake/Build/Module.o ./build/ir/Lake/LeanVersion.o ./build/ir/Lake/Build/Trace.o ./build/ir/Lake/Build/MonadCore.o ./build/ir/Lake/Config/Script.o -rdynamic
Lake version 3.0.0-pre (Lean version master (4.0.0))

USAGE:
  lake [OPTIONS] <COMMAND>

OPTIONS:
  --version             print version and exit
  --help, -h            print help of the program or a command and exit
  --dir, -d=file        use the package configuration in a specific directory
  --file, -f=file       use a specific file for the package configuration
  --lean=cmd            specify the `lean` command used by Lake

COMMANDS:
  new <name>            create a Lean package in a new directory
  init <name>           create a Lean package in the current directory
  server                start the Lean language server
  run <script>          run arbitrary package scripts
  configure             download and build dependencies
  build [<targets>...]  configure and build targets
  clean                 remove build outputs

See `lake help <command>` for more information on a specific command.

[Henrik Böving]

Works for me on Fedora 35 without any issues for lake, lean4-socket and the few small projects I built myself with lake \o/ @Sebastian Ullrich

[Sebastian Ullrich]

@Yakov Pechersky Ah, I assume you haven't updated elan in a while. You'll probably need to reinstall it via

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

[Gabriel Ebner]

lean4-socket fails for me on nixos. I guess we need support for the system compiler in lake:

examples/gethostname
error: ./../../././native/native.c:13:10: fatal error: 'stdlib.h' file not found
#include <stdlib.h>
         ^~~~~~~~~~
1 error generated.

error: external command leanc exited with status 1
error: build failed

[Henrik Böving]

Oh if i try to run the examples it fails as well :( Seems like it only ever then tries to compile the C code.

[Scott Morrison]

Works for me on macOS (11.6).

[Scott Morrison]

I tried in an ubuntu Docker container, just installing git and curl from apt-get, then installing elan, then your instructions.

Curiously, lake +Kha/lean4:v4.0.0-bundle-rc build builds, but then ./build/bin/lake takes about 70s before returning. Subsequent runs seem fine!?

[Wojciech Nawrocki]

Scott Morrison said:

Curiously, lake +Kha/lean4:v4.0.0-bundle-rc build builds, but then ./build/bin/lake takes about 70s before returning. Subsequent runs seem fine!?

I also observed this.

[Gabriel Ebner]

Looking at your dockerfile, I believe the last lake build call will download then lean version specified in /home/lean/lake/lean-toolchain.

[Scott Morrison]

Do you mean the ./build/bin/lake call, rather than "the last `lake build'" call?

[Gabriel Ebner]

You might also want to pass --default-toolchain none to the elan installer. Then you don't need to elan uninstall stable.

[Gabriel Ebner]

@Sebastian Ullrich I see that you've just merged the PR. What is the recommended way to compile interfaces to native libraries now? The leanc wrapper no longer finds system libraries. Try e.g. lake run examples in https://github.com/xubaiw/lean4-socket as mentioned above:

examples/sockaddr
error: ./../../././native/native.c:13:10: fatal error: 'stdlib.h' file not found
#include <stdlib.h>
         ^~~~~~~~~~
1 error generated.

error: external command leanc exited with status 1
error: build failed

[Sebastian Ullrich]

Ah sorry, I didn't take a closer look at how this is set up in existing projects. I think the clean solution is to replace calls to leanc with cc $(leanc --print-cflags).

[Sebastian Ullrich]

@Mac This is probably a good time to expose leanc's cflags/ldflags variables as declarations? We can stick them in uhhhh Lean.Compiler.FFI I guess.

[Mac]

@Sebastian Ullrich sounds good to me

[Sebastian Ullrich]

@Mac I've reviewed the possible cflags options and the only flag apart from the -I relevant for building custom .o files is -fPIC on Linux. But since the question of whether position-independent code is needed depends on what the eventual link target is, I wonder if that should be regarded a build system concern. "All you need to compile against the Lean API is to include $LEAN_SYSROOT/include" sounds like a good invariant to guarantee to me.

[Mac]

@Sebastian Ullrich Cool! Furthermore, Lake already provides that path with getLeanIncludeDir.

Personally, though, I still think it would a good idea to expose leanc's configuration options (default compiler, internal/extra cflags, internal/static/shared ldflags) in Lean proper so that tools (like Lake) can potentially leverage them in customized approaches.

[Sebastian Ullrich]

See PR :)

[Sebastian Ullrich]

:eyes:

$ git diff
diff --git a/lakefile.lean b/lakefile.lean
index fde5791..a5a070b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,3 +4,5 @@ open System Lake DSL
 package lake where
   binRoot := `Lake.Main
   supportInterpreter := true
+  moreLeancArgs := #["-target", "x86_64-w64-windows-gnu", "-fno-PIC", "--sysroot", "/home/sebastian/Downloads/lean-4.0.0-windows"]
+  moreLinkArgs := #["-target", "x86_64-w64-windows-gnu", "-fno-PIC", "--sysroot", "/home/sebastian/Downloads/lean-4.0.0-windows"]

$ ~/Downloads/lean-4.0.0-linux/bin/lake build
...
error: lld: error: unknown argument: --as-needed

$ /home/sebastian/Downloads/lean-4.0.0-linux/bin/leanc -o ./build/bin/lake ... # massage linker cmdline a bit since `leanc` doesn't check for `-target` yet...

$ file build/bin/lake.exe
build/bin/lake.exe: PE32+ executable (console) x86-64, for MS Windows

$ WINEPATH=~/Downloads/lean-4.0.0-windows/bin nix shell nixpkgs#wineWowPackages.stable -c wine build/bin/lake.exe
0050:err:ole:start_rpcss Failed to start RpcSs service
Lake version 3.0.0-pre (Lean version master (4.0.0))

USAGE:
  lake [OPTIONS] <COMMAND>
...

[Sebastian Ullrich]

Step 3 shows that a bit more setup is yet to be done, but the bundled release for Windows apparently contains all the files necessary to cross-compile Lean programs to Windows. Supposedly the same is true for the other two platforms.

[Sebastian Ullrich]

$ git diff
diff --git a/lakefile.lean b/lakefile.lean
index fde5791..7c68820 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,3 +4,5 @@ open System Lake DSL
 package lake where
   binRoot := `Lake.Main
   supportInterpreter := true
+  moreLeancArgs := #["-target", "x86_64-apple-darwin", "--sysroot", "/home/sebastian/Downloads/lean-4.0.0-darwin"]
+  moreLinkArgs := #["-target", "x86_64-apple-darwin", "--sysroot", "/home/sebastian/Downloads/lean-4.0.0-darwin"]

$ file build/bin/lake
build/bin/lake: Mach-O 64-bit x86_64 executable, flags:<NOUNDEFS|DYLDLINK|TWOLEVEL|WEAK_DEFINES|BINDS_TO_WEAK|PIE|HAS_TLV_DESCRIPTORS>

[Gabriel Ebner]

Nice! Does elan still have the code to install multiple targets?

[Sebastian Ullrich]

I don't think so, but the obvious next step is for elan's leanc to recognize -target, download the appropriate release on the fly (into the existing toolchain dir?), and pass it as --sysroot, no? :laughter_tears:

[Sebastian Ullrich]

(It doesn't quite work that way because the leanc lake will call will not be elan's)

[Floris van Doorn]

This works for me on both Windows 10 and Ubuntu 20.04

[Locria Cyber]

It might be better to bundle liblean* source code (C++), like what Zig did to libc.

[Sebastian Ullrich]

This is a pretty vacuous statement without defining "better". But also, leanc is not capable of building the C++ code, it's specifically made for compiling Lean's C output and in the future will presumably be replaced by the pure-LLVM IR pipeline.

[François G. Dorais]

Aside: Does extern inline llvm work? Or is extern inline restricted to c?

[Henrik Böving]

Extern inline LLVM is planned but not implemented