initial commit

anoma · Dec 12, 2024 · 710b4fe · 710b4fe
1 parent 7f0ea7f
commit 710b4fe
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 6 deletions.
diff --git a/Juvix.lean b/Juvix.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Juvix` library.
+-- Import modules here that should be built as part of the library.
+import Juvix.Basic
diff --git a/JuvixLean/Basic.lean → Juvix/Basic.lean b/JuvixLean/Basic.lean → Juvix/Basic.lean
diff --git a/JuvixLean.lean b/JuvixLean.lean
diff --git a/README.md b/README.md
@@ -1 +1,7 @@
-# juvix-lean
+# Juvix Lean formalization library
+
+The Juvix Lean library provides primitives for verifying the correctness of Juvix compiler runs, i.e., proving that the semantics of a particular Juvix program is preserved by the compilation process.
+
+The major components of the library include:
+- formalization of Juvix compiler internal representations and their semantics,
+- proof-producing metaprograms for verifying that individual Juvix compiler transformations preserve the semantics.
diff --git a/lakefile.toml b/lakefile.toml
@@ -1,7 +1,7 @@
 name = "juvix-lean"
 version = "0.1.0"
 keywords = ["math"]
-defaultTargets = ["JuvixLean"]
+defaultTargets = ["Juvix"]
 
 [leanOptions]
 pp.unicode.fun = true # pretty-prints `fun a ↦ b`
@@ -12,4 +12,4 @@ name = "mathlib"
 scope = "leanprover-community"
 
 [[lean_lib]]
-name = "JuvixLean"
+name = "Juvix"