Runtime for Lingua Franca's Lean Target

The reactor-lean library provides the runtime implementation for Lingua Franca's Lean target. It provides primitives for constructing objects of the Reactor model, as well as functions for executing them according to the execution semantics of the Reactor model. Have a look at the Lingua Franca Wiki for an overview of the Reactor model.

Additionally, reactor-lean provides a DSL for declaring reactor-based programs directly in Lean. The DSL is expanded into a complete reactor-based program and thus provides most of the code generation required to use this library.

Requirements

To use this library you need to install Lean 4. The linked instructions will also install Lean's package manager Lake, which we require.

Build Instructions

To building a reactor-based program with this library:

1. Clone this repository.
2. Write the program in Main.lean using reactor-lean's lf-DSL. Note that while this can be done manually, it is intended to be automatically generated by Lingua Franca.
3. Within this repository's directory, run lake update to fetch the dependency Std4.
4. Run lake build.

Lingua Franca Frontend

The parts of Lingua Franca that make use of this library can be found here.