adding a new backend (JS, Elixir)

Stream: general

[TongKe Xue]

I have recently been learning Lean4 via the excellent Game Server ( https://www.youtube.com/@TongKeXue/videos ) and the excellent https://lean-lang.org/functional_programming_in_lean/ .

I am interested in understanding what needs to be modified at https://github.com/leanprover/lean4/blob/master/src/Lean/Compiler/IR/EmitC.lean to have Lean emit JS.

The end goal being:

1. write core JS logic in lean; emit JS code as something esbuild can process
2. link lean-js-output w/ js libraries
3. we can now do JS dev in dependently-typed lean

My questions are:

1. what are the general steps for adding a new backend (just for local dev) ?
2. after cp EmitC.lean EmitJS.lean, what steps can I do to get a *.js output file (that contains C code) ?
3. EmitC.lean is only 800 loc, so translation should not be too bad; are there any high level invariants / contracts I need to be aware of ?

Thanks!

[Arthur Paulino]

Note that it as a (very likely long) chain of 6 imports, so the 800 LOC is illusory:

public import Lean.Compiler.NameMangling
public import Lean.Compiler.IR.EmitUtil
public import Lean.Compiler.IR.NormIds
public import Lean.Compiler.IR.SimpCase
public import Lean.Compiler.IR.Boxing
public import Lean.Compiler.ModPkgExt

[Arthur Paulino]

I'd try a different approach. I'd tackle it from the higher level by using Lean 4 more closely to how it's meant to be used, via metaprogramming.

[TongKe Xue]

Arthur Paulino said:

I'd try a different approach. I'd tackle it from the higher level by using Lean 4 more closely to how it's meant to be used, via metaprogramming.

I don't understand the idea you have in mind. Can you point me at documentation / sample code / tutorial that does what you have in mind ?

Thanks!

[Eric Wieser]

In the past there was work to use emscripten to compile C to js, but it suffered from the sheer size of all the Olean files

[TongKe Xue]

I am currently testing out a different approach of "foobar.lean -> foobar.c -> manually link it via FFI (wasm in JS case)"

Currently, I have this:

cat foobar.lean; lean foobar.lean -c foobar.c; clang foobar.c
def main : IO Unit := IO.println "Hello, world!"

foobar.c:4:10: fatal error: 'lean/lean.h' file not found
    4 | #include <lean/lean.h>
      |          ^~~~~~~~~~~~~
1 error generated.

What is the correct (i.e. not hardcoding) way to get the path for where lean.h is stored and the corresponding liblean.so we're going to have to link against?

[Arthur Paulino]

TongKe Xue said:

Arthur Paulino said:

I'd try a different approach. I'd tackle it from the higher level by using Lean 4 more closely to how it's meant to be used, via metaprogramming.

I don't understand the idea you have in mind. Can you point me at documentation / sample code / tutorial that does what you have in mind ?

Thanks!

Unfortunately I don't know any minimally well documented example of this. But here's a starter with a few hints:

import Lean

elab "#compile" n:ident : command => do
  -- Here we're in `CommandElabM`, which gives us access to the
  -- current environment
  let stt ← get
  let constants : Lean.ConstMap := stt.env.constants
  -- You can ctrl+click on `Lean.ConstMap` above to inspect it.

  -- `CommandElabM` also gives you access to `IO` so you can, for example, write
  -- data to your file system. E.g., when writing some generated source on your
  -- target language (JS or any other).
  IO.println "hi"

  -- `n` allows you to get the corresponding `Lean.Name`, which can be used t
  -- retrieve the target constant you want to compile
  match constants.find? n.getId with
  | none => throw (.error n "Not found in environment") -- You can also throw errors
  | some (constant : Lean.ConstantInfo) =>
    -- You can inspect `Lean.ConstantInfo` by ctrl+clicking on it
    -- From here, you can do anything with `constant` and `constants` at hand
    -- I'll just print a boolean that confirms it's a definition
    IO.println constant.isDefinition

def myMain (x y : UInt64) : UInt64 :=
  x + y

#compile myMain
-- hi
-- true

From the metaprogramming layer you have way more control than you'd have on highly processed code.

[TongKe Xue]

1. Thank you for the minimal example.
2. I have it running locally.

The reason I was originally looking at the EmitC layer was that I was:

1. I wanted to deal with something with all the proofs removed.
2. Besides "refcount 1 on shared structure == we can overwrite in place", I thought the C -> JS conversion would mainly be syntactical, i.e. changing C syntax to JS syntax. I've since realized this is probably false, as the emitted C code includes "lean/lean.h" and needs to be linked vs some "lean runtime lib", which JS does not have. (Unless we emscriptsen the C Lean runtime to wasm.)

I'm looking at your approach above -- and please correct me if I'm wrong -- we're basically getting it at the AST level right? Which means (1) we need to remove the proof ourselves, (2) we need to run our own optimization passes [which I believe there are a few before emitting C].

Again, I'm new to this codebase; please let me know if I'm getting things wrong. Thanks!

[Arthur Paulino]

TongKe Xue said:

I'm looking at your approach above -- and please correct me if I'm wrong -- we're basically getting it at the AST level right? Which means (1) we need to remove the proof ourselves, (2) we need to run our own optimization passes [which I believe there are a few before emitting C].

It's not as raw as an AST. It's already elaborated, with all meta variables filled. But you're right in thinking that you'd need to remove proofs manually and you'd need to implement your own optimizations.

But there's no need to deal with C stuff, like linking etc. It's your compiler and you're in control.

[TongKe Xue]

Two separate followups to this

I can build a lean program 'manually' via

lean foobar.lean -c foobar.c
clang foobar.c -I`lean --print-prefix`/include -L`lean --print-libdir` -lleanshared

Two followups

1. is it possible to build this so the output is wasm32 instead of x86_64 ? I'm not trying to run entire lean4 server in Chrome/wasm32, I just want to run particular programs (written in lean4) in Chrome/wasm32

2. is the generated x86_64 code multi thread safe? [i.e. I want to write it in an erlang/beam https://www.erlang.org/doc/system/nif.html , and call it from Elixir]

The end goal here is to have an app running in Chrome/wasm32 talking to an x86_64 linux server, and have it "sorta" verified in lean4. [i.e. we verify core logic in lean4, then make assumptions about websockets + included libraries]

Thanks!