Ideas about a JS backend

Stream: lean4

[Xubai Wang]

I'm considering writing a javascript backend for lean so that we can write frontend code directly in Lean (e.g. doc-gen4).
The current design I have come up with is to implement a EmitJs.lean (counterpart to Lean.Compiler.IR.EmitC) code generator and lean.mjs (~ lean.h) for all those @[extern] opaque definitions, and then we can compile each *.lean file to *.mjs.

[Xubai Wang]

But I got stuck when I try to reuse the extern attribute

attribute [extern js "thunkPure"] Thunk.pure
-- error: invalid attribute 'extern', declaration is in an imported module

It seems that all ParametricAttribute are restricted to the same module. Will it be more reasonable to place the restriction on specific attributes rather than on the base type?

[Yuri de Wit]

@Xubai Wang are you working on a public repo somewhere?

[Edward Ayers]

@Wojciech Nawrocki I remember you showed me a definition file for the needed Lean JS runtime at some point, but I can't find the link.

[Wojciech Nawrocki]

I think that's lean.h. It contains the Lean intrinsics which any runtime needs to implement.

[Edward Ayers]

lean.h

[Xubai Wang]

@Yuri de Wit Yes. I'm going to write the backend in a lean4 fork: https://github.com/xubaiw/lean4-js/tree/js-backend. But I haven't made any commits yet.

[Xubai Wang]

I wonder how scalar type is identified in lean's c side.

static inline bool lean_is_scalar(lean_object * o) { return ((size_t)(o) & 1) == 1; }
static inline lean_object * lean_box(size_t n) { return (lean_object*)(((size_t)(n) << 1) | 1); }
static inline size_t lean_unbox(lean_object * o) { return (size_t)(o) >> 1; }

It seems that scalar type is just a size_t casted to lean_object* pointer whose last bit is 1. Does this mean that nonscalar lean_object pointer is restricted to be out of the pattern? Is it possible to enforce on a pointer's actual value?

[Sebastian Ullrich]

@Xubai Wang I have trouble parsing your specific questions, but are you aware of https://leanprover.github.io/lean4/doc/dev/ffi.html#translating-types-from-lean-to-c?

[Xubai Wang]

Sorry for my vague expression. I have read about it but still unclear about how it works internally. In other words, why does a Nat pointer have 0 as its lowest bit?

[Xubai Wang]

I'm porting all of these stuff in javascript, so it's just important to figure out the mechanism :D

[Xubai Wang]

I got it. So a scalar type is always boxed on the lean side and always unboxed on the backend side. The backend representation doesn't matter as long as we have a method to decide whether it is a scalar one, right?

[Sebastian Ullrich]

Xubai Wang said:

In other words, why does a Nat pointer have 0 as its lowest bit?

Because lean_object is at least 4-byte aligned (since it starts with an int)

[Sebastian Ullrich]

Xubai Wang said:

So a scalar type is always boxed on the lean side and always unboxed on the backend side

I'm not sure what you mean by that. The use of "scalar type" is also a bit confusing. The IR and runtime know unboxed integer types, and then there is IRType.object, which may be either a tagged "pointer" or a true reference to a lean_object.