Merge branch 'main' of https://github.com/lean-dojo/LeanCopilot into …

…main

LeanCopilot/LlmAesop.lean

@@ -1,10 +1,11 @@
 import LeanCopilot.Tactics
 import LeanCopilot.Options
+import Std.Data.String.Basic
 import Aesop
 
 set_option autoImplicit false
 
-open Lean
+open Lean Meta Elab Term Tactic
 
 namespace LeanCopilot
 
@@ -13,7 +14,18 @@ def tacGen : Aesop.TacGen := fun (mvarId : MVarId) => do
  let state ← ppTacticState [mvarId]
  let nm ← SuggestTactics.getGeneratorName
  let model ← getGenerator nm
- generate model state ""
+ let suggestions ← generate model state ""
+ -- A temporary workaround to prevent the tactic from using the current theorem.
+ -- TODO: Use a more pincipled way, e.g., see Lean4Repl.lean in LeanDojo.
+ let theoremName := match (← liftM (m := MetaM) <| Term.TermElabM.run getDeclName?).1.get! |>.toString with
+ | "_example" => ""
+ | n => n
+ let theoremNameMatcher := String.Matcher.ofString theoremName
+ let filteredSuggestions := suggestions.filterMap fun ((t, s) : String × Float) =>
+ let isAesop := t == "aesop"
+ let isSelfReference := ¬ (theoremName == "") ∧ (theoremNameMatcher.find? t |>.isSome)
+ if isSelfReference ∨ isAesop then none else some (t, s)
+ return filteredSuggestions
 
 
 macro "#configure_llm_aesop" : command => `(@[aesop 100%] def tacGen := LeanCopilot.tacGen)

LeanCopilot/Models/FFI.lean

@@ -79,11 +79,7 @@ def generate (model : NativeGenerator) (input : String) (targetPrefix : String)
  let temperature := model.params.temperature
  let tokensWithScores := FFI.generate model.name inputTokens targetPrefixTokens numReturnSequences beamSize minLength maxLength lengthPenalty patience temperature
 
- return tokensWithScores.filterMap fun ((ts, s) : Array String × Float) =>
- match tokenizer.detokenize ts with
- | "aesop" => none
- | t => some (t, s)
-
+ return tokensWithScores.filterMap fun ((ts, s) : Array String × Float) => (tokenizer.detokenize ts, s)
 
 
 instance : TextToText NativeGenerator where

LeanCopilot/Tactics.lean

@@ -2,8 +2,9 @@ import Lean
 import LeanCopilot.Options
 import LeanCopilot.Frontend
 import Aesop.Util.Basic
+import Std.Data.String.Basic
 
-open Lean Meta Elab Tactic
+open Lean Meta Elab Term Tactic
 
 set_option autoImplicit false
 
@@ -34,11 +35,23 @@ Generate a list of tactic suggestions.
 -/
 def suggestTactics (targetPrefix : String) : TacticM (Array (String × Float)) := do
  let state ← getPpTacticState
- if ← isVerbose then
- logInfo s!"State:\n{state}"
  let nm ← getGeneratorName
  let model ← getGenerator nm
- generate model state targetPrefix
+ let suggestions ← generate model state targetPrefix
+ -- A temporary workaround to prevent the tactic from using the current theorem.
+ -- TODO: Use a more pincipled way, e.g., see Lean4Repl.lean in LeanDojo.
+ let theoremName := match (← getDeclName?).get! |>.toString with
+ | "_example" => ""
+ | n => n
+ let theoremNameMatcher := String.Matcher.ofString theoremName
+ if ← isVerbose then
+ logInfo s!"State:\n{state}"
+ logInfo s!"Theorem name:\n{theoremName}"
+ let filteredSuggestions := suggestions.filterMap fun ((t, s) : String × Float) =>
+ let isAesop := t == "aesop"
+ let isSelfReference := ¬ (theoremName == "") ∧ (theoremNameMatcher.find? t |>.isSome)
+ if isSelfReference ∨ isAesop then none else some (t, s)
+ return filteredSuggestions
 
 
 private def annotatePremise (premisesWithInfoAndScores : String × String × String × Float) : MetaM String := do

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
  "type": "git",
  "subDir": null,
- "rev": "baf6defee1fe881ae535519c0776f37f6ef08603",
+ "rev": "b197bd218dbab248ad8899404334d41da04f5d13",
  "name": "std",
  "manifestFile": "lake-manifest.json",
  "inputRev": "main",