wasm build

Stream: lean4

[Alexander Bentkamp]

I am working on compiling lean to wasm. I am getting these warnings about signature mismatches, which seem to cause runtime errors later.

wasm-ld-13: warning: function signature mismatch: lean_llvm_initialize_target_info
>>> defined as (i32) -> i32 in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libLean.a(EmitLLVM.o)
>>> defined as () -> i32 in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleancpp.a(llvm.cpp.o)

wasm-ld-13: warning: function signature mismatch: lean_io_rename
>>> defined as (i32, i32, i32) -> i32 in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libInit.a(IO.o)
>>> defined as (i32, i32) -> i32 in /home/alex/Projects/lean4/build/release/stage1/runtime/libleanrt_initial-exec.a(io.cpp.o)

wasm-ld-13: warning: function signature mismatch: lean_local_ctx_mk_local_decl
>>> defined as (i32, i32, i32, i32, i32) -> i32 in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleancpp.a(local_ctx.cpp.o)
>>> defined as (i32, i32, i32, i32, i32, i32) -> i32 in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libLean.a(LocalContext.o)

wasm-ld-13: warning: function signature mismatch: llvm_count_params
>>> defined as (i32, i32) -> i64 in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libLean.a(EmitLLVM.o)
>>> defined as (i32, i32, i32) -> i64 in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleancpp.a(llvm.cpp.o)

wasm-ld-13: warning: function signature mismatch: lean_llvm_get_default_target_triple
>>> defined as (i32) -> i32 in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libLean.a(EmitLLVM.o)
>>> defined as (i32, i32) -> i32 in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleancpp.a(llvm.cpp.o)

All of these are opaque Lean definitions that are connected to C code via @[extern], but the C code always has one more argument than the Lean function. Any ideas what's going on here?

[Sebastian Ullrich]

I am working on compiling lean to wasm

That's great to hear!

All of these are opaque Lean definitions that are connected to C code via @[extern], but the C code always has one more argument than the Lean function

I opened lean4#2433 to address these

[Alexander Bentkamp]

That's great to hear!

No promises. I have no idea what I am doing :-)

[Alexander Bentkamp]

@Sebastian Ullrich I hope I can some advice from you again. I have compiled Lean to wasm, but when executed, I get this error. I assume that I should replace a 64bit function by 32bit for the wasm build? But how? (BTW, I think the warning warning: unsupported syscall: __syscall_prlimit64 is unrelated)

$ node stage1/bin/lean.js
warning: unsupported syscall: __syscall_prlimit64

Aborted(alignment fault)
/home/alex/Projects/lean4/build/release/stage1/bin/lean.js:79
   throw ex;
   ^

