From 014fc51d291188afd405c33a8281fbb5013ad304 Mon Sep 17 00:00:00 2001 From: Raito Bezarius Date: Mon, 25 Mar 2024 21:09:26 +0100 Subject: Initial extraction Signed-off-by: Raito Bezarius --- lakefile.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 lakefile.lean (limited to 'lakefile.lean') diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..f92b653 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,19 @@ +import Lake +open Lake DSL + +require base from git + "https://github.com/AeneasVerif/aeneas"@"main"/"backends/lean" + +package «AvlVerification» where + -- add package configuration options here + +lean_lib «AvlVerification» where + -- add library configuration options here + +@[default_target] +lean_exe «avlverification» where + root := `Main + -- Enables the use of the Lean interpreter by the executable (e.g., + -- `runFrontend`) at the expense of increased binary size on Linux. + -- Remove this line if you do not need such functionality. + supportInterpreter := true -- cgit v1.2.3