Lean on a RISC-V microcontroller (ESP32-C3)

Stream: lean4

[György Kurucz]

In case anyone is interested, I recently managed to compile Lean programs to a RISC-V microcontroller. (Searching the Zulip, I couldn't find any references to microcontrollers or embedded systems, so AFAICT I am the first one to do this.)

Right now my demo program can read GPIO input, and flash an LED in various patterns. Obviously this is still just an early proof-of-concept, a lot more work would be needed to turn this into something generally usable.

Here is the project repo, and I also have a longer blog article about this project if you are interested in the details.

Notes about my experience doing this:

• My biggest issue was that in the precompiled Init library the initialization code (initialize_Init) is quite big (by embedded standards at least), is anyone aware of a (nice) method to only end up with initialization code for constants that are actually used by the program?

• Runtime: it would be cool to have a lot more #ifdefs to compile away e.g. the checks for all the negative refcounts when threading is disabled, or disable all the library functions that don't have a reasonable implementation in an embedded context (e.g. everything in process.cpp).

• Lake could have better support for cross compilation, e.g. right now it seems that there isn't really support for managing multiple libInit.as or runtimes for different architectures. (Having all the libs as LLVM bitcode could solve the arch issue, but as I mentioned previously you probably want to have a different runtime version for the embedded target.)

• 31 bit integers would be cool, a la OCaml. (But maybe a more general special casing of Fin n could be done? E.g. as long as n <= 2^31 we know that it is always represented as a scalar, no need to check for the general Nat representation.)