RuntimeError: unreachable
    at __trap (wasm://wasm/25671866:wasm-function[158293]:0x6ee7463)
    at ___trap (/home/alex/Projects/lean4/build/release/stage1/bin/lean.js:141294:54)
    at abort (/home/alex/Projects/lean4/build/release/stage1/bin/lean.js:585:3)
    at alignfault (/home/alex/Projects/lean4/build/release/stage1/bin/lean.js:324:2)
    at _alignfault (/home/alex/Projects/lean4/build/release/stage1/bin/lean.js:16944:25)
    at SAFE_HEAP_STORE_i64_8_8 (wasm://wasm/25671866:wasm-function[164989]:0x6f8f0c8)
    at lean_ctor_set_uint64.5 (wasm://wasm/25671866:wasm-function[12482]:0x9a7bc9)
    at l_Lean_Name_str___override (wasm://wasm/25671866:wasm-function[12835]:0x9c07df)
    at lean_name_mk_string (wasm://wasm/25671866:wasm-function[12839]:0x9c0d9b)
    at lean::name_mk_string_of_cstr(lean_object*, char const*) (wasm://wasm/25671866:wasm-function[139067]:0x697dc06)

Node.js v19.4.0

[Sebastian Ullrich]

@Alexander Bentkamp Not sure I'm afraid. It should be two pointers followed by a uint64, so one would think it would be aligned naturally :thinking: ...

[Alexander Bentkamp]

Thanks, in the meantime I have become more confident again that I can figure this out.

[Sebastian Ullrich]

In general it could definitely be the case that we missed alignment issues from size_t < uint64_t

[Rujia Liu]

Any update? I'm also interested in wasm build. If this is still not finished, maybe I can try. Thanks! @Alexander Bentkamp

[Alexander Bentkamp]

Please do try. You'll probably be faster than me.

But I can share some infos. I just discussed this with @Sebastian Ullrich in person. The build command we came up with is as follows:

git clone https://github.com/leanprover/lean4 --recurse-submodules
cd lean4
mkdir -p build/release
cd build/release
cmake ../.. -DUSE_GMP=OFF -D CMAKE_C_COMPILER=emcc -D CMAKE_CXX_COMPILER=emcc -DUSE_GMP=OFF -DCMAKE_C_FLAGS=-fPIC -DCMAKE_CXX_FLAGS=-fPIC -DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang
make

The idea is to build a native 32 bit binary in stage0. For stage1, we then use the native 32bit binary to build 32bit oleans and a wasm binary. That way, we can avoid building the oleans using the wasm binary, which would be much slower.

I ran into a couple of issues:

• First, I got the error fatal error: 'cstdlib' file not found 32bit. I could resove this by sudo apt-get install gcc-multilib g++-multilib.
• Then, the build stops multiple times with segmentation faults. When you run make again, however, it seems that it manages to build the files on the second attempt.
• Finally there seems to be an issue with --gc-sections, so I removed the line 343 string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--gc-sections") from src/CMakeLists.txt.

With these fixes, the build suceeds eventually, but I haven't tested whether the binaries are usable.

[Rujia Liu]

Thanks for your info! I'll try :)

[Rujia Liu]

Could you tell me your platform info? @Alexander Bentkamp I assume you're using a recent linux and recent gcc? I'm on windows 10 and planning to try out other compilers and building scripts as well (not just for wasm build. For native x64 build I still wish I could debug in Visual Studio :D)

But of course I'll try the popular emscripten docker (which uses gcc) first.

[Alexander Bentkamp]

Yes, I use a recent Ubuntu. But for compilation of the 32bit binary, I use clang instead of gcc.

[Alexander Bentkamp]

For the wasm build I installed emsdk and use the contained emcc.

[Rujia Liu]

Ok, I've started. Since I'm very new to lean, I started by building a "regular lean" and tried to understand what's going on before diving directly to wasm. Now I have a question: what should we expect from a wasm build? Probably most people are mainly expecting a proof assistant on the web, but I'm a programmer, my main purpose is to explore ways of using lean to develop realiable (and reasonably fast) softwares, so maybe we're expecting different feature sets?

From my (very limited) understanding, stage1 involves calling stage0 binary to copile .lean to .olean, then .c, and use a C compiler to compile it to binary, but for wasm, we need to have a compiler in wasm? Or maybe lean.exe --run actually runs the program directly instead of doing AOT with a C compiler or LLVM? For me, the ideal solution is to allow executing lean codes in the browser with some interpreter mode without depending on a C compiler (or even LLVM) on the web, and at the same time allows the user to AOT the codes directly to wasm without depending on lean compiler (but can depend on a small runtime library of course)

Anyway, it is reasonable to setup my first goal to: make something like node stage1/bin/lean.js hello.lean --run print a Hello World? (the command line is hypothetical) @Alexander Bentkamp @Sebastian Ullrich

[Alexander Bentkamp]

Right, I would be more interested in getting lean.js --server to work, but there is probably some overlap in our goals.

[Rujia Liu]

I see. What's the purpose of --server? Start a language server that for example can talk to vscode? Or something that needs another dedicated client?

[Siddharth Bhat]

I've begun investigating a build of lean where the ABI is 32 bit without even involving wasm into the mix. This is necessary as wasm also uses a 32 bit ABI. Such a build already fails (the stage0 compiler mysteriously segfaults on compiling stage1). I have a collection of "litmus tests" I developed for the Lean compiler when working on it (https://github.com/bollu/lean4/tree/1-aug-2022-llvm-backend/tests/backendramp). I'm going to try the stage0 compiler on these tests to see if they isolate the problem. Help is very much appreciated :)

the steps necessary for this setup (I specialize for ubuntu, similar instructions apply for other linuxes):

1. Install a toolchain for cross compiling to i386/i686:

$ sudo apt install g++-i686-linux-gnu

2. Run a build of Lean with i686, without GMP (the cross compile toolchain doesn't have the GMP version for the target architecture, so disable it):

$ cd /path/to/lean4
$ export CXX=i686-linux-gnu-g++
$ export CC=i686-linux-gnu-gcc
$ mkdir -p build/release && cd build/release
$ cmake ../../ -DUSE_GMP=OFF
$ VERBOSE=1 make -j4 stage1

Now watch the stage0 compiler crash when building Structural/FindRecArg.olean for stage1. Happy debugging :smile:

More seriously, I'm yet to debug what's going on here, and help would be super useful. Throwing the stage0 command into GDB and seeing where it crashes would be progress!

[Rujia Liu]

Thank you @Siddharth Bhat That's super helpful. I'll look into this. Interestingly I've just finished porting to wasm of another programming language implementation which also involved porting to 32-bit as a first step. I had to look very carefuly into the codebase and figure out which usize should be u64 and vice-versa (the codebase is in rust). I even had to modify some memory layout to make some low-level tricks to work. The key to my success with that programming language is a set of very low-level tests, and your "litmus tests" would be extremely helpful when tackling the same problem in lean! Thank you again!

[Siddharth Bhat]

Glad to hear it, feel invited to ping me if you get stuck / want help @Rujia Liu !

[Rujia Liu]

After reading some codes, I think I can answer some of my own questions: lean --run runs a simple interpreter defined in ir_interpreter.cpp which is exactly designed for use cases like wasm; lean --server is indeed LSP watchdog, and related info is described in src/lean/Server/README.md. But since I haven't read very carefully, correct me if I'm wrong :)

[Rujia Liu]

@Siddharth Bhat I tried to build 32-bit with msys32 (I only have windows 10 now) and it succeeded! At least the generated FindRecArg.olean "looks like" 32-bit because it's only 923KB while in the default 64-bit build it's 1.3MB. The generated .ilean and .c are identical, but I think it's normal? I've played around the final stage1/bin/lean.exe and cannot make it crash by compiling some code.

The only difference I can see, is I'm using -fPIC as suggested by @Alexander Bentkamp , But it could also be the difference between msys32 and unbuntu. Anyway, I have experience that some programs that "should" crash, don't crash on windows :) So could you first try to build it with -fPIC? If it still crashes, I'll try docker instead (It'll be great if you have a Dockerfile that can reproduce the crash)

[Rujia Liu]

Oh! I forgot to run make test! It reported 93/1721 tests failed, so that means windows is good at "crash prevention" and the binary is still buggy (though not easily crashing). I think I'll try to find out why these tests are failing tomorrow, but I'm very new to lean so I definitely need help :)

[Rujia Liu]

I looked into the failed tests. Most of them are failed to create thread(maybe my mingw32 environment is incomplete), only 4 of them are actually mismatches, and one of them (updateExprIssue) only had an misplaced empty line. Another one of them (307) should be integer overflow problem, other two tests (csimpAttr and unhygienicCode) are quite confusing.

[Siddharth Bhat]

Thanks a lot for looking into it. Let me try compiling with PIC and see if the result changes on ubuntu.

[Rujia Liu]

Maybe you don't need to compile with -fPIC anymore because just now I tried a fresh build without -fPIC, still in msys2, and got the same set of failed tests.

[Rujia Liu]

I'm trying to understand more about the compiler. Could you tell me what's olean used for? I thought .olean is used to produced .c but after reading console output when building stage1, I can see that stage0's lean.exe is used to produce .olean file and a .c file in the same command, so it looks like the .c is not produced from a .olean? I'm saying this because it looks like the .c files produced from 32-bit and 64-bit systems are the same, but the .olean files are different. If we don't need these .olean files in the build process (though probably needed by some other places), I can concentrate on the runtime codes and not codes reading/writing olean files, which should be much easier to follow, and we can use a 64-bit stage0 lean.exe to compile a 32-bit stage 1 lean.exe? @Siddharth Bhat

[Mario Carneiro]

.olean files are what lean itself needs to process later lean files

[Mario Carneiro]

it has e.g. the elaborated lean declarations in the module, any initializer declarations that need to be run and data for the environment extensions

[Mario Carneiro]

lean will produce both .c and .olean files from a given lean file

[Mario Carneiro]

so it looks something like foo.lean + import1.olean + import2.olean -> lean -> foo.olean + foo.c

[Mario Carneiro]

and then foo.c -> leanc -> foo.o and foo.o, bar.o, main.o -> ld -> main.exe like a regular C project (if you are actually generating an executable, libraries like mathlib skip this stage)

[Rujia Liu]

Thank you! That's very clear! I think building stage1 involves calling both stage0 and stage1's lean.exe so I should make both 32-bit (or both 64-bit).
Another question: I'm a long time Visual Studio user but unfortunately the current cmake said only Unix Makefile is supported, but reading CMakelist.txt I have an impression that it used to support native Visual Studio generator? Anyway, will it be difficult to modify the script (or probably write my own) to generate a Visual Studio solution (I feel more confident to debug within Visual Studio than with gdb or lldb)? It looks like the building process is not very complicated, but I don't know whether there are lots of subtle issues or even traps.

[Sebastian Ullrich]

Our build process is very much Unix focused in various aspects, there is no intention to change that

[Siddharth Bhat]

@Rujia Liu The build process is subtle, and in my experience has been complex to modify.

[Rujia Liu]

Thank you @Sebastian Ullrich @Siddharth Bhat Then I would rather not mess with it for now. I'm reasonably comfortable with this current build process.

Now I'm trying to bulid wasm with the official emscripten docker, but hoping to build a stage0 wasm32 binary as a first step. However, I got the same problem as the very first message in this topic (signature mismatch). I then realized that although the codes were fixed, stage0 was not updated. Maybe that's the reason why you built a native 32-bit stage0, then a wasm32 stage1. However, the docker doesn't have 32-bit clang and my development machine don't have Internet access to do apt-get. My plan is to copy my msys32 generated .c files back to my docker container's stdlib directory and copy c++ codes inside src to stage0 (i.e. do a manual update of stage0), hope it will work...

[Rujia Liu]

My manual update to stage0 looks good. At least it successfully built. wasm-ld reported that sigaltstack is undefined, which I think is not supported by emscripten so I disabled it.

However, I was unable to execute it (got some bad memory error). I thought it may be related to multi-threading, so I tried to disable multi-threading, but mutex.cpp doesn't compile. It'll be help if @Alexander Bentkamp can remember some details:

• Did you disable multi-threading? (maybe not, because you successfully built it)
• Did you disable BSYMBOLIC? I had to do this otherwise wasm-ld will complain
• Did you change CMAKE_AR to emar? I did anyway, but don't know whether it's doing anything helpful or bad
• Did you disable undefined symbol error? (I had to do this to workaround the sigaltstack problem)
• Did you add any extra flags to emcc? I had to add -s USE_PTHREADS=1 to lean's own cxx flags otherwise wasm-ld will complain. But I don't have time to add those memory flags today.

If can't make multi-threaded version work, can I first try to make single-threaded lean work? I have an impression that emscripten's pthread support isn't great and in my several other projects disabled them (but some are using it successfully) @Sebastian Ullrich

[Alexander Bentkamp]

As I wrote, I hadn't tested whether the binaries I managed to compile are usable. They are not. I ran into similar issues that you are reporting.

[Alexander Bentkamp]

My new approach is to start with a very old version of Lean, in which wasm was working:

git clone https://github.com/leanprover/lean4 --recurse-submodules
cd lean4
git checkout d92e4a7
mkdir -p build/release
cd build/release
emcmake cmake ../.. -DUSE_GMP=OFF
emmake make -j8 stage0

This produces a usable wasm binary on stage0. Now I am trying to gradually work forward to the present version of Lean while making sure that the binary still works.

[Rujia Liu]

Thanks! That's good news! what's the date of that commit? My network is too bad for a complete clone so mine is a very shallow clone. Anyway, I'd like to stick with current version, so let's take different routes :)

[Alexander Bentkamp]

It's from Jun 6, 2021

[Rujia Liu]

That's long time ago. Thanks for your info.

[Rujia Liu]

I've manually fix the compilation problem in single-threaded lean, but I cannot prevent calling initialize_stack_overflow() from crashing so I disabled it. I hope it will not cause problems later on. After that, when running when node, it got the following error:

Calling stub instead of signal()
exception thrown: RangeError: Maximum call stack size exceeded,RangeError: Maximum call stack size exceeded
    at lean_apply_1 (wasm-function[127664]:0)
    at l_Lean_Parser_andthenInfo___elambda__1 (wasm-function[69888]:77)
    at lean_apply_1 (wasm-function[127664]:5749)
    at l_Lean_Parser_andthenInfo___elambda__1 (wasm-function[69888]:77)
    at lean_apply_1 (wasm-function[127664]:5749)
    at l_Lean_Parser_andthenInfo___elambda__1 (wasm-function[69888]:77)
    at lean_apply_1 (wasm-function[127664]:5749)
    at l_Lean_Parser_andthenInfo___elambda__1 (wasm-function[69888]:77)
    at lean_apply_1 (wasm-function[127664]:5749)
    at l_Lean_Parser_nodeInfo___elambda__1 (wasm-function[69895]:135)

I've already increased node's stack but larger stack results in less information (just "Exception thrown"), so maybe it's indeed infinite recursion? Any idea/hunches?

[Rujia Liu]

Some progress: now the wasm build can print the usage, the feature set (--features) and the libdir (--print-libdir). It reports Unknown package 'Init' when trying to run a hello world program, because there is no .olean in the libdir. But since I'm only trying single-threaded version, there is no --server so I can't test it. @Alexander Bentkamp

[Alexander Bentkamp]

How about echo "prelude\n#check Prop" | node lean --stdin?

[Rujia Liu]

Ok let me try (it's in another computer, I need to move myself)

[Rujia Liu]

<stdin>:1:7: error: expected token
Prop : Type
program exited (with status: 1), but EXIT_RUNTIME is not set, so halting execution but not exiting the runtime or preventing further async execution (build with EXIT_RUNTIME=1, if you want a true shutdown)

[Alexander Bentkamp]

Looks good

[Sebastian Ullrich]

You could try Init.Prelude next

[Rujia Liu]

Do you mean replace "prelude" with "Init.Prelude"? It report Unkown Package 'init' again.

[Alexander Bentkamp]

I think he means

node lean --stdin < ~/Projects/lean4/src/Init/Prelude.lean

where ~/Projects/lean4 is the place where I have cloned the lean4 repo.

[Alexander Bentkamp]

Or

node lean ~/Projects/lean4/src/Init/Prelude.lean

achieves the same I guess...

[Rujia Liu]

Oh! I'm too new to lean to understand this... Anyway, here is the result:

<stdin>:1151:9: error: expected token
<stdin>:1370:14: error: typeclass instance problem is stuck, it is often due to metavariables
  Sub ?m.7261
<stdin>:1373:24: error: expected token
<stdin>:1432:8: error: expected token
<stdin>:2354:16: error: invalid {...} notation, expected type is not known
<stdin>:3086:34: error: expected token
<stdin>:3246:14: error: expected token
<stdin>:3249:2: error: expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'class', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax' or 'theorem'
<stdin>:3254:11: error: unknown constant 'CoeFun'
<stdin>:3256:34: error: unknown constant 'EStateM.Backtrackable.restore'
<stdin>:3262:11: error: unknown constant 'CoeFun'
<stdin>:3264:31: error: unknown constant 'EStateM.Backtrackable.restore'
<stdin>:3302:0: error: invalid occurrence of universe level 'u_1' at 'EStateM.instOrElseEStateM', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
  EStateM.orElse.{u, u_1}
at declaration body
  fun {ε σ α δ : Type u} [Backtrackable δ σ] => { orElse := EStateM.orElse }
<stdin>:3310:0: error: invalid occurrence of universe level 'u_1' at 'EStateM.instMonadExceptOfEStateM', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
  EStateM.tryCatch.{u, u_1}
at declaration body
  fun {ε σ δ : Type u} [Backtrackable δ σ] =>
    { throw := fun {α : Type u} => EStateM.throw, tryCatch := fun {α : Type u} => EStateM.tryCatch }
<stdin>:3342:2: error: 'restore' is not a field of structure 'EStateM.Backtrackable'
<stdin>:3474:48: error: unknown identifier 's'
<stdin>:3474:49: error: expected token
<stdin>:4389:29: error: failed to synthesize instance
  MonadWithReader ?m.73191 MacroM
<stdin>:4389:52: error: expected structure
<stdin>:4398:2: error: failed to synthesize instance
  MonadExcept Exception MacroM
<stdin>:4406:2: error: failed to synthesize instance
  MonadExcept Exception MacroM
<stdin>:4418:2: error: failed to synthesize instance
  MonadWithReader ?m.75079 MacroM
<stdin>:4418:25: error: expected structure
<stdin>:4424:13: error: failed to synthesize instance
  MonadExcept Exception MacroM
<stdin>:4425:13: error: failed to synthesize instance
  MonadWithReader ?m.75752 MacroM
<stdin>:4425:36: error: expected structure
<stdin>:4520:25: error: failed to synthesize instance
  MonadWithReader Syntax UnexpandM
program exited (with status: 1), but EXIT_RUNTIME is not set, so halting execution but not exiting the runtime or preventing further async execution (build with EXIT_RUNTIME=1, if you want a true shutdown)

[Alexander Bentkamp]

Hm, looks like a Lean version mismatch? At least, it didn't crash entirely :-)

[Rujia Liu]

I copied the .olean files produced by my ealier 32-bit lean (built with msys2 on Windows 10) into the docker and run the hello world program, it threw some exceptions with a very long stacktrace involving __mmap and at the very bottom there is lean_read_module_data which looks reasonable. Maybe I shouldn't mix olean files like this?

[Rujia Liu]

Oh, maybe... I'm in a rush so I can get something wrong.

[Alexander Bentkamp]

As far as I know, olean files should work as long the number of bits is the same (32/64).

[Rujia Liu]

I hope I can have some time to figure about the mismatch thing and the __map thing tomorrow, but I'm getting really busy

[Rujia Liu]

Oh, that's good news! Then maybe we just shouldn't use __mmap.
BTW: I've managed to build and debug lean with in Visual Studio so maybe I can handle this lean_read_module_data issue :)

[Alexander Bentkamp]

I am a bit stuck at commit 2418acd (August 20th, 2021)

Before that commit, when replacing the line size_t read_sz = std::min(remain, 65536); in stage0/src/runtime/io.cpp by size_t read_sz = std::min(remain, static_cast<size_t>(65536));, the following works fine:

emcmake cmake ../..
emmake make -j8 stage0

[Rujia Liu]

After disabling, the hello world program now gets: To use dlopen, you need to use Emscripten's linking support, see https://github.com/emscripten-core/emscripten/wiki/Linking

[Rujia Liu]

Alexander Bentkamp said:

I am a bit stuck at commit 2418acd (August 20th, 2021)

Before that commit, when replacing the line size_t read_sz = std::min(remain, 65536); in stage0/src/runtime/io.cpp by size_t read_sz = std::min(remain, static_cast<size_t>(65536));, the following works fine:
emcmake cmake ../..

I also modified that 65536 cast :) Did that commit modify CMakeList.txt? So far the biggest trap is to pass correct information to stage0... In the latest code, even with emcmake, stage0 didn't know it's emscripten :-S

[Alexander Bentkamp]

And after commit 2418acd, it all breaks down. The first issue can be solved by replacing

[ -n "$LEAN_CXX" ] || LEAN_CXX=c++

by

[ -n "$LEAN_CXX" ] || LEAN_CXX=emcc

in stace0/src/bin/leanc.in.
But then I get error: unable to find library -lgmp while building libleanshared.so and I am not sure how to fix this.

[Rujia Liu]

In the current code, the top-level CMakeList.txt seems to assume emscripten -> use_gmp. I just commented it. Maybe 2418acd has the same problem?

[Rujia Liu]

(It explictly added a dependency of gmp when detected Emscripten)

[Alexander Bentkamp]

Hm, yeah, I am not sure if I should use GMP or not. I think in 2021, there was no option to disable GMP at all.

[Alexander Bentkamp]

Sorry, got the commit number wrong. The problematic commit is 6521143.

[Rujia Liu]

I've leaving the office now. The 2nd biggest trap is to we must tell node to use a larger stack. All my current commands start with LEAN_PATH=/home/stage0/bin node --stack-size=8192 lean. The directory is /home is because in shell.cpp it only mounted /home and /tmp (but you can modify that after the build because that's in lean.js). Hope it helps...

