proofs broken after upgrade

Stream: new members

[Michael Beeson]

I upgraded to the latest version of lean. Now I get these messages:

inf.lean:1:0
file 'algebra/char_zero' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more
inf.lean:6:0
invalid import: data.real.basic
could not resolve import: data.real.basic
inf.lean:152:4
unknown identifier 'simp_rw'

At the top of my file I have

import tactic.finish
import data.real.basic

I can't remember why I wanted data.real.basic, but I definitely need simp_rw.

[Reid Barton]

import tactic.basic will import all the generally useful tactics such as finish and simp_rw.

[Michael Beeson]

Thanks. Now I have "no messages", which is good. I guess data.real.basic is irrelevant.

[Michael Beeson]

But now:

iMac:inf beeson$ leanproject build
Building project inf
Cmd('git') failed due to: exit code(128)
  cmdline: git reset --hard HEAD --
  stderr: 'fatal: Could not parse object 'HEAD'.'
iMac:inf beeson$

[Julian Berman]

(I am by no means a lean expert) but that error is coming from git basically saying some commit you're on "doesn't exist" really

[Julian Berman]

It could presumably be either the repo for your inf project itself, or for a dependency (say mathlib) which leanproject manages on your behalf

[Julian Berman]

Is your inf directory a git repo itself? If so possibly try git fetch

[Kevin Buzzard]

Can you output the result of ls in the directory where you are doing the commands?

[Kevin Buzzard]

I mean, where you're doing leanproject commands

[Michael Beeson]

iMac:inf beeson$ ls
Junk        _target     leanpkg.path    leanpkg.toml    src
iMac:inf beeson$

[Kevin Buzzard]

That looks lovely.

[Kevin Buzzard]

Is it a git repo?

[Kevin Buzzard]

what's the output of ls -al?

[Kevin Buzzard]

Do you know how git works?

[Reid Barton]

That's not the error message you'd get if it wasn't

[Kevin Buzzard]

OK then I give in :-)

[Reid Barton]

that said, the error message is still baffling

[Reid Barton]

I assume leanproject is running this in the mathlib directory? surely it's not going to git reset --hard HEAD your project itself??

[Michael Beeson]

I didn't make it a git repo but maybe Lean does that automatically.

iMac:inf beeson$ ls -al
total 40
drwxr-xr-x@ 10 beeson  staff   320 Sep 11 18:27 .
drwxr-xr-x@ 11 beeson  staff   352 Sep  5 20:26 ..
-rw-r--r--@  1 beeson  staff  6148 Sep 11 10:15 .DS_Store
drwxr-xr-x@  9 beeson  staff   288 Jun 12 23:19 .git
-rw-r--r--@  1 beeson  staff    31 Jun 12 23:17 .gitignore
drwxr-xr-x@  6 beeson  staff   192 Sep 11 10:16 Junk
drwxr-xr-x@  3 beeson  staff    96 Jun 12 23:17 _target
-rw-r--r--@  1 beeson  staff    54 Sep 12 07:09 leanpkg.path
-rw-r--r--@  1 beeson  staff   236 Sep 12 07:08 leanpkg.toml
drwxr-xr-x@ 11 beeson  staff   352 Sep 12 07:46 src
iMac:inf beeson$

No, I only know epsilon about git.

[Julian Berman]

What does git status tell you?

[Michael Beeson]

I guess I caused this problem by keeping my project under my Dropbox folder so it would sync to my laptop. Normally I keep
all my work in directories that start with Users/beeson/Dropbox so they sync to the laptop. And, I upgraded both machines
to the Aug. 2020 version of Lean. Before that they were in sync. Now, however, leanproject build seems to work on the laptop
but not on the desktop.

[Michael Beeson]

So the "leanproject build" command on the laptop left files in dropbox that are not correct on the desktop??

[Michael Beeson]

iMac:inf beeson$ git status
On branch master

No commits yet

Untracked files:
  (use "git add <file>..." to include in what will be committed)

    .DS_Store
    .gitignore
    Junk/
    leanpkg.toml
    src/

nothing added to commit but untracked files present (use "git add" to track)

[Julian Berman]

OK, well that's good, since yeah it's almost certainly then coming from leanproject running that on mathlib, which @Reid Barton mentioned (and which I see does indeed happen here: https://github.com/leanprover-community/mathlib-tools/blob/bf53aa4268452fbfbfd48e519ef847cae7e0053c/mathlibtools/lib.py#L592)

[Julian Berman]

I don't know if there's a leanproject(-or-lean-specific) way to fix this but I'd assume if you delete mathlib in the target directory that you'll get back a working clone. But probably would wait for one of the above experts to chime in :)

[Michael Beeson]

so I did "leanproject up" again. Output includes

> git checkout --detach c3a6a6990d620c3fadf11631038b38dd7fd50b39    # in directory _target/deps/mathlib
HEAD is now at c3a6a6990 doc(group_theory/subgroup): fix links in module doc (#4115)
Looking for local mathlib oleans
Found local mathlib oleans

After that, leanproject build works again normally.

[Julian Berman]

Cool, looks like you found the leanproject-specific solution, so well done :)

[Michael Beeson]

And also works on the laptop. So I guess the problem is solved. But I have no idea what the problem actually was or what caused it.

[Julian Berman]

Did you update on one machine or the other very recently? If so maybe dropbox was behind and only partially copied the .git directory over from one to the other, which yeah will confuse git.

[Michael Beeson]

That's a good theory! I'll bet you're right about that. Dropbox is usually virtually instant, but I guess there may be a lot of big
files involved in upgrading lean.

[Michael Beeson]

Thanks very much to all of you. It is really wonderful that all you geniuses are willing to help a bumbling newcomer, and at all hours and rapidly.
It's nice to feel that someone has my back.

[Julian Berman]

Yeah, overall I think what you're doing is fine (letting dropbox save you from having to learn too much git for your own machines), you just will run into this kind of thing if you switch from one to the other mid-sync.

[Patrick Massot]

Using Dropbox in this context is really really asking for trouble, but I'm glad you managed to get out of trouble.