fix(repl): Elaborate with `errToSorry` as false by default

Main.lean

@@ -8,12 +8,6 @@ import Repl
 open Pantograph.Repl
 open Pantograph.Protocol
 
-/-- Print a string to stdout without buffering -/
-def printImmediate (s : String) : IO Unit := do
-  let stdout ← IO.getStdout
-  stdout.putStr (s ++ "\n")
-  stdout.flush
-
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parseCommand (s: String): Except String Command := do
   match s.trim.get? 0 with
@@ -40,27 +34,27 @@ partial def loop : MainM Unit := do repeat do
   | .error error =>
     let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
     -- Using `Lean.Json.compress` here to prevent newline
-    printImmediate error.compress
+    IO.println error.compress
   | .ok command =>
     try
       let ret ← execute command
       let str := match state.options.printJsonPretty with
         | true => ret.pretty
         | false => ret.compress
-      printImmediate str
+      IO.println str
     catch e =>
       let message := e.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
-      printImmediate error.compress
+      IO.println error.compress
 
-def main (args: List String): IO Unit := do
+
+unsafe def main (args: List String): IO Unit := do
   -- NOTE: A more sophisticated scheme of command line argument handling is needed.
   if args == ["--version"] then do
     IO.println s!"{Pantograph.version}"
     return
 
-  unsafe do
-    Pantograph.initSearch ""
+  Pantograph.initSearch ""
 
   -- Separate imports and options
   let (options, imports) := args.partition (·.startsWith "--")
@@ -68,7 +62,7 @@ def main (args: List String): IO Unit := do
   let coreState ← Pantograph.createCoreState imports.toArray
   try
     let mainM := loop.run { coreContext } |>.run' { env := coreState.env }
-    printImmediate "ready."
+    IO.println "ready."
     mainM
   catch ex =>
     let message := ex.toString

Pantograph/Delate.lean

@@ -164,7 +164,7 @@ partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
   self e := instantiateDelayedMVars e
 
 /--
-Convert an expression to an equivalent form with
+Convert an expression to an equiavlent form with
 1. No nested delayed assigned mvars
 2. No aux lemmas or matchers
 3. No assigned mvars

README.md

@@ -81,7 +81,7 @@ the environment might be setup like this:
 ``` sh
 LIB="../lib"
 LIB_MATHLIB="$LIB/mathlib4/.lake"
-export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
 
 LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```

Repl.lean

@@ -81,6 +81,7 @@ def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name
     : EMainM α := do
   let scope := (← get).scope
   let context := {
+    errToSorry := false,
     isNoncomputableSection := scope.isNoncomputable,
   }
   let state := {

doc/rationale.md

@@ -47,12 +47,12 @@ include:
 
 - If a tactic loses track of metavariables, it will not be caught until the end
   of the proof search. This is a bug in the tactic itself.
-- Although a timeout feature exists in Pantograph, it relies on the coöperative
-  multitasking from the tactic implementation. There is nothing preventing a
-  buggy tactic from stalling Lean if it does not check for cancellation often.
+- Timeouts for executing tactics is not available. Maybe this will change in the
+  future.
 - Interceptions of parsing errors generally cannot be turned into goals (e.g.
   `def mystery : Nat := :=`) due to Lean's parsing system.
 
+
 ## References
 
 * [Pantograph Paper](https://arxiv.org/abs/2410.16429)