Lean3: mathlibtools has been disabled

Stream: general

[ASIAN ASSASSIN]

Hey guys sorry for disturbing you but my university requires me to use lean 3 instead of 4 but the walkthrough to installing lean 3 doesn't work because of this error "

Error: mathlibtools has been disabled because it has an archived upstream repository! It was disabled on 2024-09-09." is there any other way to download lean 3 and not 4?

[Shreyas Srinivas]

You could try using the docker container for lean3

[Shreyas Srinivas]

But if your university requires lean3 then surely all students must be running into this error and your instructors ought to know by now

[Shreyas Srinivas]

which hopefully convinces them to use lean 4.

[Eric Wieser]

This sounds like a mistake; I don't think we realized that archiving the repo would cause homebrew to fail to install it.

[Julian Berman]

If you trust me (which you shouldn't, but you can look at https://github.com/Julian/homebrew-lean/blob/main/Formula/mathlibtools.rb if you know what you're looking at), then you should be able to get up and running by running brew install julian/lean/mathlibtools instead of brew install mathlibtools. I just pushed an (undisabled) equivalent formula.

[Julian Berman]

(Moving this thread anywhere but #lean4 also seems like a decent idea perhaps.)

[Notification Bot]

This topic was moved here from #lean4 > Lean3: mathlibtools has been disabled by Eric Wieser.

[Kim Morrison]

@ASIAN ASSASSIN, you would mind putting us in touch with whoever at your university is running the course requiring Lean 3? (You could DM me a contact detail.)

[ASIAN ASSASSIN]

@Julian Berman wow, thank you very much you're so kind:sob:

[ASIAN ASSASSIN]

@Julian Berman after installing lean 3 can these command lines still be used?
" /usr/local/bin/brew install elan-init mathlibtools elan toolchain install stable elan default stable "
or is there another because when I command ela toolchain install stable it outputs an error. Sorry I ask a lot of questions I'm new to this.

[Julian Berman]

Running brew install elan-init julian/lean/mathlibtools was what I believe should be the replacement command. The other 2 commands likely shouldn't be necessary so you might be able to skip them entirely, though that depends on the project your professor has given you. If you get an error message, please share what it says, along with at least a screenshot of what the project you have been given looks like.

[ASIAN ASSASSIN]

when I run lean --version it outputs this error : "

toolchain 'stable' is not installed
info: caused by: not a directory: '/Users/briannajoe/.elan/toolchains/stable'"

Screen Shot 2024-09-27 at 09.54.23.png

it's still the beginning but this is my first assignment

[Julian Berman]

Is there a leanpkg.toml file next to that file? What does it contain?

[Mauricio Collares]

Kim Morrison said:

ASIAN ASSASSIN, you would mind putting us in touch with whoever at your university is running the course requiring Lean 3? (You could DM me a contact detail.)

The exercises seem to come from Altenkirch's COMP2065 "Introduction to Formal Reasoning" (lecture notes at https://people.cs.nott.ac.uk/psztxa/comp2065.23-24.ifr-notes/_build/html/index.html, but I could only find the exercises themselves in some random GitHub repository).