[Rujia Liu]

Oh, GMP was mandatory at that time... I see. That's unfortunate (I hate using gmp with emscripten...)

[Rujia Liu]

And I can remember that I must make sure the definition LEAN_EMSCRIPTEN is available to all codes. Using emcc is not enough. Without it, all my attempts resulted in crahes.

[Rujia Liu]

Last try: change emcc parameter to -sMAIN_MODULE=2 according to https://emscripten.org/docs/compiling/Dynamic-Linking.html.
Now running hello world got Main.lean:1:0: error: could not find native implementation of external declaration 'IO.getRandomBytes' (symbols 'l_IO_getRandomBytes___boxed' or 'l_IO_getRandomBytes') so it didn't find that function even with dlopen enabled. Maybe I should also add EMSCRIPTEN_KEEPALIVE but I'm running out of time now.

[Alexander Bentkamp]

How do I make sure that LEAN_EMSCRIPTEN is always defined?

[Alexander Bentkamp]

Have you encountered _malloc is not a function?

[Patrick Massot]

That isn't possible: everything is a function in Lean.

[Alexander Bentkamp]

Must be an issue in the JS code then :grinning_face_with_smiling_eyes:

[Rujia Liu]

Alexander Bentkamp said:

How do I make sure that LEAN_EMSCRIPTEN is always defined?

