Merge pull request #153 from stanford-centaur/version/v0.3.8

fix: Documentation and upstream bugs

Author: lenianiva

doc/setup.md

@@ -29,7 +29,12 @@ server = Server()
 
 The server created from `Server()` is sufficient for basic theorem proving tasks
 reliant on Lean's `Init` library. Some users may find this insufficient and want
-to use non-builtin libraries such as Aesop or Mathlib4.
+to use non-builtin libraries such as Aesop or Mathlib4. In this case, feed in a
+list of module names via the `imports` parameter e.g. `imports=["Mathlib"]`. Due
+to inherent restrictions in Lean, importing a module that has not been imported
+before after the server has already started is not allowed and will trigger
+initializer exceptions. It may be possible to circumvent this if Lean relaxes
+this constraint.
 
 To use external Lean dependencies such as
 [Mathlib4](https://github.com/leanprover-community/mathlib4), Pantograph relies

pantograph/test_server.py

@@ -289,7 +289,7 @@ def test_load_sorry(self):
         state0 = unit.goal_state
         self.assertEqual(state0.goals, [
             Goal(
-                "_uniq.3",
+                "_uniq.5",
                 [Variable(name="p", t="Prop")],
                 target="p → p",
             ),
@@ -301,15 +301,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.17",
+                "_uniq.19",
                 [Variable(name="p", t="Prop")],
                 target="p ∨ p",
             ),
             Goal(
-                "_uniq.19",
+                "_uniq.21",
                 [
                     Variable(name="p", t="Prop"),
-                    Variable(name="h1", t="p ∨ p", v="?m.17"),
+                    Variable(name="h1", t="p ∨ p", v="?m.19"),
                 ],
                 target="p → p",
             ),
@@ -321,7 +321,7 @@ def test_distil_search_target(self):
         state0 = unit.goal_state
         self.assertEqual(state0.goals, [
             Goal(
-                "_uniq.1",
+                "_uniq.3",
                 [],
                 target="∀ (p : Prop), p → p",
             ),