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.

Sign up for GitHub

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

Jump to bottom

Error message for "Invalid Lake configuration" appears for non-config related errors #6827

Closed
BoltonBailey opened this issue Jan 28, 2025 · 0 comments · Fixed by #6829
Closed

Error message for "Invalid Lake configuration" appears for non-config related errors #6827

BoltonBailey opened this issue Jan 28, 2025 · 0 comments · Fixed by #6829
Labels
error message Error message produced by Lean is confusing or not informative P-medium We may work on this issue if we find the time

Comments

@BoltonBailey
Copy link
Contributor

See discussion in this Zulip thread.

When the Lean 4 server attempts to set up the environment and experiences an error, it prints the following error message:

Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.

It prints this message even if the error it experienced has nothing to do with the configuration file, (e.g. if there is a network error). One can see this by running $ lake new test math, then disconnecting from the internet and opening Basic.lean in VSCode.

The error message should be changed to something that better represent the set of possible problems that could give rise to this error.
@BoltonBailey BoltonBailey mentioned this issue Jan 28, 2025
Merged
@tydeu tydeu added the error message Error message produced by Lean is confusing or not informative label Jan 28, 2025
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Feb 4, 2025
github-merge-queue bot pushed a commit that referenced this issue Feb 8, 2025
@BoltonBailey
chore: change Lake configuration error message (#6829)
4989a60 
This PR changes the error message for Lake configuration failure to
reflect that issues do not always arise from an invalid lakefile, but
sometimes arise from other issues like network errors. The new error
message encompasses all of these possibilities.

Closes #6827
tobiasgrosser pushed a commit to opencompl/lean4 that referenced this issue Feb 16, 2025
@BoltonBailey @tobiasgrosser
chore: change Lake configuration error message (leanprover#6829)
869a2b9 
This PR changes the error message for Lake configuration failure to
reflect that issues do not always arise from an invalid lakefile, but
sometimes arise from other issues like network errors. The new error
message encompasses all of these possibilities.

Closes leanprover#6827
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
error message Error message produced by Lean is confusing or not informative P-medium We may work on this issue if we find the time
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

chore: change Lake configuration error message BoltonBailey/lean4
3 participants
@BoltonBailey @tydeu @leanprover-bot