I just passed it via -DSTAGE0_LEAN_EXTRA_CXX_FLAGS though I think a better way would be -DSTAGE0_CMAKE_TOOLCHAIN_FILE (haven't validated yet)

[Rujia Liu]

And no, I haven't encountered _malloc is not a function.

[Rujia Liu]

I added EMSCRIPTEN_KEEPALIVE and still no luck. However, after inspecting the generated wasm, I can see a lot of lean functions inside:

Exports:
  Functions:
    "__wasm_call_ctors": [] -> []
    "main": [I32, I32] -> [I32]
    "l_default_sizeOf___boxed": [I32, I32] -> [I32]
    "lean_apply_1": [I32, I32] -> [I32]
    "l_System_Uri_pathToUri___lambda__1___boxed": [I32, I32] -> [I32]
    "l_System_Uri_fileUriToPath_x3f___lambda__1___boxed": [I32] -> [I32]
    "l_System_Uri_fileUriToPath_x3f___lambda__2___boxed": [I32, I32] -> [I32]
    "l_Char_toUpper___boxed": [I32] -> [I32]
    "l___private_Init_System_FilePath_0__System_hashFilePath____x40_Init_System_FilePath___hyg_113____boxed": [I32] -> [I32]
    "l_System_FilePath_normalize___lambda__1___boxed": [I32, I32] -> [I32]
    "l_System_FilePath_normalize___lambda__2___boxed": [I32, I32] -> [I32]
    "l_System_FilePath_join": [I32, I32] -> [I32]
    "l_List_contains___at___private_Init_System_FilePath_0__System_FilePath_posOfLastSep___spec__1___boxed": [I32, I32] -> [I32]
    "lean_mk_io_user_error": [I32] -> [I32]
    "lean_mk_io_error_other_error": [I32, I32] -> [I32]
    "lean_io_error_to_string": [I32] -> [I32]
    "l_Char_toLower___boxed": [I32] -> [I32]
    "l_IO_Mutex_atomically___rarg___lambda__3___boxed": [I32] -> [I32]
    "lean_task_get": [I32] -> [I32]
    "l_EStateM_instInhabitedEStateM___rarg": [I32, I32] -> [I32]
    "l_EIO_toBaseIO___rarg": [I32, I32] -> [I32]
    "l_IO_monoNanosNow___boxed": [I32] -> [I32]
    "l_IO_sleep___lambda__1___boxed": [I32, I32] -> [I32]
    "l_IO_FS_Mode_noConfusion___rarg___lambda__1___boxed": [I32] -> [I32]
    "l_IO_FS_instInhabitedStream___lambda__1": [I32] -> [I32]
    "l_IO_FS_instInhabitedStream___lambda__2___boxed": [I32, I32] -> [I32]
    "l_IO_FS_instInhabitedStream___lambda__3___boxed": [I32, I32] -> [I32]
    "l___private_Init_System_IO_0__IO_FS_reprDirEntry____x40_Init_System_IO___hyg_2730____boxed": [I32, I32] -> [I32]
    "l___private_Init_System_IO_0__IO_FS_reprFileType____x40_Init_System_IO___hyg_2828____boxed": [I32, I32] -> [I32]
    "l___private_Init_System_IO_0__IO_FS_beqFileType____x40_Init_System_IO___hyg_2993____boxed": [I32, I32] -> [I32]
    "l___private_Init_System_IO_0__IO_FS_reprSystemTime____x40_Init_System_IO___hyg_3036____boxed": [I32, I32] -> [I32]
    "l___private_Init_System_IO_0__IO_FS_beqSystemTime____x40_Init_System_IO___hyg_3102____boxed": [I32, I32] -> [I32]
    "l___private_Init_System_IO_0__IO_FS_ordSystemTime____x40_Init_System_IO___hyg_3197____boxed": [I32, I32] -> [I32]
    "l___private_Init_System_IO_0__IO_FS_reprMetadata____x40_Init_System_IO___hyg_3371____boxed": [I32, I32] -> [I32]
    "l_IO_withStdin___rarg___lambda__2___boxed": [I32] -> [I32]
    "l_IO_mkRef___rarg": [I32, I32] -> [I32]

There are slightly above 10000 functions, but no l_IO_getRandomBytes___boxed. I wonder whether this looks like we hit some limitation of number of exported functions, or l_IO_getRandomBytes___boxed is really special.

[Rujia Liu]

I somehow forced to export that l_IO_getRandomBytes___boxed function but still got the same error. When running wasmer inspect, I got this:

error: failed to inspect `lean2.wasm`
╰─▶ 1: Validation error: effective type size exceeds the limit of 100000 (at offset 0x16f1e4)

So it looks like there is indeed some limitation?

[Alexander Bentkamp]

Looks like a limitation of wasmer inspect, not of wasm.

[Rujia Liu]

Ok, so the exported function table could be incomplete, too (I mean, the function is actually exported, but dsym() couldn't find it)? What do you suggest me to do next? I'm stuck

[Alexander Bentkamp]

where does this function actually get called? And where is it defined?

[Sebastian Ullrich]

dlsym is from the interpreter, trying to execute an initialize block in this case

[Sebastian Ullrich]

So if the exported symbol table is incomplete, that's a problem, yes

[Alexander Bentkamp]

Maybe -s LINKABLE=1 -s EXPORT_ALL=1 would help (https://stackoverflow.com/questions/33190760/export-all-functions-with-emscripten)

[Rujia Liu]

Hello world works now!!! @Alexander Bentkamp @Sebastian Ullrich It turns out that with emscripten, dlsym should be called in a specific way. Here is what I changed:

void * lookup_symbol_in_cur_exe(char const * sym) {
#if defined(LEAN_EMSCRIPTEN)
    void* self = dlopen(NULL, RTLD_LAZY);
    return dlsym(self, sym);
#endif

[Rujia Liu]

BTW: I've also added -s LINKABLE=1 -s EXPORT_ALL=1, thanks!

[Rujia Liu]

But there is still a weird thing:

node lean --stdin < /home/lean4/src/Init/Prelude.lean

Got the errors I posted, but

node lean /home/lean4/src/Init/Prelude.lean

Got no output at all (I guess this is the correct behavior?).

[Siddharth Bhat]

@Rujia Liu that’s very cool! Do you have your changes on a branch somewhere I can go see? :)

[Alexander Bentkamp]

I don't know why there would be a difference, but no output is the correct behavior.

[Alexander Bentkamp]

And yes, please share your setup :-)

[Rujia Liu]

Not at this moment... I made quite a few experiments that I've no idea which ones are working... After some cleaning up I'll push the changes into my fork (which doesn't exist yet :P) Could you wait some time because I'm busy currently

[Alexander Bentkamp]

Make sure to save the current state somewhere so that you don't lose it :D

[Rujia Liu]

Alexander Bentkamp said:

Make sure to save the current state somewhere so that you don't lose it :D

Yes! Great advice! That's what I often did :)

[Alexander Bentkamp]

And we'd be happy to see a version without cleanup as well :grinning_face_with_smiling_eyes:

[Rujia Liu]

Oh, nice to hear that :grinning_face_with_smiling_eyes:

[Rujia Liu]

Ok, created an PR for easier discussion (is there a better way?) https://github.com/leanprover/lean4/pull/2543 I hope that didn't violate any guidelines @Alexander Bentkamp @Siddharth Bhat

[Alexander Bentkamp]

Awesome, thanks a lot!

[Alexander Bentkamp]

Could you share the build commands you are using?

[Sebastian Ullrich]

And if you could (eventually) put them in a new CI job, that would be even better!

[Rujia Liu]

Oh! I thought I post the commands in the PR but apparently the post failed... Here it is:

cd /src/lean4/build/release
rm -rf *
emcmake cmake ../.. -DUSE_GMP=OFF -DSTAGE0_CMAKE_AR=/emsdk_portable/upstream/emscripten/emar -DSTAGE0_CMAKE_TOOLCHAIN_FILE=/emsdk_portable/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DDSTAGE0_CMAKE_CROSSCOMPILING_EMULATOR="/emsdk_portable/node/12.9.1_64bit/bin/node"
VERBOSE=1 emmake make -j4 stage0
"/src/lean4/build/release/stage0/leanc.sh" /src/lean4/build/release/stage0/shell/CMakeFiles/shell.dir/lean.cpp.o -Wl,--whole-archive -lInit -lLean -lleancpp -lleanrt -rdynamic -o /src/lean4/build/release/stage0/bin/lean -s ERROR_ON_UNDEFINED_SYMBOLS=0 -s ASSERTIONS=1 -s WASM=1 -fexceptions -lnodefs.js -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s LLD_REPORT_UNDEFINED=1
cp -a /src/lean4/build/release/stage0 /home
cd /home/stage0/bin
LEAN_PATH=/home/stage0/bin node --stack-size=8192 lean --run Main.lean

Note that I didn't bother changing the final command to build the wasm, so I added a followup command after make. The next command is to copy everything into a directory insode /home because the current code only mounted /home and /tmp. The last command is try to run a Hello World program (or whatever else).

[Rujia Liu]

Sebastian Ullrich said:

And if you could (eventually) put them in a new CI job, that would be even better!

I hope so! But I need to get rid of the follow up command first :laughing:

[Rujia Liu]

The local paths used in the command was reported by executing emcmake alone first. Ideally we need to pass those things to stage0 automatically?

[Rujia Liu]

Forgot to say: you need to update stage0 before building with emscripten because there are still extern function signature mismatches (the source codes were fixed long ago but stage0 was not updated after that) @Alexander Bentkamp

[Alexander Bentkamp]

How do I do that?

[Rujia Liu]

Oops, I missed the update. It looks like stage0 was updated after releasing official 4.0

[Rujia Liu]

Updated in c2a5730bc97ba89cf6bc586ec45ef6ae2a2c0271

[Alexander Bentkamp]

Ok, I updated stage0 like this:

rm -rf *
cmake ../..
make update-stage0

[Rujia Liu]

Oh, that's the official way. I discovered that after my manual update :sweat_smile:

[Alexander Bentkamp]

With that, the build works for me, too. I don't have the oleans ready to test though.

[Rujia Liu]

hmmm... maybe add a 32-bit build to CI and then you can download the oleans

[Alexander Bentkamp]

I tried to compile the multithreaded version. In stage0/src/CMakeLists.txt, I edited:

    # set(MULTI_THREAD OFF)
    # TODO(WN): code size/performance tradeoffs
    # - we're using -O3; it's /okay/
    # - -flto crashes at runtime
    # - -Oz produces quite slow code
    # - system libraries such as OpenGL are included in the JS but shouldn't be
    # - we need EMSCRIPTEN_KEEPALIVE annotations on exports to run meta-dce (-s MAIN_MODULE=2)
    # - -fexceptions is a slow JS blob, remove when more runtimes support the WASM exceptions spec

    # From https://emscripten.org/docs/compiling/WebAssembly.html#backends:
    # > The simple and safe thing is to pass all -s flags at both compile and link time.
    set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -s MAIN_MODULE=1 -fwasm-exceptions -pthread")
    string(APPEND LEANC_EXTRA_FLAGS " -pthread")

[Alexander Bentkamp]

This compiles, but lean --server yields:

Watchdog error: Cannot read LSP request: hardware fault (error code: 29)

[Rujia Liu]

Oh, I never tried that. Did multithreaded version work in that old version (2021 June) or just before the problematic commit 6521143?

[Rujia Liu]

Acoording to IOError.lean, that's just EIO (input/output error). Hardware fault looks scary :sweat_smile:

[Alexander Bentkamp]

I don't think --server ever worked...

[Alexander Bentkamp]

See also @Wojciech Nawrocki 's post on this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/web.20editor/near/281494817

[Alexander Bentkamp]

I'm not sure what he means when writing that wasm thread "execution semantics are specific to the web and would also need special support in the Lean runtime."

[Rujia Liu]

Thanks for the pointer. I'm leaving the office now and will try to read it home

[Wojciech Nawrocki]

Alexander Bentkamp said:

I'm not sure what he means when writing that wasm thread "execution semantics are specific to the web and would also need special support in the Lean runtime."

The point I was attempting to make is that the when you are a WASM blob running in a browser, the environment you observe and interact with just isn't the usual Unix-based OS environment. There are no processes and threads, instead there are Web Workers. There are no files, instead there are various objects that are similar to files in some respect, e.g. Web Storage or the File System API (this does access actual files on disk). Emscripten allows us to pretend to some extent that we are still programming against Unix, e.g. by implementing pthreads as a pool of web workers. Nevertheless the illusion is not perfect, and for first-class WASM support I believe there needs to be some dedicated support in the Lean runtime for these Web Things.

Note also that the in-progress LLVM backend may be capable of compiling Lean to WASM (because LLVM is) without any need for Emscripten. What you lose then is all these translation layers that the Emscripten runtime provides (e.g. for pthreads).

[Rujia Liu]

Thank you @Wojciech Nawrocki ! I can think of two other options:

• Use WASIX. However, it's wasmer-only (not a standard), but it seems to have everthing we need, including multiprocessing and sockets. Currently it doesn't support C++ but recently it filed an issue in zig to offer some money for WASIX support. When it's finished, maybe we can use zig cc to build lean4 and use WASIX? It seems to require least changes to lean4 codebase, but I've no idea whether it'll work at all.
• Use wasi-preview2 (after it's finalized). It requires us to at least write some wit definitions, and maybe other changes in lean4 codebase, but it should work. And since we go rid of emscripten, it will be much more lightweight.

I'm not an export in this area. Just writing down what I have in mind.

[Rujia Liu]

Another concern is that while the wasm + glue js is 100MB (11MB zipped), which is not too bad (a native libleanshared is already ~70MB), even 32-bit .oleans are as big as 500MB (190MB zipped), which is far beyond my expectation. It's not cool to having to dowload 200MB to use a fully browser based lean ide or similar service. Is there anyway (or ongoing effort) to solve/workaround this?

[Wojciech Nawrocki]

I cannot comment on WASI/WASIX. My impression was that these projects were aimed more at running WASM code in native applications (i.e., not inside a browser), but this impression may be incorrect. As for .olean size, at least part of the reason why Lean 4 .oleans are large is that it is possible to load them directly into memory by mmaping them. This is super-fast but comes at the cost of some disk space, since the objects we load up should be 'ready to go' rather than compressed somehow. The efforts of @Mario Carneiro on ltar (a tool that can compress .oleans well) might be relevant here.

[Mario Carneiro]

I think in order to be able to get smaller oleans on disk you need support in lean core for not doing the mmap thing (e.g. a compiler flag). Once this is done it is possible to deserialize and you can get an approximately 6x reduction in olean size before compression

[Rujia Liu]

Thank you both! WASI is designed for native applications, yes, but it has browser shims. WASIX also has browser support but after I read the discussions in that zig issue, now I don't think we can rely on WASIX in near future. As for .olean files: I already disabled mmap in my wasm build because I can't make it work with emscripten anyway. And it's great to know it'll be approximately 6x reduction by serializing, before compression.

[Alexander Bentkamp]

I've written a GitHub action that can reproduce @Rujia Liu 's achievement: https://github.com/abentkamp/lean4/blob/wasm-experiments/.github/workflows/wasm.yml
The output is here: https://github.com/abentkamp/lean4/actions/runs/6196384753/job/16822920883

@Sebastian Ullrich: What would it take to merge this into master? I am aware that the setup is not very clean yet, but we also shouldn't lose the progress we made. The big problems are:

• The native 32bit throws random segfaults, which is why I have to run make || true several times.
• The Github Action is not integrated into matrix setup of the Lean CI because it does not proceed in the way it's supposed to. I first run native 32bit to get the oleans, then a wasm build for stage0 only.

Are 50min CI time (on GitHub Servers) acceptable?

[Sebastian Ullrich]

Awesome! We should definitely fix the segfaults first though :) . And instead of recompiling stage 0 to emcc, I really hope we can move that to stage 1 in order to get close to the standard pipeline

[Rujia Liu]

I think the 32bit build is faulty, as some tests failed already. The most obvious one is an arithmetic overflow that I should be able to fix (but don't have time now). Some other failing tests might need help, but could also be a good exercise for myself :)

[Sebastian Ullrich]

There is no inherent reason this setup should be slower to compile than other platforms, is there? It should speed up when the ccache is warm

[Rujia Liu]

I don't understand why is it so slow. In my machine a fresh wasm32 build is about 2~3 min (after 32-bit olean is built). Is github's CI job forced to be single-threaded? I'm not familiar with github CI at all. But anyway it should take similar time as native 64-bit build.

[Alexander Bentkamp]

There is this message in the beginning:

Failed to find ccache, prepare for longer and redundant builds...

[Rujia Liu]

Ouch, I never noticed that ccache is so effective... I built too many times and forgot how long the first one took... Only remembered that later ones are quick :)

[Alexander Bentkamp]

Ok, looking at the tests sounds like a good approach.
Test 307 fails because #eval INT32_MIN / -2 yields -1073741824 instead of 1073741824. Why would that happen?

[Rujia Liu]

Yeah, I'm planning to look at this tomorrow :)

[Alexander Bentkamp]

Maybe leanruntest_listtostring.lean is actually more interesting because it is actually causing a segfault.

[Alexander Bentkamp]

This is the gdb stack trace, but it does not help me much :-)

(gdb) run ../../tests/lean/run/listtostring.lean
Starting program: /home/alex/Projects/test/lean4/build/release/stage0/bin/lean ../../tests/lean/run/listtostring.lean
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Program received signal SIGSEGV, Segmentation fault.
0xf7613d07 in lean_inc (o=0x9d517858) at /home/alex/Projects/test/lean4/build/release/stage0/include/lean/lean.h:449
449     static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); }
(gdb) bt
#0  0xf7613d07 in lean_inc (o=0x9d517858) at /home/alex/Projects/test/lean4/build/release/stage0/include/lean/lean.h:449
#1  0xf7614d5f in lean::inc (o=0x9d517858) at /home/alex/Projects/test/lean4/stage0/src/runtime/object.h:54
#2  0xf7616dfb in lean::object_ref::object_ref (this=0x56649a9c, s=...) at /home/alex/Projects/test/lean4/stage0/src/runtime/object_ref.h:22
#3  0xf761562b in lean::name::name (this=0x56649a9c, other=...) at /home/alex/Projects/test/lean4/stage0/src/util/name.h:76
#4  0xf77dd2a4 in lean::ir::interpreter::frame::frame (this=0x56649a9c, mFn=..., mArgBp=6173, mJpBp=0) at /home/alex/Projects/test/lean4/stage0/src/library/compiler/ir_interpreter.cpp:339
#5  0xf77dd267 in __gnu_cxx::new_allocator<lean::ir::interpreter::frame>::construct<lean::ir::interpreter::frame, lean::name const&, unsigned int&, unsigned int> (this=0xffff5c78,
    __p=0x56649a9c, __args=@0xff90b1a4: 0, __args=@0xff90b1a4: 0, __args=@0xff90b1a4: 0) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/ext/new_allocator.h:162
