search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.4k stars 311 forks source link

Doc bug: "Using mathlib4 as a dependency" tutorial command failed #11031

Open sullyj3 opened 7 months ago

sullyj3 commented 7 months ago

Hi there!

I tried the command recommended here:

lake +leanprover-community/mathlib4:lean-toolchain new my_project_name math

And it failed with 

info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download nonexistent lean version `leanprover-community-mathlib4-lean-toolchain`
info: caused by: could not download file from 'https://github.com/leanprover-community/mathlib4/releases/expanded_assets/lean-toolchain' to '/home/james/.elan/tmp/6thtp_96151it0z7_file'
info: caused by: http request returned an unsuccessful status code: 404

I was able to workaround by just creating an empty project and using the "In an existing project" instructions instead.

quinn-dougherty commented 6 months ago

I'm failing with 

╰─>$ lake +leanprover-community/mathlib4:lean-toolchain new lean-contracts math
error: unknown command '+leanprover-community/mathlib4:lean-toolchain'
fogti commented 1 month ago

I'm failing at using the "In an existing project" part, because it apparently only works when .git is added to the end of the URL, otherwise it (lean-4.11.0-rc1) just silently ignores the dependency.