leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: Some error while installing lean


Michael Wahlberg (Feb 04 2023 at 18:29):

I can't make any sense of this error, does anybody here have any ideas? Screenshot-2023-02-04-235702.png

Mauricio Collares (Feb 04 2023 at 20:12):

The Lean version specified in your project's lake-toolchain file must match std4's (currently leanprover/lean4:nightly-2023-01-29 but that might depend on your lake manifest)


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll