bump toolchain

Author: durant42040

lean_dojo_v2/external_api/LeanCopilot/Frontend.lean

@@ -29,11 +29,11 @@ def suggestion (tac : String) (msgs : MessageLog := {}) : TacticM Suggestion :=
       let e ← g.withContext do (PrettyPrinter.ppExpr goalType)
       str := str ++ Format.pretty ("\n⊢ " ++ e)
     pure (some str)
-  let style? := if goals.isEmpty then some .success else none
+  let style? := none
   let msg? ← msgs.toList.findM? fun m => do pure <|
     m.severity == MessageSeverity.information && (← m.data.toString).startsWith "Try this: "
   let suggestion ← match msg? with
-  | some m => pure <| SuggestionText.string (((← m.data.toString).drop 10).takeWhile (· != '\n'))
+  | some m => pure <| SuggestionText.string (((← m.data.toString).drop 10).takeWhile (· != '\n')).toString
   | none => pure <| SuggestionText.string tac
   return { suggestion, postInfo?, style? }
 

lean_dojo_v2/external_api/LeanCopilot/Models/External.lean

@@ -74,15 +74,15 @@ def ExternalGenerator.generate (model : ExternalGenerator) (input : String) (tar
   return res.outputs.map fun g => (g.output, g.score)
 
 
-def generateRunpod (input : String) (modelName : String) (targetPrefix : String) : IO $ Array (String × Float) := do
+def generateRunpod (input : String) (modelName : String) (_targetPrefix : String) : IO $ Array (String × Float) := do
   let url := "https://router.huggingface.co/v1/chat/completions"
-  
+
   -- Format the prompt (same as Python pre_process_input)
   let prompt := if modelName == "deepseek" then
     s!"Here is a theorem you need to prove in Lean:```lean\n{input}```\nNow you should suggest exactly one line tactic in lean code. Only output the tactic, no explanation, no comments, no theorem, nothing else:"
   else
     input
-  
+
   -- Build JSON payload
   let message := Json.mkObj [("role", Json.str "user"), ("content", Json.str prompt)]
   let messages := Json.arr #[message]
@@ -95,38 +95,38 @@ def generateRunpod (input : String) (modelName : String) (targetPrefix : String)
     ("n", Json.num 4)
   ]
   let reqStr := reqJson.pretty 99999999999999999
-  
+
   -- Read HF_TOKEN from .env file in current directory
   let envFile := ".env"
   let envContent ← IO.FS.readFile envFile
   let lines := envContent.splitOn "\n"
   let mut token := ""
   for line in lines do
     if line.startsWith "HF_TOKEN=" then
-      token := line.drop 9  -- Remove "HF_TOKEN=" prefix
+      token := (line.drop 9).toString  -- Remove "HF_TOKEN=" prefix
   if token == "" then
     throw $ IO.userError "HF_TOKEN not found in .env file. Please create a .env file with: HF_TOKEN=your_token_here"
-  
+
   -- Make API call
   let out ← IO.Process.output {
     cmd := "curl"
     args := #["-X", "POST", url, "-H", "accept: application/json", "-H", "Content-Type: application/json", "-H", s!"Authorization: Bearer {token}", "-d", reqStr]
   }
   if out.exitCode != 0 then
      throw $ IO.userError s!"Request failed. Please check if the API is accessible at `{url}`."
-  
+
   -- Parse response
   let some json := Json.parse out.stdout |>.toOption
     | throw $ IO.userError "Failed to parse response"
-  
+
   -- Debug: print raw response
   IO.println s!"Raw API response: {out.stdout}"
-  
+
   let some choices := json.getObjVal? "choices" |>.toOption
     | throw $ IO.userError "No choices in response"
   let some choicesArray := choices.getArr? |>.toOption
     | throw $ IO.userError "Choices is not an array"
-  
+
   -- Extract and clean responses (same as Python post_process_output)
   let mut results : Array (String × Float) := #[]
   for choice in choicesArray do
@@ -140,19 +140,19 @@ def generateRunpod (input : String) (modelName : String) (targetPrefix : String)
     let cleaned := if modelName == "deepseek" then
       -- Extract content between backticks
       if contentStr.startsWith "`" && contentStr.endsWith "`" then
-        contentStr.drop 1 |>.dropRight 1  -- Remove first and last backtick
+        contentStr.drop 1 |>.dropEnd 1  -- Remove first and last backtick
       else
         contentStr
     else
       contentStr
-    results := results.push (cleaned, 1.0)
-  
+    results := results.push (cleaned.toString, 1.0)
+
   -- Deduplicate (same as Python choices_dedup)
   let mut uniqueData : List (String × Float) := []
   for result in results do
     if !uniqueData.any (·.1 == result.1) then
       uniqueData := uniqueData.append [result]
-  
+
   return uniqueData.toArray
 
 

lean_dojo_v2/external_api/LeanCopilot/Tactics.lean

@@ -16,7 +16,7 @@ def ppTacticState : List MVarId → MetaM String
   | [] => return "no goals"
   | [g] => return (← Meta.ppGoal g).pretty
   | goals =>
-      return (← goals.foldlM (init := "") (fun a b => do return s!"{a}\n\n{(← Meta.ppGoal b).pretty}")).trim
+      return (← goals.foldlM (init := "") (fun a b => do return s!"{a}\n\n{(← Meta.ppGoal b).pretty}")).trimAscii.toString
 
 
 /--
@@ -49,7 +49,7 @@ elab_rules : tactic
   | `(tactic | suggest_tactics_deepseek%$tac $pfx:str) => do
     let tacticsWithScores ← suggestTactics "deepseek" pfx.getString
     let tactics := tacticsWithScores.map (·.1)
-    let range : String.Range := { start := tac.getRange?.get!.start, stop := pfx.raw.getRange?.get!.stop }
+    let range : Lean.Syntax.Range := { start := tac.getRange?.get!.start, stop := pfx.raw.getRange?.get!.stop }
     let ref := Syntax.ofRange range
     hint ref tactics True
 

lean_dojo_v2/external_api/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.27.0-rc1