Lean backend

.gitignore

@@ -21,6 +21,9 @@ src/dist/
 **/RocqMakefile
 **/RocqMakefile.conf
 **/.RocqMakefile.d
+**/CoqMakefile
+**/CoqMakefile.conf
+**/.CoqMakefile.d
 **/.lia.cache
 *.aux
 **/.coqdeps.d
@@ -31,5 +34,12 @@ doc/book
 # direnv
 .direnv/
 
+# lean
+**/.lake/
+**/lake-manifest.json
+**/lean-toolchain
+
 *~
 *#
+
+*.DS_Store

Makefile

@@ -73,6 +73,15 @@ $(rocq-examples):
 	make -C $@ clean
 	make -C $@
 
+
+lean-examples = tests/lean/amm tests/lean/ERC20
+
+.PHONY: test-lean $(lean-examples)
+test-lean: compiler $(lean-examples)
+$(lean-examples):
+	make -C $@ clean
+	make -C $@
+
 test-parse: parser compiler $(parser_pass:=.parse.pass) $(parser_fail:=.parse.fail)
 test-type: parser compiler $(typing_pass:=.type.pass) $(typing_fail:=.type.fail)
 test-invariant: parser compiler $(invariant_pass:=.invariant.pass) $(invariant_fail:=.invariant.fail)

act.cabal

@@ -64,6 +64,7 @@ library
     Act.Lex
     Act.Parse
     Act.Rocq
+    Act.Lean
     Act.Syntax
     Act.Syntax.Untyped
     Act.Syntax.Typed

doc/src/SUMMARY.md

@@ -22,7 +22,8 @@
 # Verification with act 
 
 - [hevm backend: Equivalence to EVM bytecode](./equiv.md)
-- [Rocq backend](./rocq.md) 
+- [Rocq backend](./rocq.md)
+- [Lean backend](./lean.md)