minor edits

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):

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}%")
 

E3/Engine/choosePerms.py

@@ -6,13 +6,16 @@
 from dataclasses import dataclass, field
 from collections import Counter
 
+
 def is_permutation(list1, list2):
     return Counter(list1) == Counter(list2)
 
+
 SHORTCIRCUIT_THRESHOLD = 4000000
 SHORTCIRCUIT_SAMPLE_THRESHOLD = 0.88
 SHORTCIRCUIT_SAMPLE_CUTOFF = 50
 
+
 class QuantifierData:
     points: list[str]
     lines: list[str]
@@ -23,8 +26,14 @@ def __init__(self, points, lines, circles):
         self.lines = lines
         self.circles = circles
 
-def has_permutation(x:QuantifierData,y:QuantifierData):
-    return is_permutation(x.points, y.points) and is_permutation(x.lines, y.lines) and is_permutation (x.circles, y.circles)
+
+def has_permutation(x: QuantifierData, y: QuantifierData):
+    return (
+        is_permutation(x.points, y.points)
+        and is_permutation(x.lines, y.lines)
+        and is_permutation(x.circles, y.circles)
+    )
+
 
 class PropData:
     univNames: QuantifierData
@@ -33,12 +42,22 @@ class PropData:
     def __init__(self, univNames, existNames):
         self.univNames = univNames
         self.existNames = existNames
-
-    def asList(self):
-        return self.univNames.points + self.univNames.lines + self.univNames.circles + self.existNames.points + self.existNames.lines + self.existNames.circles
 
-def has_match(x : PropData, y : PropData):
-    return has_permutation(x.univNames,y.univNames) and has_permutation(x.existNames, y.existNames)
+    def asList(self):
+        return (
+            self.univNames.points
+            + self.univNames.lines
+            + self.univNames.circles
+            + self.existNames.points
+            + self.existNames.lines
+            + self.existNames.circles
+        )
+
+
+def has_match(x: PropData, y: PropData):
+    return has_permutation(x.univNames, y.univNames) and has_permutation(
+        x.existNames, y.existNames
+    )
 
 
 class PermutationStruct:
@@ -75,7 +94,7 @@ class NameMap:
     sim: float
 
     def __eq__(self, other) -> bool:
-        self.name==other.name
+        self.name == other.name
 
 
 def readNames(data):
@@ -115,7 +134,8 @@ def checkPerm(names, target, reference, guarded):
 
 
 def checkAndInsert(heap, name, N):
-    if name in heap: return ()
+    if name in heap:
+        return ()
     if len(heap) < N:
         heapq.heappush(heap, name)
     else:
@@ -155,48 +175,65 @@ def choosePermutations(
 
     nonempty_names = []
 
-
-    if not univ.noPoints(): nonempty_names+=[univ.pointPerms]
-    if not univ.noLines(): nonempty_names+=[univ.linePerms]
-    if not univ.noCircles(): nonempty_names+=[univ.circlePerms]
-    if not exist.noPoints(): nonempty_names+=[exist.pointPerms]
-    if not exist.noLines(): nonempty_names+=[exist.linePerms]
-    if not exist.noCircles(): nonempty_names+=[exist.circlePerms]
-
+    if not univ.noPoints():
+        nonempty_names += [univ.pointPerms]
+    if not univ.noLines():
+        nonempty_names += [univ.linePerms]
+    if not univ.noCircles():
+        nonempty_names += [univ.circlePerms]
+    if not exist.noPoints():
+        nonempty_names += [exist.pointPerms]
+    if not exist.noLines():
+        nonempty_names += [exist.linePerms]
+    if not exist.noCircles():
+        nonempty_names += [exist.circlePerms]
 
     ceiling = 1
     for x in nonempty_names:
         ceiling *= ceiling * len(x)
-    if ceiling > SHORTCIRCUIT_THRESHOLD :
+    if ceiling > SHORTCIRCUIT_THRESHOLD:
         short_circuiting = True
 
-    if has_match(ground,remove_all_guards(test)):
+    if has_match(ground, remove_all_guards(test)):
         print("match found")
-        sim = checkPerm(ground.asList(), target, reference, replaceGuards(ground.asList()))
+        sim = checkPerm(
+            ground.asList(), target, reference, replaceGuards(ground.asList())
+        )
         checkAndInsert(permHeap, NameMap(ground.asList(), sim), N)
 
     for uPoints, uLines, uCircles, ePoints, eLines, eCircles in allCombs:
         perm = uPoints + uLines + uCircles + ePoints + eLines + eCircles
         sim = checkPerm(asList, target, reference, perm)
         x = NameMap(perm, sim)
         checkAndInsert(permHeap, x, N)
-        if (short_circuiting and sim > SHORTCIRCUIT_SAMPLE_THRESHOLD):
+        if short_circuiting and sim > SHORTCIRCUIT_SAMPLE_THRESHOLD:
             seen_sc += 1
-        if (short_circuiting and seen_sc >= SHORTCIRCUIT_SAMPLE_CUTOFF):
+        if short_circuiting and seen_sc >= SHORTCIRCUIT_SAMPLE_CUTOFF:
             return permHeap, asList
     return permHeap, asList
 
 
 def removeGuards(data):
     return list(map(lambda x: x.replace("grd_", ""), data))
 
+
 def replaceGuards(data):
-    return list(map(lambda x : "grd_"+x,data))
+    return list(map(lambda x: "grd_" + x, data))
+
 
 def remove_all_guards(x: PropData):
-    univ = QuantifierData(removeGuards(x.univNames.points), removeGuards(x.univNames.lines), removeGuards(x.univNames.circles))
-    exist = QuantifierData(removeGuards(x.existNames.points), removeGuards(x.existNames.lines), removeGuards(x.existNames.circles))
-    return PropData(univ,exist)
+    univ = QuantifierData(
+        removeGuards(x.univNames.points),
+        removeGuards(x.univNames.lines),
+        removeGuards(x.univNames.circles),
+    )
+    exist = QuantifierData(
+        removeGuards(x.existNames.points),
+        removeGuards(x.existNames.lines),
+        removeGuards(x.existNames.circles),
+    )
+    return PropData(univ, exist)
+
 
 def main():
 
@@ -229,6 +266,6 @@ def main():
     with open(args.outFile, "w") as file:
         json.dump(dict, file)
 
+
 if __name__ == "__main__":
     main()
-

README.md

@@ -67,6 +67,8 @@ Optionally, you can:
 1. Run `lake -R -Kenv=dev build SystemE:docs` to build the documentation
 1. View the auto-generated documentation locally at ./lake/build/doc, e.g., using `python -mhttp.server`
 
+If you have problems building the project, [Dockerfile](./Dockerfile) and [scripts/build.sh](./scripts/build.sh) may serve as useful references.
+
 
 ## The Formal System E
 

scripts/build.sh

@@ -1,4 +1,5 @@
 #!/bin/bash
+# This script was designed to run on GitHub Codespaces.
 
 # Install elan.
 curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
@@ -18,6 +19,7 @@ cd ../..
 
 pip install smt-portfolio
 
+# Build the Lean project.
 lake script run check
 lake exe cache get
 lake build SystemE Book UniGeo E3