Prototype compiler for the Lustre language. References:
- A Formally Verified Compiler for Lustre
- Mechanized semantics and verified compilation for a dataflow synchronous language with reset
- Weaving Synchronous Reactions into the Fabric of SSA-form Compilers
- Verified Lustre Normalization with Node Subsampling
This project is written in Haskell and thus depends on GHC and Cabal which can be installed using GHCup.
After cloning this repository you can run:
$ git submodule update --init
$ cabal v2-build all
$ cabal v2-exec lustre-compiler -- -v3 --prog=examples/test2.lus --log=dbg.log
Writing logs to HOME/lustre-compiler/dbg.log.
Writing C code to HOME/lustre-compiler/examples/test2.lus.compiled/test2.c.
Copyright (c) 2025, Chaitanya Koparkar
All rights reserved.