Init LeanCopilot` failed / Building LeanCopilot.Tactics issue #125
Comments
|
I get similar |
|
The problem seems to be here https://github.com/lean-dojo/LeanCopilot/blob/main/LeanCopilot/Tactics.lean#L55 and here https://github.com/lean-dojo/LeanCopilot/blob/main/LeanCopilot/Tactics.lean#L124 but as a noob I have no idea what it is telling me. |
|
I've run into the same problem trying to get started with LeanCopilot today. |
|
Thank you for the report! This particular issue was due to an update (slight restructuring) in part of Lean's Batteries. The resulting bug has been fixed in PR #129, which however is not merged for now due to another observed (probably unrelated) issue also introduced by breaking changes in recent release of Lean. The related issue to that is #127. Further updates will be discussed there. Thanks again. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I've run into the following error when trying to import LeanCopilot v1.6.0 into a project. I've used a previous versions of Lean/LeanCopilot in a past project with no issues on the same machine. The error occurs when building LeanCopilot.Tactics.
Init LeanCopilot` failed:
.... normal looking output here ...
✖ [526/535] Building LeanCopilot.Tactics
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/build/lib:/home/alh/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/lib/lean:/home/alh/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/lib:././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib /home/alh/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/lean --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libctranslate2.so ././.lake/packages/LeanCopilot/././LeanCopilot/Tactics.lean -R ././.lake/packages/LeanCopilot/./. -o ././.lake/packages/LeanCopilot/.lake/build/lib/LeanCopilot/Tactics.olean -i ././.lake/packages/LeanCopilot/.lake/build/lib/LeanCopilot/Tactics.ilean -c ././.lake/packages/LeanCopilot/.lake/build/ir/LeanCopilot/Tactics.c --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Url-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-Download-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libModelCheckpointManager-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Native-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-ByT5-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Builtin-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Interface-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-External-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Generic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-FFI-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Attr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-CodeAction-Deprecated-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Alias-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-AssocList-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Classes-SatisfiesM-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Monadic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-SeqFocus-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Nat-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-ForInStep-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Init-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-List-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-WF-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-HashMap-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-Registry-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Models-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Options-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-MLList-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Tactic-Lint-Misc-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Control-Nondet-Basic-1.so --load-dynlib=././.lake/packages/LeanCopilot/.lake/build/lib/libLeanCopilot-Frontend-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Nanos-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Init-Lemmas-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Basic-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-Array-Merge-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-UnorderedArraySet-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Lean-Expr-1.so --load-dynlib=././.lake/packages/batteries/.lake/build/lib/libBatteries-Data-String-Basic-1.so --load-dynlib=././.lake/packages/aesop/.lake/build/lib/libAesop-Util-Basic-1.so --json
error: ././.lake/packages/LeanCopilot/././LeanCopilot/Tactics.lean:48:30: unknown constant 'String.Matcher.ofString'
error: ././.lake/packages/LeanCopilot/././LeanCopilot/Tactics.lean:54:54: invalid field notation, type is not of the form (C ...) where C is a constant
theoremNameMatcher
has type
?m.4235 state nm model suggestions __do_lift✝¹ declName
error: ././.lake/packages/LeanCopilot/././LeanCopilot/Tactics.lean:55:6: failed to synthesize
Decidable (isSelfReference ∨ isAesop = true)
Additional diagnostic information may be available using the
set_option diagnostics truecommand.error: ././.lake/packages/LeanCopilot/././LeanCopilot/Tactics.lean:124:0: invalid occurrence of universe level 'u_1' at 'LeanCopilot._aux_LeanCopilot_Tactics___elabRules_LeanCopilot_tacticSuggest_tactics__1', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
suggestTactics.{u_1} (TSyntax.getString pfx)
at declaration body
fun (x : Syntax) =>
let_fun __discr : Syntax := x;
if __discr.isOfKind
LeanCopilot.tacticSuggest_tactics_ = true then let_fun __discr_1 : Syntax := __discr.getArg 0; let_fun __discr_2 : Syntax := __discr.getArg 1; bif false || __discr_2.isOfKindstr thenlet_fun pfx : TSyntax `str := { raw := __discr_2 };
let_fun tac : Syntax := __discr_1;
do
let __discr ← Aesop.time (suggestTactics pfx.getString)
match __discr with
| (tacticsWithScores, elapsed) => do
let __do_lift ← isVerbose
let __do_jp : Unit → TacticM Unit := fun (y : Unit) =>
let tactics : Array String := Array.map (fun (x : String × Float) => x.fst) tacticsWithScores;
do
let __do_lift ← isVerbose
let __do_jp : Unit → TacticM Unit := fun (y : Unit) =>
let range : String.Range := { start := tac.getRange?.get!.start, stop := pfx.raw.getRange?.get!.stop };
let ref : Syntax := Syntax.ofRange range;
do
let __do_lift ← liftM SuggestTactics.checkTactics
hint ref tactics __do_lift
if __do_lift = true then do
let y ←
logInfo ((MessageData.ofFormat ∘ format) (toString "Tactics: " ++ toString tactics ++ toString ""))
__do_jp y
else do
let y ← pure PUnit.unit
__do_jp y
if __do_lift = true then do
let y ←
logInfo
((MessageData.ofFormat ∘ format)
(toString "" ++ toString elapsed.printAsMillis ++ toString " for generating " ++
toString tacticsWithScores.size ++
toString " tactics"))
__do_jp y
else do
let y ← pure PUnit.unit
__do_jp y
else
let_fun __discr : Syntax := __discr.getArg 1;
throwUnsupportedSyntax
else
let_fun __discr : Syntax := x;
throwUnsupportedSyntax
error: Lean exited with code 1
Some required builds logged failures:
error: build failed
The text was updated successfully, but these errors were encountered: