Merge pull request #139 from stanford-centaur/version/v0.3.7

chore: Update to version v0.3.7

Author: lenianiva

.gitmodules

@@ -1,4 +1,4 @@
 [submodule "src"]
 	path = src
 	url = https://github.com/leanprover/Pantograph.git
-	branch = fixed/v4.21.0
+	branch = dev

examples/Example/lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
+   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
+   "rev": "e96b5eca4fcfe2e0e96a1511a6cd5747515aba82",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.21.0",
+   "inputRev": "v4.22.0-rc4",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Example",

examples/Example/lakefile.lean

@@ -2,7 +2,7 @@ import Lake
 open Lake DSL
 
 require aesop from git
-  "https://github.com/leanprover-community/aesop.git" @ "v4.21.0"
+  "https://github.com/leanprover-community/aesop.git" @ "v4.22.0"
 
 package Example
 

pantograph/server.py

@@ -478,7 +478,7 @@ async def goal_load_async(self, path: str) -> GoalState:
 
     goal_load = to_sync(goal_load_async)
 
-    async def tactic_invocations_async(self, file_name: Union[str, Path]) -> List[CompilationUnit]:
+    async def tactic_invocations_async(self, file_name: Union[str, Path]) -> list[CompilationUnit]:
         """
         Collect tactic invocation points in file, and return them.
         """
@@ -638,7 +638,7 @@ def test_version(self):
         """
         NOTE: Update this after upstream updates.
         """
-        self.assertEqual(get_version(), "0.3.6")
+        self.assertEqual(get_version(), "0.3.7")
 
     def test_server_init_del(self):
         import warnings
@@ -755,12 +755,12 @@ def test_have(self):
         state1 = server.goal_tactic(state0, tactic=TacticHave(branch="2 = 1 + 1", binder_name="h"))
         self.assertEqual(state1.goals, [
             Goal(
-                "_uniq.257",
+                "_uniq.255",
                 variables=[],
                 target="2 = 1 + 1",
             ),
             Goal(
-                "_uniq.259",
+                "_uniq.257",
                 variables=[Variable(name="h", t="2 = 1 + 1")],
                 target="1 + 1 = 2",
             ),
@@ -772,13 +772,13 @@ def test_let(self):
             state0, tactic=TacticLet(branch="2 = 1 + 1", binder_name="h"))
         self.assertEqual(state1.goals, [
             Goal(
-                "_uniq.257",
+                "_uniq.255",
                 variables=[],
                 name="h",
                 target="2 = 1 + 1",
             ),
             Goal(
-                "_uniq.259",
+                "_uniq.257",
                 variables=[Variable(name="h", t="2 = 1 + 1", v="?h")],
                 target="1 + 1 = 2",
             ),
@@ -798,13 +798,13 @@ def test_conv_calc(self):
         state2 = server.goal_tactic(state1b, "1 + a + 1 = a + 1 + 1")
         self.assertEqual(state2.goals, [
             Goal(
-                "_uniq.381",
+                "_uniq.372",
                 variables,
                 target="1 + a + 1 = a + 1 + 1",
                 name='calc',
             ),
             Goal(
-                "_uniq.400",
+                "_uniq.391",
                 variables,
                 target="a + 1 + 1 = a + b",
                 mode=TacticMode.CALC,
@@ -916,15 +916,15 @@ def test_load_sorry(self):
         state1b = server.goal_tactic(state0, tactic=TacticDraft("by\nhave h1 : Or p p := sorry\nsorry"))
         self.assertEqual(state1b.goals, [
             Goal(
-                "_uniq.16",
+                "_uniq.17",
                 [Variable(name="p", t="Prop")],
                 target="p ∨ p",
             ),
             Goal(
-                "_uniq.18",
+                "_uniq.19",
                 [
                     Variable(name="p", t="Prop"),
-                    Variable(name="h1", t="p ∨ p"),
+                    Variable(name="h1", t="p ∨ p", v="?m.17"),
                 ],
                 target="p → p",
             ),