fix compilation order

reilabs · Jul 26, 2024 · ee887a2 · ee887a2
1 parent ddcadfa
commit ee887a2
Show file tree

Hide file tree

Showing 10 changed files with 10 additions and 9 deletions.
diff --git a/.github/workflows/prover-test.yml b/.github/workflows/prover-test.yml
@@ -74,4 +74,4 @@ jobs:
         run: |
           cd light-prover/formal-verification
           ~/.elan/bin/lake exe cache get
-          ~/.elan/bin/lake build || ~/.elan/bin/lake build
+          ~/.elan/bin/lake build
diff --git a/light-prover/formal-verification/.gitignore b/light-prover/formal-verification/.gitignore
@@ -0,0 +1 @@
+lakefile.olean
diff --git a/light-prover/formal-verification/FormalVerification/Lemmas.lean b/light-prover/formal-verification/FormalVerification/Lemmas.lean
@@ -1,5 +1,5 @@
 import Mathlib
-import ProvenZK
+import «ProvenZk»
 import FormalVerification.Circuit
 
 open LightProver (F Order)

diff --git a/light-prover/formal-verification/FormalVerification/Merkle.lean b/light-prover/formal-verification/FormalVerification/Merkle.lean
@@ -1,4 +1,4 @@
-import ProvenZk
+import «ProvenZk»
 import FormalVerification.Circuit
 import FormalVerification.Lemmas
 import FormalVerification.Rangecheck

diff --git a/light-prover/formal-verification/FormalVerification/Poseidon.lean b/light-prover/formal-verification/FormalVerification/Poseidon.lean
@@ -1,7 +1,7 @@
 import FormalVerification.Circuit
 import FormalVerification.Lemmas
 import Mathlib
-import ProvenZk
+import «ProvenZk»
 
 open LightProver (F Order)
 

diff --git a/light-prover/formal-verification/FormalVerification/RangeTree.lean b/light-prover/formal-verification/FormalVerification/RangeTree.lean
@@ -1,4 +1,4 @@
-import ProvenZK
+import «ProvenZk»
 import FormalVerification.Poseidon
 import FormalVerification.Circuit
 import FormalVerification.Lemmas

diff --git a/light-prover/formal-verification/FormalVerification/Rangecheck.lean b/light-prover/formal-verification/FormalVerification/Rangecheck.lean
@@ -1,4 +1,4 @@
-import ProvenZk
+import «ProvenZk»
 import FormalVerification.Circuit
 import FormalVerification.Lemmas
 

diff --git a/light-prover/formal-verification/Main.lean b/light-prover/formal-verification/Main.lean
@@ -1,4 +1,4 @@
-import ProvenZK
+import «ProvenZk»
 import FormalVerification.Circuit
 import FormalVerification.Lemmas
 import FormalVerification.Merkle

diff --git a/light-prover/formal-verification/lake-manifest.json b/light-prover/formal-verification/lake-manifest.json
@@ -14,7 +14,7 @@
     "subDir?": null,
     "rev": "659b51e94d4c5160c5d93b92323f0d0dda05c3ad",
     "opts": {},
-    "name": "ProvenZK",
+    "name": "«proven-zk»",
     "inputRev?": "v1.4.0",
     "inherited": false}},
   {"git":

diff --git a/light-prover/formal-verification/lakefile.lean b/light-prover/formal-verification/lakefile.lean
@@ -8,7 +8,7 @@ package «formal-verification» {
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"@"v4.2.0"
 
-require ProvenZK from git
+require «proven-zk» from git
   "https://github.com/reilabs/proven-zk.git"@"v1.4.0"
 
 lean_lib FormalVerification {