Merge pull request #149 from stanford-centaur/frontend/distil

doc: Set `ignore_values = False` by default

Author: lenianiva

doc/goal.ipynb

@@ -494,7 +494,7 @@
     "def f : Nat -> Nat := sorry\n",
     "theorem property (n : Nat) : f n = n + 1 := sorry\n",
     "\"\"\"\n",
-    "target, = await server.load_sorry_async(sketch)\n",
+       "target, = await server.load_sorry_async(sketch, ignore_values=True)\n",
     "print(target.goal_state)"
    ]
   },

pantograph/server.py

@@ -564,7 +564,7 @@ async def load_sorry_async(
             self,
             src: str,
             binder_name: Optional[str] = None,
-            ignore_values: bool = True) -> list[SearchTarget]:
+            ignore_values: bool = False) -> list[SearchTarget]:
         """
         Condense search target into goals
         """

pantograph/test_server.py

@@ -268,7 +268,7 @@ def test_load_definitions(self):
 
     def test_load_sorry(self):
         server = Server()
-        unit, = server.load_sorry("theorem mystery (p: Prop) : p → p := sorry", ignore_values=False)
+        unit, = server.load_sorry("theorem mystery (p: Prop) : p → p := sorry")
         #self.assertIsNotNone(unit.goal_state, f"{unit.messages}")
         state0 = unit.goal_state
         self.assertEqual(state0.goals, [
@@ -301,7 +301,7 @@ def test_load_sorry(self):
 
     def test_distil_search_target(self):
         server = Server()
-        unit, = server.load_sorry("theorem mystery (p: Prop) : p → p := sorry")
+        unit, = server.load_sorry("theorem mystery (p: Prop) : p → p := sorry", ignore_values = True)
         state0 = unit.goal_state
         self.assertEqual(state0.goals, [
             Goal(