Merge pull request #2 from loganrjmurphy/docker

Add Dockerfile and more instructions
loganrjmurphy · May 29, 2024 · b50829c · b50829c
2 parents 1669056 + 2628d91
commit b50829c
Show file tree

Hide file tree

Showing 9 changed files with 144 additions and 1,424 deletions.
diff --git a/.dockerignore b/.dockerignore
@@ -0,0 +1,5 @@
+.vscode
+tmp
+.lake
+python/__pycache__
+*/.DS_Store
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,4 @@
+Book/All.lean
 /build
 /lake-packages/*
 /.lake/*

diff --git a/AutoFormalization/proof/autoformalize.py b/AutoFormalization/proof/autoformalize.py
@@ -10,7 +10,9 @@
 
 
 def preceding_propositions(idx):
-    with open("AutoFormalization/proof/book_propositions.json", "r", encoding="utf-8") as f:
+    with open(
+        "AutoFormalization/proof/book_propositions.json", "r", encoding="utf-8"
+    ) as f:
         propositions = json.load(f)
     pre_props = []
     for i in range(1, idx):

diff --git a/AutoFormalization/statement/evaluate.py b/AutoFormalization/statement/evaluate.py
@@ -6,6 +6,7 @@
 from E3.checker import Checker
 from E3.utils import ROOT_DIR
 
+
 def main():
     parser = argparse.ArgumentParser()
     parser.add_argument(
@@ -32,14 +33,9 @@ def main():
     )
     parser.add_argument(
         "--mode",
-        choices=[
-            "bvars", 
-            "skipApprox", 
-            "onlyApprox", 
-            "full"
-        ],
+        choices=["bvars", "skipApprox", "onlyApprox", "full"],
         default="skipApprox",
-        help="E3 checker mode"
+        help="E3 checker mode",
     )
     parser.add_argument(
         "--reasoning",
@@ -112,7 +108,7 @@ def main():
                         cnt += 1
                 except Exception as e:
                     print(e)
-                    continue 
+                    continue
 
     print(f"cnt: {cnt}, tot: {tot}, acc: {(cnt/tot)*100:.2f}%")