#6  0xf77dce5b in std::allocator_traits<std::allocator<lean::ir::interpreter::frame> >::construct<lean::ir::interpreter::frame, lean::name const&, unsigned int&, unsigned int> (__a=...,
    __p=0x56649a9c, __args=@0xff90b1a4: 0, __args=@0xff90b1a4: 0, __args=@0xff90b1a4: 0) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/alloc_traits.h:516
#7  0xf77dcd2f in std::vector<lean::ir::interpreter::frame, std::allocator<lean::ir::interpreter::frame> >::emplace_back<lean::name const&, unsigned int&, unsigned int> (this=0xffff5c78,
    __args=@0xff90b1a4: 0, __args=@0xff90b1a4: 0, __args=@0xff90b1a4: 0) at /usr/bin/../lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/vector.tcc:115
#8  0xf77d99dd in lean::ir::interpreter::push_frame (this=0xffff5c60, d=..., arg_bp=6173) at /home/alex/Projects/test/lean4/stage0/src/library/compiler/ir_interpreter.cpp:744
#9  0xf77e19d2 in lean::ir::interpreter::call (this=0xffff5c60, fn=..., args=...) at /home/alex/Projects/test/lean4/stage0/src/library/compiler/ir_interpreter.cpp:878

[Rujia Liu]

I'm not sure if it's essentially the same thing, but when debugging 307.lean with Visual Studio, it got an assertion failed:

static inline lean_obj_res lean_int_to_nat(lean_obj_arg a) {
    assert(!lean_int_lt(a, lean_box(0)));
    if (lean_is_scalar(a)) {
        return a;
    } else {
        return lean_big_int_to_nat(a);
    }
}

I don't understand the code, but is it possible that some of thesize_ts inside the lean_box function should actually be uint64 instead? @Sebastian Ullrich

[Rujia Liu]

Leaving the office now... will continue tomorrow :)

[Rujia Liu]

I just tried listtostring.lean in debug mode, it doesn't seem to terminate (but didn't crash). I waited 2 minutes I think

[Rujia Liu]

Oops, as soon as I come back to my PC, I gotStackoverflow detected. Aborting.

[Rujia Liu]

Really leaving now :)

[Alexander Bentkamp]

Ok, I think the box/unboxing mechanism can explain why #eval INT32_MIN / -2 yields the wrong result. As I understand it, box will shift all bits to the left and add a one at the end to mark the resulting lean object as a scalar. unbox will take such a scalar lean object and shift all bits back to the right to yield the original value. With 64 bit, boxing and unboxing an integer (32bit) is no big deal. There is lots of space to shift into. On 32bit however, boxing and unboxing will erase the first bit of the integer.

[Alexander Bentkamp]

Well, it's defintely more complicated than what I wrote above, but might be related to this.

[Alexander Bentkamp]

Okay, I found the issue that causes #eval INT32_MIN / -2 to fail. The constant LEAN_MAX_SMALL_INT was too large by one. The integer 1 << 30 uses all 32 bits. If you shift it left and then right (during boxing/unboxing), the left-most bit will become a 1. Here is a fix:
https://github.com/abentkamp/lean4/commit/24634b130ce153796764937d6cf106919d8481e1

[Alexander Bentkamp]

Unfortunately, the segfaults are still there.

[Schrodinger ZHU Yifan]

Do we have a -m32 pipeline to run these tests？

[Rujia Liu]

Ok, great. I hope I'll find sometime to tackle this segfault. Do you have any pointers to some docs about how IR interpreter works? My current knowledge about lean4 is too poor... @Alexander Bentkamp

[Rujia Liu]

Schrodinger ZHU Yifan said:

Do we have a -m32 pipeline to run these tests？

You mean github CI job? Current it doesn't build 32-bit binary (and that's what we're currently working on)

[Rujia Liu]

You can try this if you want to run 32-bit tests. @Schrodinger ZHU Yifan

Alexander Bentkamp said:

I've written a GitHub action that can reproduce Rujia Liu 's achievement: https://github.com/abentkamp/lean4/blob/wasm-experiments/.github/workflows/wasm.yml
The output is here: https://github.com/abentkamp/lean4/actions/runs/6196384753/job/16822920883

[Rujia Liu]

Some progress: the problematic line is #eval toString (List.range 100000).toArray which got stack overflow. First I realized that I forgot the manually increase the stack size, which is required on Windows. I set it to 512MB and 32-bit binary passed the test. However, 64-bit binary failed. I increased the stack size to 1GB and it passed the test too. It's a bit surprising that this program requires such a big stack... Anyway, it looks like the program itself is ok, maybe on linux the stack size is set differently in 32/64 bit system?

[Rujia Liu]

I've skimmed over my remaining 32-bit failing tests: updateExprIssue, csimpAttr, unhygienicCode. It looks like all are caused by stdout and stderr "unsynchornized". If we only compare data sent to stdout or stderr, Expected and produced are identical. However, the combined .expected.out and .produced.out are mixing stdout/stderr output in two different ways. But maybe it only occurs in msys2 because even my vs2022 build cannot reproduce this. So I don't have many things I can easily do now.

Which other tests are failing in your local machine? @Alexander Bentkamp

[Alexander Bentkamp]

I added a test run to CI: https://github.com/abentkamp/lean4/actions/runs/6206411798/job/16850644397

[Alexander Bentkamp]

@Rujia Liu How exactly do you increase the stack size?

[Rujia Liu]

I'm using MSVC, so I opened project property dialog, in Linker/System, changed both Stack Reserve Size and Stack Commit Size. But since you're using linux, this won't work for you. You need to use ulimit? In the current test code, it uses ulimit -s 2048 I think. And later I found it seems to use considerably less stack in release, but didn't measure.

[Rujia Liu]

I also changed the constant used inget_stack_size in stackinfo.cpp to make sure it returns the same size as I set in the dialog, but in linux it uses getrlimit so it should work automatically.

[Alexander Bentkamp]

Hm, increasing ulimit does not seem to help

[Rujia Liu]

Does #eval toString (List.range 10).toArray crash?

[Alexander Bentkamp]

No, for small numbers, it works

[Alexander Bentkamp]

I guess tests/compiler/StackOverflow.lean is also relevant here. It also leads to a segfault, when it should actually report stack overflow.

[Alexander Bentkamp]

stack overflow detection seems not to work

[Rujia Liu]

I disabled the detection with emscripten but in native 32-bit it is not. Or I made a mistake and always disabled it? And if you can kindly provide a Dockerfile that bulid/test everything, I can play with it more easily. I forgot how to write Dockerfile for a long time (but remembers how to use it)

[Alexander Bentkamp]

This seems to work:

FROM ubuntu:latest
WORKDIR /lean4
COPY . .

RUN apt-get update
RUN apt-get install -y clang ccache cmake gcc-multilib g++-multilib


RUN mkdir -p build/release
WORKDIR build/release

RUN rm -rf *
RUN cmake ../.. -DSTAGE0_CMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DCMAKE_C_COMPILER_WORKS=1 -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_C_COMPILER=clang
RUN make -j4 || true
RUN make -j4 || true
RUN make -j4 || true
RUN make -j4 || true
RUN make -j4 || true
RUN make -j4 || true
RUN make -j4 || true
RUN make -j4
RUN make -j4 test || true

It assumes to be put into the lean4 root directory

[Rujia Liu]

Thanks! Let me try

[Schrodinger ZHU Yifan]

Since this is related to portability, I think lean is somehow doing the same “bad” thing as rust by assuming size_t should be able to hold pointers. This is not the case on some emerging architectures (https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-947.pdf). I am not sure how rust deals it actually, their provenance API doc is actually aware of such architectures.

[Rujia Liu]

Thank you @Schrodinger ZHU Yifan , I'm not aware of such architectures. In fact I've just helped porting another programming language implementation in rust, to 32-bit, by changing some memory layout and a few usize to u64, which is just as "bad"... Any link to the provenance API are you talking about? I've missed that.

[Schrodinger ZHU Yifan]

FYI, https://github.com/rust-lang/rust/issues/95228, rust is introducing the concept of provenance to restrict the legal operations on pointer arithmetics and casting.

[Rujia Liu]

Thank you!

[Alexander Bentkamp]

Quite a few of the tests seem to fail because of this:

/usr/bin/ld: skipping incompatible /home/alex/Projects/test/lean4/build/release/stage1/lib/lean/libleancpp.a when searching for -lleancpp
/usr/bin/ld: cannot find -lleancpp: No such file or directory
/usr/bin/ld: skipping incompatible /home/alex/Projects/test/lean4/build/release/stage1/lib/lean/libLean.a when searching for -lLean
/usr/bin/ld: cannot find -lLean: No such file or directory
clang: error: linker command failed with exit code 1 (use -v to see invocation)
Failed to compile C file bigctor.lean.c

I am guessing clang is accidentally called for 64bit somewhere...

[Alexander Bentkamp]

Ok, I fixed this issue: https://github.com/abentkamp/lean4/commit/48b6aa673673861f5fc0c2bf675b28d0fa769b4b

[Alexander Bentkamp]

The segfault seems to occur on any lean program that runs long enough (maybe ~2000 instructions), called via lean --run. And it occurs completely nondeterministically, sometimes earlier, sometimes later. @Sebastian Ullrich Which parts of Lean would show this nondeterministic behavior? I have already tried disabling the small object allocator, but that did not help.

[Sebastian Ullrich]

I have no idea I'm afraid. There shouldn't be any nondeterminism by default I would have thought.

[Alexander Bentkamp]

I think I have made some progress. valgrind gives me reliably the same error:

==327284== 2 errors in context 1 of 1:
==327284== Invalid read of size 4
==327284==    at 0x5BA30CA: l_Array_forInUnsafe_loop___at_Lean_importModulesCore___spec__1___lambda__1 (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x5BA40C2: l_Array_forInUnsafe_loop___at_Lean_importModulesCore___spec__1___lambda__2 (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x5BA4484: l_Array_forInUnsafe_loop___at_Lean_importModulesCore___spec__1 (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x5BA2E19: l_Lean_importModulesCore (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x5BA4B10: l_Lean_importModulesCore___boxed (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x8485689: lean_apply_2 (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x5B8A6C5: l_Lean_ImportStateM_run___rarg (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x84837DA: lean_apply_1 (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x577CAB4: l_EStateM_bind___rarg (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x84837DA: lean_apply_1 (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x6E37C1C: l_Lean_withImporting___rarg (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x5BAB0C3: l_Lean_importModules___lambda__2___boxed (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x8485647: lean_apply_2 (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x84837DA: lean_apply_1 (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x6DBA913: l_Lean_profileitIOUnsafe___rarg___lambda__1 (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x6DBAA60: l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x84837F7: lean_apply_1 (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x8393B4A: lean_profileit (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x6DBAB00: l_Lean_profileitIOUnsafe___rarg (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==    by 0x5BAB2B5: lean_import_modules (in /home/alex/Projects/lean4/build/release/stage1/lib/lean/libleanshared.so)
==327284==  Address 0x45f3dd5056e0f198 is not stack'd, malloc'd or (recently) free'd
==327284==

[Sebastian Ullrich]

And you're running it on compatible .oleans? I've lost track of what the current setup is

[Alexander Bentkamp]

The setup is simply

cmake ../.. -DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32 -g' -DSTAGE0_LEANC_OPTS='-m32 -g' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32 -g' -DLEANC_OPTS='-m32 -g' -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_C_COMPILER=clang

But I need to run make a couple of times because the segfaults occur randomly while building oleans.

[Alexander Bentkamp]

So yes, the oleans should be compatible.

[Sebastian Ullrich]

Yes, that looks good so far. One thing worth trying is to use the address sanitizer like we do in CI https://github.com/leanprover/lean4/blob/e6fe3bee71f359c866a29766f774864577099778/.github/workflows/ci.yml#L132

[Sebastian Ullrich]

And just to be sure, it might be good to replace the mmap() call with NULL for now

[Alexander Bentkamp]

where is the mmap call?

[Alexander Bentkamp]

I added the santize options:

cmake ../.. -DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF \
-DSTAGE0_LEANC_OPTS='-m32 -g' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang \
-DUSE_GMP=OFF  -DCMAKE_CXX_COMPILER=clang++ \
-DCMAKE_C_COMPILER=clang \
-DLEAN_EXTRA_CXX_FLAGS='-m32 -g -fsanitize=address,undefined'\
-DLEANC_EXTRA_FLAGS='-m32 -g -fsanitize=address,undefined -fsanitize-link-c++-runtime'\
-DSMALL_ALLOCATOR=OFF\
-DBSYMBOLIC=OFF\
-DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32 -g -fsanitize=address,undefined'\
-DSTAGE0_LEANC_EXTRA_FLAGS='-m32 -g -fsanitize=address,undefined -fsanitize-link-c++-runtime'\
-DSTAGE0_SMALL_ALLOCATOR=OFF\
-DSTAGE0_BSYMBOLIC=OFF

Now I get:

/usr/bin/ld: skipping incompatible /home/alex/Projects/test/lean4/build/release/stage0/lib/lean/libleancpp.a when searching for -lleancpp
/usr/bin/ld: cannot find -lleancpp: No such file or directory

[Alexander Bentkamp]

Oh, I see, you mean this mmap call:

#ifndef LEAN_EMSCRIPTEN
         buffer = static_cast<char *>(mmap(base_addr, size, PROT_READ, MAP_PRIVATE, fd, 0));
#endif

[Alexander Bentkamp]

Ok, removing mmap fixed something, but not everything.

[Alexander Bentkamp]

The test tests/compiler/StackOverflow.lean that I have been using to reproduce the segfault now passes reliably.

[Alexander Bentkamp]

During the build, there are still segfaults though.

[Sebastian Ullrich]

Mmh, I guess that's progress? Looks like there's cross-compilation troubles with the sanitizers, too bad

[Alexander Bentkamp]

There are still some failing tests, but none due to Segfault. That will make it harder to debug :-)

[Alexander Bentkamp]

I can reproduce the segfault that occurs during build, but it is very rare:

for i in {1..1000}; do  /home/alex/Projects/test/lean4/build/release/stage0/bin/lean -DwarningAsError=true -o "../build/release/stage1/lib/lean/Lean/Elab/Structure.olean" -i "../build/release/stage1/lib/lean/Lean/Elab/Structure.ilean" --c="../build/release/stage1/lib/temp/Lean/Elab/Structure.c.tmp" Lean/Elab/Structure.lean ; done

[Alexander Bentkamp]

although I run it 1000 times, I get only a few segfaults.

[Alexander Bentkamp]

Lean/Elab/Structure is not the only file that works, but not all files show this behavior.

[Mauricio Collares]

Does rr support recording in this context?

[Alexander Bentkamp]

Sounds good, I should try that

[Alexander Bentkamp]

By running valgrind again and again, I finally got a segfault:

==650680== Memcheck, a memory error detector
==650680== Copyright (C) 2002-2022, and GNU GPL'd, by Julian Seward et al.
==650680== Using Valgrind-3.21.0 and LibVEX; rerun with -h for copyright info
==650680== Command: /home/alex/Projects/test/lean4/build/release/stage0/bin/lean Lean/Elab/Structure.lean
==650680==
==650680== Stack overflow in thread #1: can't grow stack to 0xfed07000
==650680== Stack overflow in thread #1: can't grow stack to 0xfed07000
==650680==
==650680== Process terminating with default action of signal 11 (SIGSEGV)
==650680==  Access not within mapped region at address 0xFED07FF8
==650680== Stack overflow in thread #1: can't grow stack to 0xfed07000
==650680==    at 0x73D0C52: l___private_Lean_Meta_InferType_0__Lean_Meta_inferMVarType (../stdlib//Lean/Meta/InferType.c:5127)
==650680==  If you believe this happened as a result of a stack
==650680==  overflow in your program's main thread (unlikely but
==650680==  possible), you can try to increase the size of the
==650680==  main thread stack using the --main-stacksize= flag.
==650680==  The main thread stack size used in this run was 8388608.
==650680==
==650680== HEAP SUMMARY:
==650680==     in use at exit: 39,344,475 bytes in 517,937 blocks
==650680==   total heap usage: 1,899,263 allocs, 1,381,326 frees, 80,871,924 bytes allocated
==650680==
==650680== LEAK SUMMARY:
==650680==    definitely lost: 229 bytes in 11 blocks
==650680==    indirectly lost: 1,060 bytes in 20 blocks
==650680==      possibly lost: 0 bytes in 0 blocks
==650680==    still reachable: 39,343,186 bytes in 517,906 blocks
==650680==                       of which reachable via heuristic:
==650680==                         newarray           : 11,406,059 bytes in 473,016 blocks
==650680==         suppressed: 0 bytes in 0 blocks
==650680== Rerun with --leak-check=full to see details of leaked memory
==650680==
==650680== For lists of detected and suppressed errors, rerun with: -s
==650680== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
Segmentation fault

[Alexander Bentkamp]

It doesn't tell me much, though

[Mario Carneiro]

Could this have something to do with the stack colliding into a loaded olean file?

[Sebastian Ullrich]

Ah, I assume you disabled mmap in stage 1 (i.e. src/) only?

[Alexander Bentkamp]

Yes, thanks :-)

[Schrodinger ZHU Yifan]

So 32bit build is working now?

[Alexander Bentkamp]

We'll see tomorrow. Going to sleep now.

[Alexander Bentkamp]

Yes, no more segfaults while building :tada:

[Alexander Bentkamp]

Okay, I've also managed to build the native 32bit binary in stage0 and then wasm in stage1: https://github.com/abentkamp/lean4/actions/runs/6324555224/job/17174289560

[Alexander Bentkamp]

@Sebastian Ullrich I assume you would like me to intergate the ci into the "matrix" of ci.yml? Is there a smart way to test it on my fork?

[Sebastian Ullrich]

Yes please! I think you can push it to your own master as well, but feel free to use the PR for it

[Alexander Bentkamp]

@Sebastian Ullrich I get this error, which I believe is due to the usage of Nix in the CI:

In file included from /home/runner/work/lean4/lean4/stage0/src/library/bin_app.cpp:7:
In file included from /home/runner/work/lean4/lean4/stage0/src/library/bin_app.h:8:
In file included from /home/runner/work/lean4/lean4/stage0/src/kernel/expr.h:8:
In file included from /nix/store/2vwipws2crqcjxfzjyq9rjpk61iqf7pf-gcc-12.3.0/include/c++/12.3.0/algorithm:60:
In file included from /nix/store/2vwipws2crqcjxfzjyq9rjpk61iqf7pf-gcc-12.3.0/include/c++/12.3.0/bits/stl_algobase.h:59:
In file included from /nix/store/2vwipws2crqcjxfzjyq9rjpk61iqf7pf-gcc-12.3.0/include/c++/12.3.0/x86_64-unknown-linux-gnu/bits/c++config.h:655:
In file included from /nix/store/2vwipws2crqcjxfzjyq9rjpk61iqf7pf-gcc-12.3.0/include/c++/12.3.0/x86_64-unknown-linux-gnu/bits/os_defines.h:39:
In file included from /nix/store/i29k9pvl90385mpsavifqvm4rag684dn-glibc-2.37-8-dev/include/features.h:515:
/nix/store/i29k9pvl90385mpsavifqvm4rag684dn-glibc-2.37-8-dev/include/gnu/stubs.h:7:11: fatal error: 'gnu/stubs-32.h' file not found
# include <gnu/stubs-32.h>

Without Nix, I could add the missing 32bit libraries using sudo apt-get install gcc-multilib g++-multilib. I tried nix-env -i glibc_multi, which I believe is the missing package, but it gives me error: selector 'glibc_multi' matches no derivations.

[Schrodinger ZHU Yifan]

You probably want to search some stdEnv variants that support 32bit building.

[Schrodinger ZHU Yifan]

https://nixos.wiki/wiki/Packaging/32bit_Applications

[Schrodinger ZHU Yifan]

yes it is called multiStdenv

[Alexander Bentkamp]

Could you give me a command that I can add to get this stdEnv variant? I don't know anything about nix.

[Schrodinger ZHU Yifan]

Sorry, in that case, I am not sure about lean's infrastructure with nix. My guess is that you need to find something like stdEnv.mkDerivation in current CI configurations and change it accordingly.

[Alexander Bentkamp]

ah, I see. Nix is installed via this Github action: https://github.com/cachix/install-nix-action

[Alexander Bentkamp]

Maybe there is an option for this.

[Sebastian Ullrich]

Feel free to try with apt for now. shell: bash -euxo pipefail {0} should effectively disable Nix for the job

[Alexander Bentkamp]

:+1: Thanks, that is what I was going to do now :)

[Alexander Bentkamp]

@Sebastian Ullrich Would you like a 32bit native build in CI as well?

[Sebastian Ullrich]

You mean as stage 1? I think we only care about 32 bit because of wasm to be honest :)

[Alexander Bentkamp]

ok :-)

[Alexander Bentkamp]

Getting lean --server to run might be trickier than I anticipated. There does not seem to be a straight-forward way to pass messages back and forth between WASM and JS as it is done in the json rpc protocol.

[Patrick Massot]

Wasn't that problem solved in the Lean 3 web editor?

[Schrodinger ZHU Yifan]

I think one can just pass callback for communication? wasm is capable of handling Function

[Wojciech Nawrocki]

Here is the relevant package in lean-client-js.

[Alexander Bentkamp]

@Sebastian Ullrich Is there a mechanism that will convert my avalanche of commits into a single one or should I do that manually?

[Sebastian Ullrich]

git reset? :)

[Alexander Bentkamp]

Ok :-) On mathlib, the bot takes care of that. (At least it did on mathlib 3).

[Sebastian Ullrich]

Oh, if you mean whether we can squash the commits on merge, the answer is yes

[Alexander Bentkamp]

Ok, I squashed them manually now :-)

[Alexander Bentkamp]

@Sebastian Ullrich https://github.com/leanprover/lean4/pull/2599 is ready for review.

[Rujia Liu]

Sorry for being quiet for so long. I was deeply buried in my company work, and congratulations to the PR!

[Alexander Bentkamp]

No problem, thanks for getting the basic build to work in the beginning!

[Rujia Liu]

I'm glad to hear that :)

[Alexander Bentkamp]

@Rujia Liu Could you comment on why leanshared is not working and we need to link Init, Lean and leancpp directly?

[Rujia Liu]

My network doesn't have github access now... I even don't remember I made a such change.

[Rujia Liu]

Could you paste the change here?

[Alexander Bentkamp]

You didn't change anything in the code, but you gave us this follow up command:

"/src/lean4/build/release/stage0/leanc.sh" /src/lean4/build/release/stage0/shell/CMakeFiles/shell.dir/lean.cpp.o -Wl,--whole-archive -lInit -lLean -lleancpp -lleanrt -rdynamic -o /src/lean4/build/release/stage0/bin/lean -s ERROR_ON_UNDEFINED_SYMBOLS=0 -s ASSERTIONS=1 -s WASM=1 -fexceptions -lnodefs.js -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s LLD_REPORT_UNDEFINED=1

[Alexander Bentkamp]

note that it says -lInit -lLean -lleancpp -lleanrt instead of -lleanshared, which is done for other lean builds.

[Rujia Liu]

Ok, I remembered. I copied that command from the console, and changed some parameters. I didn't created that command from scratch. So probably both will work.

[Rujia Liu]

But since that command is different, it should be affected from some emscripten-specific cmake options?

[Rujia Liu]

Anyway, I think the best thing to do is just try the "popular" one, if it works, use it instead :)

[Alexander Bentkamp]

ok :-)

[Alexander Bentkamp]

you might have copied these options from the build command of leanshared itself. For building lean the options you used were not used before.

[Rujia Liu]

Yes, of course. I didn't look very carefully when copying :)

[Alexander Bentkamp]

I just assumed it was crucial because I had some issues with leanshared in my early experiments.

[Alexander Bentkamp]

Okay, I think this is just not possible because leanshared links the C++ std library, but emscripten does not support side modules that link system libraries: https://emscripten.org/docs/compiling/Dynamic-Linking.html#overview-of-dynamic-linking

[Alexander Bentkamp]

It seems that with Emscripten, there are two options for communication between client and server. We can choose either independently for server to client and for client to server messages. One option is stdin/stdout and the other option is direct function calls. The advantage of stdin/stdout is that we should be able to reuse more existing server code. The advantage of direct function calls might be that it's slightly faster if we can avoid encoding each message into a json string.

The Lean3 version seems to use direct calls from client to server and stdout from server to client.

Any opinions?

[Wojciech Nawrocki]

The advantage of direct function calls might be that it's slightly faster if we can avoid encoding each message into a json string.

I would be surprised if this overhead was of any relevance in practice. It is orders of magnitude less work to do this than to elaborate a definition, for example, which the server does every few edits.

[Alexander Bentkamp]

Yeah, I agree. I am wondering why the Lean3 version does not use stdin then. It seems like the way to go.

However, I currently get a "hardware fault" error if I try to wait for input via stdin in Lean code compiled to wasm. But I am fairly confident that this can be fixed.

[Sebastian Ullrich]

Alexander Bentkamp said:

Okay, I think this is just not possible because leanshared links the C++ std library, but emscripten does not support side modules that link system libraries: https://emscripten.org/docs/compiling/Dynamic-Linking.html#overview-of-dynamic-linking

Doesn't that imply that leanshared should be the main module?

[Alexander Bentkamp]

I just assumed that lean would be the main module, but you are right, leanshared should be the main module. Let's see if we can make that work.

[Alexander Bentkamp]

Okay, it seems to be possible, but not easy. Do we really need to link dynamically? What is the benefit?

[Sebastian Ullrich]

It's just a size optimization. If we're not planning to use Lake anyway, it doesn't matter

[Alexander Bentkamp]

@Sebastian Ullrich Any idea why this breaks the windows build?
https://github.com/leanprover/lean4/pull/2599/commits/ff0b8e13f09493923bc38a4e44a6c6dde95fe51d

[Alexander Bentkamp]

Okay, found the issue.

[Alexander Bentkamp]

Yay! Merged into master!

[Alexander Bentkamp]

Now --server... :thinking:

[Alexander Bentkamp]

Any ideas how to solve issue of the Watchdog/FileWorker separation? Probably, I should start with a version of the server that supports only a single file. That should be enough for most if not all use cases.

[Kevin Buzzard]

How far away are we from NNG being usable by 300 people at once? What other big tasks need to be done?

[Alexander Bentkamp]

We can now compile entire files in the browser, but we cannot run the interactive mode of Lean yet. Our current setup of the NNG is that it runs via the interactive editor, so we need the interactive mode to make the game work.

[Patrick Massot]

What is the current size of the wasm build?

[Alexander Bentkamp]

70 MB for the wasm-binary and the emscripten runtime
400 MB ilean+olean of Init+Lean+Lake
all uncompressed

[Schrodinger ZHU Yifan]

That's actually a lot for a web app. Did you try -Os or -DCMAKE_BUILD_TYPE=MinSizeRel?

[Patrick Massot]

This is what I feared. It's great that you're doing all this, but it will probably remain unused until we can get that down to a reasonable size.

[Alexander Bentkamp]

-Os and -DCMAKE_BUILD_TYPE=MinSizeRel does not make a big difference

[Henrik Böving]

To shave some size of, if we dont do multi file there is no reason to ship lake olean and binaries right?

[Henrik Böving]

Init we definitely need to keep...Lean is a bit harder. If you pinky promise to not do meta programming it should just work without Lean oleans though right?

[Alexander Bentkamp]

I didn't count the binary, but yes, then we are at 380MB olean+ilean

[Henrik Böving]

Only taking Lake away or Lake + Lean?

[Alexander Bentkamp]

Only Lake. I hadn't read the message about Lean yet.

[Alexander Bentkamp]

Don't you need Lean to use Tactics? Otherwise, for NNG, we don't need metaprogramming.

[Alexander Bentkamp]

But tar compressed the 380MB become 150MB. And with Mario's compression even less, right?

[Alexander Bentkamp]

Init alone is just 32MB uncompressed.

[Henrik Böving]

Built in tactics are pre compiled into the compiler and I thiiink (this is getting handwavy) it could work out to just run them without Lean oleans.

Mario's stuff is even better but you'd need an additional rust wasm binary to unpack so one would have yo check if the sizd cost pays off here.

Let's try Init only then huh?^^

[Joe Hendrix]

I'm curious what is taking up so much room within the .olean. For example, could one strip out proofs (maybe by introducing axioms instead) and get significantly smaller files?

[Sebastian Ullrich]

About 30% smaller for mathlib: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/olean.20dump.20tool/near/368371297. So it would help, but does not immediately make loading mathlib in wasm feasible.

[Sebastian Ullrich]

@Alexander Bentkamp We really should avoid Lean in NNG and similar games. Which means that these tactics would need to become [builtinTactic] and be compiled into the wasm binary

[Kevin Buzzard]

Note that PRs like #7504 substantially decrease olean file sizes (total mathlib olean file size went down by nearly 5% on #7281 and presumably the same thing is happening with #7504)

[Somo S.]

@Sebastian Ullrich said:

I'm happy to announce https://live.lean-lang.org/, the official online playground for Lean 4 + std/mathlib hosted by the Lean FRO and based on lean4web by Alexander Bentkamp and Jon Eugster. Many thanks to Alex for helping with the setup!

Is this using the wasm build work discussed on this thread? if so, dies this announcement also mean we can now also build our own exe projects to wasm?

[Sebastian Ullrich]

It doesn't, this hasn't changed:

does not immediately make loading mathlib in wasm feasible

[Alexander Bentkamp]

@Somo S. Actually, building your own exe projects to wasm should be possible, even though there is no good setup for this yet. What would you like to build?

[Somo S.]

oh nothing in particular at the moment ... i am just, in general, excited at the prospects of seeing lean4 among the growing list of languages that support wasm/wasi as we approach wasi-preview2

[Alexander Bentkamp]

Okay, I am starting to understand why lean3 wasm did not use stdin. Apparently, Emscripten does not support waiting for stdin: https://github.com/emscripten-core/emscripten/issues/17800. There is a workaround using Asyncify. I am not sure how much overhead that adds.

[Alexander Bentkamp]

A basic version of a web assembly web editor is working:
https://abentkamp.github.io/lean-wasm/index.html#code=universe%20u%0A%0A%40%5Binline%5D%20def%20id%20%7B%CE%B1%20%3A%20Sort%20u%7D%20(a%20%3A%20%CE%B1)%20%3A%20%CE%B1%20%3A%3D%20a%0A%0A%23check%20id
I haven't taken care of the oleans yet. So it only works with Lean in "prelude mode", i.e. Lean doesn't even know about Nat etc.

[James Gallicchio]

frankly it's cool enough to hit restart server and watch my computer's CPU usage go up :-)

[Sebastian Ullrich]

@Alexander Bentkamp That's awesome! What did you use for inter"process" communication in the end? Did you encounter further stumbling blocks on the way?

[Alexander Bentkamp]

I don't use the Watchdog at all and modified the FileWorker a bit:
https://github.com/abentkamp/lean4/blob/wasm-server/src/Lean/Server/FileWorker.lean#L473
It additionally sends out server capabilities the initialized notification. So this will only work to handle a single file.

[Alexander Bentkamp]

We'll have to see how to integrate this into the codebase later.

[Alexander Bentkamp]

And as I mentioned above, Emscripten does not seem capable of wainting for stdin. So I replaced the c++ implementation of Handle.read with a call to a JavaScript function that waits for input:
https://github.com/abentkamp/lean4/blob/wasm-server/src/runtime/io.cpp#L313-L332

[Alexander Bentkamp]

When adding the oleans and import Init, I get

could not find native implementation of external declaration 'UInt64.ofNatCore' (symbols 'l_UInt64_ofNatCore___boxed' or 'l_UInt64_ofNatCore')

Caused by the line

syntax:1024 (name := coeNotation) "↑" term:1024 : term

in Init/Coe.lean.
Any ideas?

[Sebastian Ullrich]

Either the symbol is not in the binary or wasm dlsym somehow misbehaves

[Alexander Bentkamp]

Thanks, problem solved. It stupidly removed -s MAIN_MODULE=1 thinking that it was no longer needed. Apparently it's crucial for dlsym :-).

[Alexander Bentkamp]

It works:
https://abentkamp.github.io/lean-wasm/index.html#code=%23check%20Nat
(make sure to clear your cache to get the new version...)

[Alexander Bentkamp]

To be able to wait for stdin, I use Asyncify, which apparently is not compatible with fwasm-exceptions. So every exception call will have some overhead. I think @Wojciech Nawrocki mentioned that exceptions are used extensively in the server implementation? Would it be worth to explore ways to avoid Asyncify?

[Sebastian Ullrich]

C++ exceptions should be rare, it's okay if they are slower

[Wojciech Nawrocki]

They are used extensively in the kernel; the server is all Lean, so no exceptions there (only Lean's own Except, but that doesn't need stack unwinding).

[Alexander Bentkamp]

Okay, but doesn't the server use the kernel as well?

[Alexander Bentkamp]

On another note: I've noticed that my current setup does not allow for changes of the imports because that will cause the FileWorker to terminate the process.

[Wojciech Nawrocki]

Alexander Bentkamp said:

Okay, but doesn't the server use the kernel as well?

Ah yeah, I guess what Sebastian is saying is that this is fine since there aren't that many exceptions flying around relative to all the other work the server is doing.

[Wojciech Nawrocki]

Alexander Bentkamp said:

On another note: I've noticed that my current setup does not allow for changes of the imports because that will cause the FileWorker to terminate the process.

The file worker code assumes that its entire process will be shutdown and restarted whenever the imports change. If they change without restarting, afaicr the worker will exit with an error code.

[Alexander Bentkamp]

Hm, ok. I guess it won't be easy to get something working for wasm without having too much code duplication.

[Alexander Bentkamp]

I think it's time to rethink why we would like to have a wasm version of Lean. I just discussed with @Jon Eugster and we finally came to the conclusion that it's actually not that useful. Both for the web editor and the games, the current server solution seems to work fine.

[Sebastian Ullrich]

I think for the games, being able to easily rehost and remix them is a plus, though not a terribly important one. For the editor I agree.

[Somo S.]

@Alexander Bentkamp said:

.. we finally came to the conclusion that it's actually not that useful.

is a corollary to this that it's also not useful for users to (eventually) be able to target wasm for any executable they are building (thinking post wasi-previews) or is that a separate matter altogether which could still be considered in future?

[Scott Morrison]

Oh, I'm surprised! I was thinking in terms of "live" documentation and online blueprints, where you can have side by side natural language proofs and the ability to jump into proof states, or get tooltips showing types, etc, in an HTML document.

[Sebastian Ullrich]

I was thinking about that as well but I guess the question is, do you need it to be interactive/editable? What you have listed is more or less covered by LeanInk

[Sebastian Ullrich]

@Somo S. That seems like a separate matter altogether

[Scott Morrison]

I worry that although the server solution is good enough for a demo web editor and an "officially supported" game or two, without a pure JS solution we cut off most external innovation in these directions. Hosting a server is a big barrier to entry.

[Scott Morrison]

Of course, officially supporting WASM is a big commitment!

[Sebastian Ullrich]

I won't deny that it would be very cool to be able to jump into any Lean GitHub project and start editing: https://code.visualstudio.com/blogs/2023/06/05/vscode-wasm-wasi. Whether that can ever be scaled up to Mathlib sizes, I don't know.

[Mario Carneiro]

Well, as one data point, we were able to do it in lean 3 :/ I think lean 4 is being way less resource-conscious than lean 3 (for a variety of reasons) and this is coming back to bite us

[Mario Carneiro]

(That's not entirely true, lean 3 also had issues shipping mathlib toward the end.)

[Mario Carneiro]

but my impression is that the resource issues have meant that instead of being able to ship 80% of mathlib we can now barely ship 10% and full mathlib looks hopelessly out of reach

[Eric Wieser]

Mario Carneiro said:

(That's not entirely true, lean 3 also had issues shipping mathlib toward the end.)

For more context; these issues were due to a 100Mb limit on the deployment mechanism we were using, which we resolved by switching to a different mechanism. I think the offending bundle is now 118 Mb

[Alexander Bentkamp]

@Somo S. The lean4game server is currently an executable that is separate from the official lean server. So if we want to get wasm games, we'd have to find a way to compile a Lean project (that is not Lean itself) to wasm.

[Alexander Bentkamp]

Scott Morrison said:

I worry that although the server solution is good enough for a demo web editor and an "officially supported" game or two, without a pure JS solution we cut off most external innovation in these directions. Hosting a server is a big barrier to entry.

We would like to lower the barrier to entry by offering to import games from Github to our server without our explicit approval. So anybody would be easily be able to publish a game.

[Alexander Bentkamp]

Still, I agree that having an option to set up a wasm game would give users much more control. Also, considering that we will not be able to maintain the game server as actively as now forever, wasm might be a good idea.

[Alexander Bentkamp]

For more context; these issues were due to a 100Mb limit on the deployment mechanism we were using, which we resolved by switching to a different mechanism. I think the offending bundle is now 118 Mb

So we are really just limited by the patience of the user to download huge files, right?

[Wojciech Nawrocki]

Scott Morrison said:

Oh, I'm surprised! I was thinking in terms of "live" documentation and online blueprints, where you can have side by side natural language proofs and the ability to jump into proof states, or get tooltips showing types, etc, in an HTML document.

This is quite far down the road, but support for WASM would be great for writing widgets natively in Lean!

[Kevin Buzzard]

No wasm means we can't have a million people playing NNG at the same time when I drop the new OG season, right?

[Alexander Bentkamp]

@Sebastian Ullrich Would it be possible to publish the wasm build in Lean releases (I mean here: https://github.com/leanprover/lean4/releases)? Then I could more easily link against the libraries when building lean4game(or other projects) for wasm.

[Sebastian Ullrich]

Absolutely, we basically just have to set release: truein the config (and check that all relevant files are included). We should also add it as, presumably, a Tier 2 platform in doc/setup.md

[ZHAO Jiecheng]

Kevin Buzzard said:

No wasm means we can't have a million people playing NNG at the same time when I drop the new OG season, right?

Maybe you can upload it to Steam. :stuck_out_tongue_wink:

[Kevin Buzzard]

Can I make it an executable?

[ZHAO Jiecheng]

(deleted)

[ZHAO Jiecheng]

Kevin Buzzard said:

Can I make it an executable?

I guess, you can. Though it might be a large package that wrap everything in it. But since a typical game often requires several gigabytes of storage space. I don't think it matters.

[Kyle Miller]

Alexander Bentkamp said:

I think it's time to rethink why we would like to have a wasm version of Lean [...] we finally came to the conclusion that it's actually not that useful

Does this mean Lean itself compiled to wasm? If Lean itself isn't compiled to wasm, would it still possible to compile Lean code to wasm? Something I've been looking forward to is rewriting a bunch of pure javascript knot theory computations in Lean, proving they're correct, and then targeting wasm.

[Somo S.]

Somo S. said:

Alexander Bentkamp said:

.. we finally came to the conclusion that it's actually not that useful.

is a corollary to this that it's also not useful for users to (eventually) be able to target wasm for any executable they are building (thinking post wasi-previews) or is that a separate matter altogether which could still be considered in future?

@Kyle Miller i had asked a similar question above.. looks like the talk here is just about the lean executable.

[Alexander Bentkamp]

@Kyle Miller @Somo S. I am already compiling Lean code to wasm that is not Lean itself. Starting with the next release of Lean, the Lean wasm build will be part of the release. At that point, I'll be able to share my current setup more easily.

[Alexander Bentkamp]

Oh, I see the first wasm release is out :-)

[Alexander Bentkamp]

So here is how you can compile Lean to WASM. Any tips on how to integrate this better with lake/elan are very welcome.

Create a new Lean project:

mkdir wasmtest
cd wasmtest
lake init wasmtest

Download the WASM release:

mkdir -p toolchains
wget -P toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_wasm32.tar.zst
tar --use-compress-program=unzstd -xvf toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst -C toolchains

Compile the project using the same toolchain as the wasm build:

echo "leanprover/lean4:v4.3.0-rc2" > ./lean-toolchain
lake build

We are only interested in the c files produced by lake.

Add a output directory for wasm

mkdir -p .lake/build/wasm

Compile to wasm. (Make sure emcc is installed: https://emscripten.org/docs/getting_started/downloads.html)

emcc -o .lake/build/wasm/main.js -I toolchains/lean-4.3.0-rc2-linux_wasm32/include -L toolchains/lean-4.3.0-rc2-linux_wasm32/lib/lean \
  $(find .lake/build/ir -name *.c) -lInit -lLean -lleancpp -lleanrt \
  -sFORCE_FILESYSTEM -lnodefs.js -s EXIT_RUNTIME=0 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto

You can play around with the options here. This is what I use for lean4game.

Test it using node:

node .lake/build/wasm/main.js

[Sebastian Ullrich]

Putting all of these steps in a lakefile in order to automate them would sound like a great first step to me :big_smile:

[Alexander Bentkamp]

Here is what I am wondering specifically:

• Can I install the wasm build via elan instead of downloading it via wget?
• Can I instruct lake to build only the c files?

[Sebastian Ullrich]

Unfortunately elan is not set up for handling multiple architectures, it's probably better to handle this in Lake(files) than extending elan. There should be a facet for the .c files.

[Scott Morrison]

> node .lake/build/wasm/main.js

Hello, world!

Awesome.

[Scott Morrison]

(I needed to change $(find .lake/build/ir -name *.c) to $(find .lake/build/ir -name "*.c").)

[Scott Morrison]

We're going to get lake js, right?

[Graham Leach-Krouse]

I threw together an experimental flake based on the above. Seems to work! In case anyone would like to try it out:

mkdir wasm-lean
cd wasm-lean
nix flake init -t github:gleachkr/wasm-lean
nix build .#js

[Mac Malone]

I love to see a Lake target for the WASM build! :smiling_face_with_hearts: @Alexander Bentkamp Is this meant to be alternative for a binary executable or for a static or shared library? If just an executable would it be desirable to have a separate configuration (i.e., a lean_js alalean_exe) or do we want to be able to build a JS version of any Lean library, module, and/or executable?

[Alexander Bentkamp]

I suspect that an executable would be enough for most people.

For my ongoing work on lean4game I have some other requirements (not crucial that lake supports these, though...):

• I want to load oleans from wasm, so I need to compile them for 32bit. I use the native 32bit build because wasm is a bit slow.
• My main file is written in C and only then it calls exported Lean functions.

[Thea Brick]

I wrote a quick utility to download the necessary toolchain and run all of the steps above https://github.com/T-Brick/lean2wasm