Trouble installing (Windows) - revision not found 'master'

Stream: new members

[Ryan O'Donnell]

Hi -
I'm trying to install Lean 4 on a Windows machine. I got the Lean4 extension in VS Code and am following the Setup doc. I got through installing elan and am now trying 'Set Up Lean 4 Project', one using Mathlib.
During the process, I got the following error:

"lake +leanprover-community/mathlib4:lean-toolchain update
info: learninglean1: no previous manifest, creating one from scratch
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4
error: .\.\.lake\packages\mathlib: revision not found 'master'"

In fact, I got this the first time I tried the process. Then I tried to figure out several fixes, ran into various other errors, finally tried to delete/uninstall everything and start from scratch... and I got back to the above error again. Any ideas?

Thanks!
Ryan

[Ruben Van de Velde]

Very odd, that seems like it should work. Might an antivirus get in the way?

[Ryan O'Donnell]

It's on a new laptop with a generic Windows 11 installation. Not sure what to try...

[Kevin Buzzard]

Try disabling your antivirus? Is your internet working fine?

[Ryan O'Donnell]

Internet works fine.

I now tried instead to follow the directions here:
https://leanprover-community.github.io/install/project.html

I did
"lake +leanprover/lean4:nightly-2024-04-24 new tolearnlean math"
That succeeded.
I went to the new "tolearnlean" folder and did
"lake update"
That yielded a new error message:

"info: tolearnlean: no previous manifest, creating one from scratch
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
error: .\.\.lake\packages\mathlib: could not resolve 'HEAD' to a commit; the repository may be corrupt, so you may need to remove it and try again"

I'm not sure I have any antivirus/firewall... To the extent that one exists, I'll try to disable it and rerun from the VS Code interface...

thanks for your help!
Ryan

[Ryan O'Donnell]

@Kevin Thanks for the great talk at CMU last month, by the way. My PhD student subsequently formalized a small but important group theory lemma from our latest paper. I just want to try getting involved myself... :)

[Ryan O'Donnell]

I tried it from the VS Code interface with antivirus off. Same "error: .\.\.lake\packages\mathlib: revision not found 'master'"
Also tried it from the VS Code interface with firewall off. Same "error: .\.\.lake\packages\mathlib: revision not found 'master'"
Both of these were tried with VS Code being run in Administrator mode.

[Ryan O'Donnell]

In case it's relevant, running "elan show" produces this:

"installed toolchains

---

leanprover/lean4:nightly-2024-04-24
leanprover/lean4:stable (default)
leanprover/lean4:v4.15.0-rc1

active toolchain

---

leanprover/lean4:stable (default)
Lean (version 4.14.0, x86_64-w64-windows-gnu, commit 410fab728470, Release)"

[Ryan O'Donnell]

I'm in Turkey right now, so I also tried it from a USA VPN. Didn't change anything. :(

[Ryan O'Donnell]

I tried it on another similar Windows machine and it succeeded.
Therefore it is something to do with my computer's configuration.
(Yet I only got this machine a week ago, so I haven't had that much chance to get it into a weird state...!)

[Marc Huisinga]

@Ryan O'Donnell Did you manage to figure out what caused lake update to fail to clone Mathlib on your machine? Does just git clone https://github.com/leanprover-community/mathlib4.git work?

[Ryan O'Donnell]

Thank you kindly for following up! My bad for not updating this thread, as I eventually did crack the case.

The short story is that (as many might have guessed) it had nothing to do with Lean.

Rather, I discovered that one basically cannot have git repositories inside a Box.com Drive, at least on Windows (as I was trying). It seems git is very picky about file-ownership-usernames and Box does some weird things with file-ownership-usernames.

I eventually restarted everything from scratch outside of a Box.com drive and it worked fine. I am now working on Chapter 3 exercises in Mathematics In Lean :)

[Marc Huisinga]

Thanks for reporting back, I'm sure this will be very helpful for anyone else running into a similar issue in the future :-)

[Jeremy Avigad]

@Ryan O'Donnell I am happy to hear that you are using MIL. Having just used it to teach an undergraduate course last semester, there are some improvements and revisions that I am hoping to make over the next couple of months. The most important piece of information / advice I have for new users is that it has gotten a lot easier to find theorems in the library. In addition to the suggestions in MIL (use tab completion, browse the online docs, use ctrl-click to jump to a definition and look for nearby theorems), these are good to know about:

• The search tactics have gotten faster. Use apply? to ask for suggestions for theorems to apply, rw? for suggestions for equations to rewrite with, and exact? to ask Lean to try to find something that will close the goal immediately.
• Loogle gives multiple options for symbolic search. In VS Code, type ctrl-k ctrl-s and read the instructions.
• Leansearch, an AI driven natural language search, is helpful. You can enter a vague verbal description of what you are looking for, and its suggestions are often good.

Also, Github copilot (which you can get free as an academic) is surprisingly good. It often pops up nonsense, but when it does that it is easy to ignore, and often enough it provides something helpful. (Of course, you can disable it if it is too helpful when you do the exercises.)

As far as automation, simp, ring, norm_num, and linarith are still mainstays, but thanks to Kim Morrison, we now also have omega, which solves some goals in integer linear arithmetic. It can even handle divisibility and mod:

example (n : ℕ) : n % 3 = 0 ∨ n % 3 = 1 ∨ n % 3 = 2 := by
  omega

example (x : ℤ) : 3 ∣ (x - 1) → x % 3 = 1 := by
  omega

There is other automation, like field_simp, simp_arith, gcongr, and module that is not yet discussed in MIL, but should be. Oh, and the split tactic is good for introducing cases to split if ... then ... else (and match) expressions. I don't remember if that is discussed in MIL yet, but it should be.