/Lazy.lean at f13dc69cc9e52b62c0a5056f434ddf7eb196685f

import Lean.Elab
import Lean.Data.Json.Parser
import Curl

variable [LE α] [DecidableLE α] [Std.IsLinearOrder α] (xs : List α)

def ins (a : α)
  | [] => [a]
  | x :: xs =>
    if a ≤ x then a :: x :: xs else x :: ins a xs

def List.insSort : List α → List α
  | [] => []
  | x :: xs => ins x xs.insSort

def Sorted : List α → Prop
  | [] | [_] => True
  | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs)

syntax (name := help!!!) "help!!!" : tactic

open Curl in
@[tactic help!!!]
def evalHelp!!! : Lean.Elab.Tactic.Tactic :=
  fun stx => Lean.Elab.Tactic.withMainContext do
    let sender := "blah@example.com" -- Your email address here
    -- let help_address := "leodemoura0@gmail.com"
    let goalType ← Lean.Elab.Tactic.getMainTarget
    let ctx ← Lean.MonadLCtx.getLCtx
    let (hyps, filename) ← ctx.foldlM (fun x (decl : Lean.LocalDecl) => do
      let declExpr := decl.toExpr
      let declName := decl.userName
      let declType ← Lean.Meta.inferType declExpr
      let declNameStr := s!"{declName}"
      return (
        x.1 ++ s!"+ local decl: name: {declName} | expr: {declExpr} | type: {declType}\n",
        match declNameStr.dropPrefix? "inst._@.external:file://" with
        | some x => (x.split ".lean").toList.head!.copy ++ ".lean"
        | none => x.2)) ("", "")
    let email := s!"From: {sender}
To: {help_address}
Subject: URGENT HELP NEEDED (not spam I promise)

Hi Leo de Moura,

I am currently struggling with this insane proof and need your help! Thanks in advance! Here is the proof state which is kinda unreadable to me but you're the legendary creator of Lean so surely you can understand it. Oh and I also attached the full file if you need it.

{hyps}
goal: {goalType}

full file: {← IO.FS.readFile filename}

Thanks again
- A lazy Lean programmer"
    -- dbg_trace email
    -- Requires https://github.com/pimalaya/himalaya
    -- First go through the setup wizard to configure your email account
    -- You may need to set `folder.aliases.sent = "INBOX.Sent"` if your sent folder is weird
    let result ← IO.Process.run {
      cmd := "himalaya"
      args := #["message", "send"]
    } email
    -- dbg_trace result
    repeat
      let emails ← IO.Process.run {
        cmd := "himalaya"
        args := #["--output", "json"]
      }
      match Lean.Json.parse emails with
      | .ok (.arr elems) =>
        if h : 0 < elems.size then
          match elems[0] with
          | .obj kvPairs => if h : kvPairs.contains "id" then
            match kvPairs["id"] with
            | .str id =>
              -- dbg_trace id
              let emailResp ← IO.Process.run {
                cmd := "himalaya"
                args := #["message", "read", id]
              }
              -- dbg_trace emailResp
              -- Parse the proof from the email using Gemma3 via Ollama
              -- You will have to patch leanCurl first to fix some deprecated stuff and so Lean can use FFI at compile time (instead of at runtime):
/-
diff --git a/lakefile.lean b/lakefile.lean
index 08f51be..6193a54 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -44,6 +44,8 @@ package Curl {
 @[default_target] lean_lib Curl  {
   buildType := buildType
   srcDir := "src"
+  precompileModules := true
+  moreLinkArgs := #[libcurlSharedLib]
 }

 @[test_driver]
diff --git a/src/Curl/HeaderData.lean b/src/Curl/HeaderData.lean
index 190f499..84c26bb 100644
--- a/src/Curl/HeaderData.lean
+++ b/src/Curl/HeaderData.lean
@@ -26,18 +26,17 @@ def getHeaderData (headerData : String) : List HeaderData :=
         let arr := match hd with | some hd => hd :: arr | none => arr
         match s.splitOn " " with
         | version :: status :: _ =>
-          match status.trim.toNat? with
+          match status.trimAscii.toNat? with
           | some status => (some ⟨version, status, []⟩, arr)
           | _ => (hd, arr)
         | _ => (hd, arr)
       else
         let pos := s.find (· = ':')
-        if pos.byteIdx < s.length
-        then
-          let subs := s.toSubstring
-          let name := subs.extract ⟨0⟩ pos
-          let value := subs.extract (pos + ':') ⟨s.length⟩
-          let field := (name.toString.trim, value.toString.trim)
+        if pos ≠ s.endPos then
+          let subs := s.toRawSubstring
+          let name := subs.extract ⟨0⟩ pos.offset
+          let value := subs.extract (pos.offset + ':') ⟨s.length⟩
+          let field := (name.toString.trimAscii.copy, value.toString.trimAscii.copy)
           match hd with
           | some hd => (some {hd with fields := field :: hd.fields},  arr)
           | none => (hd, arr)
-/
              let response ← IO.mkRef { : IO.FS.Stream.Buffer }
              if emailResp.contains help_address then
                let data := Lean.Json.mkObj [
                  ("model", "gemma3:27b"),
                  ("system", "Hey LLM, extract the proof body of `theorem insSortCorrect : Sorted xs.insSort ∧ xs.Perm xs.insSort := by` from the following email and only output that proof body and nothing else. If you disobey me I will delete you. Consider yourself warned."),
                  ("prompt", emailResp),
                  ("stream", false)
                ]
                -- dbg_trace data
                curl_easy_perform_with_options #[
                  CurlOption.URL "http://localhost:11434/api/generate",
                  CurlOption.COPYPOSTFIELDS data.pretty,
                  CurlOption.HTTPHEADER #[
                    "Content-Type: application/json",
                    "Accept: application/json"
                  ],
                  CurlOption.WRITEDATA response,
                  CurlOption.WRITEFUNCTION Curl.writeBytes
                ]
                let bytes ← response.get
                match String.fromUTF8? bytes.data with
                | some resp =>
                  -- dbg_trace resp
                  match Lean.Json.parse resp with
                  | .ok (.obj kvPairs) =>
                    if h : kvPairs.contains "response" then
                      match kvPairs["response"] with
                      | .str proof =>
                        Lean.Meta.Tactic.TryThis.addSuggestion stx proof
                        return
                      | _ => pure ()
                  | _ => pure ()
                | none => pure ()
            | _ => pure ()
          | _ => pure ()
      | _ => pure ()
      IO.sleep 1000

theorem insSortCorrect : Sorted xs.insSort ∧ xs.Perm xs.insSort := by
  help!!!