Merge pull request #40 from lean-dojo/dev

Constrain tactic suggestion outputs at the high level
lean-dojo · Dec 9, 2023 · b03a0af · b03a0af
2 parents dab02a1 + c5e4aee
commit b03a0af
Show file tree

Hide file tree

Showing 3 changed files with 55 additions and 7 deletions.
diff --git a/LeanCopilot/Models/FFI.lean b/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

diff --git a/LeanCopilot/Tactics.lean b/LeanCopilot/Tactics.lean
@@ -3,7 +3,7 @@ import LeanCopilot.Options
 import LeanCopilot.Frontend
 import Aesop.Util.Basic
 
-open Lean Meta Elab Tactic
+open Lean Meta Elab Term Tactic
 
 set_option autoImplicit false
 
@@ -34,11 +34,18 @@ Generate a list of tactic suggestions.
 -/
 def suggestTactics (targetPrefix : String) : TacticM (Array (String × Float)) := do
  let state ← getPpTacticState
+ let theoremName := match ((← getDeclName?).get!).toString with
+ | "_example" => ""
+ | n => n
  if ← isVerbose then
  logInfo s!"State:\n{state}"
+ logInfo s!"Theorem name:¬{theoremName}"
  let nm ← getGeneratorName
  let model ← getGenerator nm
- generate model state targetPrefix
+ let suggestions ← generate model state targetPrefix
+ let filteredSuggestions := suggestions.filterMap fun ((t, s) : String × Float) =>
+ if (t == theoremName) ∨ (t == "aesop") then none else some (t, s)
+ return filteredSuggestions
 
 
 private def annotatePremise (premisesWithInfoAndScores : String × String × String × Float) : MetaM String := do

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -18,6 +18,51 @@
  "manifestFile": "lake-manifest.json",
  "inputRev": "master",
  "inherited": false,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/xubaiw/CMark.lean",
+ "type": "git",
+ "subDir": null,
+ "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
+ "name": "CMark",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": true,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+ "type": "git",
+ "subDir": null,
+ "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
+ "name": "UnicodeBasic",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": true,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/mhuisi/lean4-cli",
+ "type": "git",
+ "subDir": null,
+ "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+ "name": "Cli",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "nightly",
+ "inherited": true,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/hargonix/LeanInk",
+ "type": "git",
+ "subDir": null,
+ "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
+ "name": "leanInk",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "doc-gen",
+ "inherited": true,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/leanprover/doc-gen4",
+ "type": "git",
+ "subDir": null,
+ "rev": "53ecc225fea834acd7f32b9dc1aed880b79d70b9",
+ "name": "«doc-gen4»",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": false,
  "configFile": "lakefile.lean"}],
  "name": "LeanCopilot",
  "lakeDir": ".lake"}