-
Notifications
You must be signed in to change notification settings - Fork 9
Open
Labels
auto-update-lean-failAuto update for Lean dependenciesAuto update for Lean dependencies
Description
Try lake update and then investigate why this update causes the lean build to fail.
Files changed in update:
- lean-toolchain
Build Output
⚠ [17/171] Replayed HumanEvalLean.HumanEval150
warning: HumanEvalLean/HumanEval150.lean:116:2: The `mvcgen` tactic is experimental and still under development. Avoid using it in production projects.
✖ [170/171] Building HumanEvalLean.HumanEval51 (880ms)
trace: .> LEAN_PATH=/home/runner/work/human-eval-lean/human-eval-lean/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-09-19/bin/lean /home/runner/work/human-eval-lean/human-eval-lean/HumanEvalLean/HumanEval51.lean -o /home/runner/work/human-eval-lean/human-eval-lean/.lake/build/lib/lean/HumanEvalLean/HumanEval51.olean -i /home/runner/work/human-eval-lean/human-eval-lean/.lake/build/lib/lean/HumanEvalLean/HumanEval51.ilean -c /home/runner/work/human-eval-lean/human-eval-lean/.lake/build/ir/HumanEvalLean/HumanEval51.c --setup /home/runner/work/human-eval-lean/human-eval-lean/.lake/build/ir/HumanEvalLean/HumanEval51.setup.json --json
error: HumanEvalLean/HumanEval51.lean:31:2: Type mismatch
List.Sublist.filter ?m.2 hst
has type
(List.filter ?m.2 s.toList).Sublist (List.filter ?m.2 t.toList)
but is expected to have type
IsSubseq (_root_.removeVowels s) (_root_.removeVowels t)
error: Lean exited with code 1
Some required targets logged failures:
- HumanEvalLean.HumanEval51
error: build failed
Metadata
Metadata
Assignees
Labels
auto-update-lean-failAuto update for Lean dependenciesAuto update for Lean dependencies