Lake uses nonexistent lean version

Stream: new members

[Michiel Huttener]

I'm currently reading "Functional Programming in Lean", but lake's new projects don't seem to be working. More specifically, I get the following error:

Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download nonexistent lean version `leanprover/lean4:rc4`
info: caused by: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/rc4' to '/Users/mbhutten/.elan/tmp/9_w4wg134zsf1g39_file'
info: caused by: http request returned an unsuccessful status code: 404

lean-toolchain was initialized to

leanprover/lean4:rc4

What version should I use and why doesn't lake figure this out by itself?

If it helps, I'm on mac, using VS Code and the lean4 extension which does work in other files.

[Alex J. Best]

How did you obtain this lakefile? When I look at examples in https://github.com/leanprover/fp-lean/tree/master I see leanprover/lean4:4.1.0 as of four days ago

[Michiel Huttener]

I followed the command in the book : lake new feline; see Section 2.4 Worked Example: cat.

[Michiel Huttener]

Note that this has nothing to do with FPIL.

[Kevin Buzzard]

If you type lake new bovine on your system now, do you get this bad lean-toolchain in the bovine directory?

[Michiel Huttener]

Yes

[Kevin Buzzard]

I think this might indicate that the problem is with your setup rather than the book. Do you have some default toolchain set up in elan which doesn't exist, or something?

[Michiel Huttener]

I don't think so. Do you know where such a configuration could be found?

[Michiel Huttener]

I ran elan update and now everything seems to be working just fine. lean-toolchain now initializes to stable. Thanks for the help!