Zulip Chat Archive

Stream: new members

Topic: Build Elan Locally?


Andrew Elsey (Apr 23 2021 at 14:58):

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 (Apr 23 2021 at 15:00):

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 (Apr 23 2021 at 15:10):

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.


Last updated: Dec 20 2023 at 11:08 UTC