Build Elan Locally?

Stream: new members

[Andrew Elsey]

Hi, weird question. I'm trying to replicate this: https://galois.com/blog/2021/03/real-time-robotics-control-in-the-lean-language/ . i.e., running an Arduino robot with a Lean4 controller running on a raspberry pi. The issue I'm running into is it looks like there's no elan build for the pi's architecture (searches for an armv7 extension for elan). My brightest idea is to try to build elan locally. Before I go tilting at windmills, I was wondering if there was any documentation on this or if anyone had any experience? Thank you.

[Mario Carneiro]

my understanding is that they used lean 4 to produce C code and then used a C compiler for the target architecture; so lean itself is running on the desktop while the C is compiled or cross-compiled to the arduino

[Andrew Elsey]

It didn't look like that based on these steps:"Run leanmake in the root directory of the repo.

If successful, the binary build/bin/balance-car should exist. " a few lines later... "Build the Lean balance-car binary on the RPi4."

But, if I can actually transpile into C (lean4 does this I guess?), that might actually be an easier way to go about things. Thank you for the tip.