Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fails to build #3

Open
idontgetoutmuch opened this issue Sep 22, 2024 · 0 comments
Open

Fails to build #3

idontgetoutmuch opened this issue Sep 22, 2024 · 0 comments

Comments

@idontgetoutmuch
Copy link

stderr:
⚠ [5118/5122] Built LLMlean.API
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:283:46: unused variable `state`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:287:47: unused variable `state`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:367:20: `Lean.HashSet` has been deprecated, use `Std.HashSet` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:367:38: `Lean.HashSet.empty` has been deprecated, use `Std.HashSet.empty` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:385:20: `Lean.HashSet` has been deprecated, use `Std.HashSet` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:385:38: `Lean.HashSet.empty` has been deprecated, use `Std.HashSet.empty` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:403:20: `Lean.HashSet` has been deprecated, use `Std.HashSet` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:403:38: `Lean.HashSet.empty` has been deprecated, use `Std.HashSet.empty` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:440:20: `Lean.HashSet` has been deprecated, use `Std.HashSet` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:440:38: `Lean.HashSet.empty` has been deprecated, use `Std.HashSet.empty` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:459:20: `Lean.HashSet` has been deprecated, use `Std.HashSet` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:459:38: `Lean.HashSet.empty` has been deprecated, use `Std.HashSet.empty` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:477:20: `Lean.HashSet` has been deprecated, use `Std.HashSet` instead
warning: ././.lake/packages/llmlean/././LLMlean/API.lean:477:38: `Lean.HashSet.empty` has been deprecated, use `Std.HashSet.empty` instead
✖ [5119/5122] Building LLMlean.LLMstep
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/llmlean/.lake/build/lib:././.lake/build/lib DYLD_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/mathlib/.lake/build/lib:././.lake/build/lib:/Users/dom/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/lib/lean:/Users/dom/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/lib /Users/dom/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/lean ././.lake/packages/llmlean/././LLMlean/LLMstep.lean -R ././.lake/packages/llmlean/./. -o ././.lake/packages/llmlean/.lake/build/lib/LLMlean/LLMstep.olean -i ././.lake/packages/llmlean/.lake/build/lib/LLMlean/LLMstep.ilean -c ././.lake/packages/llmlean/.lake/build/ir/LLMlean/LLMstep.c --json
error: ././.lake/packages/llmlean/././LLMlean/LLMstep.lean:25:2: unknown attribute [widget]
error: ././.lake/packages/llmlean/././LLMlean/LLMstep.lean:134:6: unknown identifier 'Widget.saveWidgetInfo'
error: ././.lake/packages/llmlean/././LLMlean/LLMstep.lean:122:6: invalid {...} notation, expected type is not known
error: Lean exited with code 1
Some required builds logged failures:
- LLMlean.LLMstep
error: build failed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant