Distubing messages on start up

Stream: new members

[Douglas Lewan]

Hi, all, I'm just getting started using LEAN. I've opened .../tutorial (to get lean.toml), and I'm trying to work in 00_first_proofs.lean.
I've got 128 messages that seem wrong. For example,
invalid import: data.option.defs
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

1. I would assume that all the imports in that file should work. What do I need to do to make them valid?
2. WRT memory consumption, lean itself is taking 5.4 GB. Total memory consumption seems to be near 8GB. Does it realy have to be that high?

Finally,

3. I have a lot of messages like this: invalid object declaration, environment already has an object named 'option.elim._main'. Many of these messages are exact duplicates. How can I correct things to avoid such collisions?

[Eric Wieser]

Can you edit the title of your message above to move it to a new thread? thanks!

[Douglas Lewan]

Sorry. I'm new to zulip too.

[Douglas Lewan]

Another start up problem is that I have no "goals" window. (I'm using VSCode.) The very first runhad both infoview and goals. Now I can't tell how to get the goals window.

[Scott Morrison]

It seems likely you that don't have a local copy of mathlib setup correctly. Could you point us to the installation instructions you used?

[Mario Carneiro]

Douglas Lewan said:

Another start up problem is that I have no "goals" window. (I'm using VSCode.) The very first runhad both infoview and goals. Now I can't tell how to get the goals window.

Ctrl-shift-space, or a little button in the top right of the editor window will open the goal view

[Kevin Buzzard]

Did you install the project with leanproject and did you open the root directory (not a file) with VS Code?

[Kunhao Zheng]

I've got the same issue not long ago. Did you have something like "unknown archive format" when you do "leanproject get tutorials"?
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Issue.20of.20Installation.20on.20generic.20Linux/near/236359317

[Douglas Lewan]

I followed the instructions at https://leanprover-community.github.io/install/debian_details.html. I'm running Debian 9.4, stretch.
I followed the instructions at https://leanprover-community.github.io/install/project.html to install the tutorial, yes, with leanproject.

[Kevin Buzzard]

Can you open the root directory of the tutorials project using "open folder" with VS Code, then open 00_first_proofs.lean in src, and see if it works, and if it doesn't work then send a screenshot of your VS Code?

[Douglas Lewan]

I've tried starting again 'from scratch', something that VScode doesn't seem to want to do. I'd be happy to send a screenshot, but i'm not sure how to.

[Kevin Buzzard]

I would help, were you to be more precise about which part of uploading a screenshot to Zulip you're not sure how to do

[Douglas Lewan]

Here's a screenshot of VSCode. VScode-Screenshot_2021-04-29_13-14-10.png
(Sorry, as I mentioned elsewhere, I'm new to Zulip too.)

[Kevin Buzzard]

And what happens if you try ctrl-shift-P and then start typing restart and then click on Lean: Restart?

Independent of that, if you get to a terminal by pulling up on the blue bar at the bottom and then clicking on "TERMINAL", and then type ls src/data/option/*, what does the output say?

[Douglas Lewan]

If I restart, then I get the same results (many disturbing messages).
Here's the listing you asked for:
lean@debian2019:~/src/expt/lean/tutorials$ ls src/data/option/*
ls: cannot access 'src/data/option/*': No such file or directory
lean@debian2019:~/src/expt/lean/tutorials$
I'm guessing that that's not a good thing. It certainly suggests that I've missed something. Shouldn't the leanproject install have dealt with this?

[Bryan Gin-ge Chen]

Since you're working in the tutorials project and not mathlib, try ls _target/deps/mathlib/src/data/option/*.

[Douglas Lewan]

OK, I've done that; here are the results:
lean@debian2019:~/src/expt/lean/tutorials$ ls _target/deps/mathlib/src/data/option/*
_target/deps/mathlib/src/data/option/basic.lean _target/deps/mathlib/src/data/option/defs.lean
lean@debian2019:~/src/expt/lean/tutorials$

That feels better. What should I make of it?

[Kevin Buzzard]

Well we've located your problem, at least. I would delete the tutorials directly completely, get it again using leanproject and then check the output for errors. You don't have any olean files.

[Bryan Gin-ge Chen]

Running leanproject get tutorials will create a new directory tutorials/ with everything you need, hopefully. If you see any error messages in the leanproject output let us know.

[Douglas Lewan]

OK. I'll try again. Thanks for the attention.

[Douglas Lewan]

OK. I'm trying to go bck to the beginning, or at least as far as I can. I'm starting with "elan update". That gets the following:

lean@debian2019:~/src/expt/lean$ elan update
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.29.0
info: downloading component 'lean'
10.0 MiB / 10.0 MiB (100 %) 80.0 KiB/s ETA: 0 s
info: installing component 'lean'
info: checking for self-updates
info: downloading self-update
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download file from 'https://github.com/Kha/elan/releases/download/v1.0.2/elan-x86_64-unknown-linux-musl.tar.gz' to '/tmp/elan-update.N6Fcl7Pa3otC/elan-x86_64-unknown-linux-musl.tar.gz'
info: caused by: http request returned an unsuccessful status code: 404

I'm guessing that a 404 is not desirable.

[Bryan Gin-ge Chen]

Yeah, for some reason your system is looking for an option which isn't in the list here: https://github.com/leanprover/elan/releases/tag/v1.0.2

[Bryan Gin-ge Chen]

cc @Sebastian Ullrich

[Scott Morrison]

@Douglas Lewan, what do you get from uname -s and uname -m?

[Douglas Lewan]

lean@debian2019:~/src/expt/lean$ uname -s
Linux
lean@debian2019:~/src/expt/lean$ uname -m
x86_64
lean@debian2019:~/src/expt/lean$
Is that really intereting?

[Douglas Lewan]

OK, I went looking on github at https://github.com/leanprover/elan/releases/tag/v1.0.2. It looks reasonable to me. In particular, it looks like the link that elan wants is there. What am I missing?

[Scott Morrison]

The mystery is why it is looking for https://github.com/Kha/elan/releases/download/v1.0.2/elan-x86_64-unknown-linux-musl.tar.gz, rather than linux-gnu.

[Scott Morrison]

It's a bit strange. On e.g. distributions like alpine, it would be reasonable for it to be looking for the musl version (and then to complain that that is missing). But you're on a perfectly normal looking debian from what you've said, so it should be looking for the gnu version.

[Scott Morrison]

Maybe delete the entirety of your ~/.elan directory, and start fresh?

[Scott Morrison]

(by installing elan again: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh)

[Douglas Lewan]

I'm more than happy to push things back yet another step, and I'm doing it now. I've deleted ~/.elan and am reinstalling it with the above curl ... | sh incantation..

[Scott Morrison]

Any luck, @Douglas Lewan?

[Sebastian Ullrich]

It looks like there was a bug in elan self update between 0.11.0 and 1.0.2 that would look for the wrong URL on Linux. It should be fixed now, but you will need to update manually by reinstalling if your elan is affected.

[Sebastian Ullrich]

The bug was introduced because I didn't want to break the URL for older releases. Oh well...

[Douglas Lewan]

I still get an error here:
lean@debian2019:~/src/expt/lean$ elan update
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.29.0
info: checking for self-updates
info: downloading self-update
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download file from 'https://github.com/leanprover/elan/releases/download/v1.0.3/elan-x86_64-unknown-linux-musl.tar.gz' to '/tmp/elan-update.1j5fOI1SOl2v/elan-x86_64-unknown-linux-musl.tar.gz'
info: caused by: http request returned an unsuccessful status code: 404

[Ruben Van de Velde]

Yeah, you need to reinstall elan with the instruction from the second point here: https://leanprover-community.github.io/install/debian_details.html

[Douglas Lewan]

OK, I've removed and re-installed elan. I've tried re-installing the tutorials project. I still get the following error:
Unknown archive format '/home/lean/.mathlib/95260613e481c2571df45c3961d491821f147dd8.tar.xz'
I could unpack that archive; it looks like it should be unpacked in .../tutorials. Should it?
I've looked at the source for leanproject and it invokes python magic that I don't understand..
Would unpacking that archive be the last step? If so, I'll do it. If not, how do I glean what other intermediate steps I should go through.

[Kevin Buzzard]

Yes, all your problems are caused by that big zipped up collection of oleans not being on your system, and that error may indicate that your version of python is too old. What does python3 -- version give you? Someone posted a very nice trick to persuade leanproject to use a specific version of python -- search the chat for Unknown archive format and you'll find a couple of people struggling with this for which a python upgrade fixed the problem.

[Douglas Lewan]

python3 --version gives me 3.9.4. It was built from source. That seems to be the most recent stable version.
Rather than mucking about, possibly corrupting the target system, with adding new versions of python, it strikes me that a simpler solution would be to install a ".tar" archive instead of a ".tar.xz" archive.
Again, I'll ask, can I simply unpack that archive (under .../tutorials)? Or is there more?

[Scott Morrison]

So, you can just unpack that archive (someone... we'll have to investigate to know for sure, as all of us just use the tooling!). I think we're all hesitant to recommend it as this is a step that has to be done regularly (every time you want to move to a new version of mathlib --- mathlib updates many times a day!).

[Scott Morrison]

We'd also like to work out the root cause of your problem. It may be that you have an unusual system (the fact that you have python built from source suggests so :-), or it may be a problem in the tooling, which we'd like to fix.

[Scott Morrison]

(And regarding why it is a .tar.xz, rather than just a .tar: this is a file that many of us who hack on mathlib download many times a day as part of our workflow.)

[Kevin Buzzard]

It's python3 pre about 3.5 which was problematic. If you've built from source then do you have this lzma module installed or whatever it's called? I urge you to search out the recent thread on all this.

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Issue.20of.20Installation.20on.20generic.20Linux/near/236372684

[Scott Morrison]

The thread is https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Issue.20of.20Installation.20on.20generic.20Linux

[Scott Morrison]

Kunhao Zheng's last message on that thread is almost certainly your problem.

[Kunhao Zheng]

If you cannot import lzma when in your python environment, that is exactly the same problem as mine. :thinking: Rebuilding your python (with lzma installed) or getting another one should get away with that.

[Douglas Lewan]

@Scott Morrison, No luck yet. I've stopped using python3 3.9.4 and going back to the 3.5.3, the version supplied by Debian.
I tried installing python-lzma, but it looks like that only applies to python < 3. python3 3.5.3 continues to complain about an "unknown archive format".
So, I've gone back to using python3 3.9.4
I've been combing through its code and installation and I do find /usr/local/lib/python3.9/lzma.py, which I assume can be found and loaded. (Is "loaded" the right word in python? I've had very little interaction with python.)
I've also installed the lzma and lzma-dev packages from Debian. I'm currently rebuilding python3 3.9.4. The test code mentions .tar.xz files, but does say that those tests depend on the presence of lzma.
I'll let you know how things work out.

[Douglas Lewan]

@Scott Morrison @Kunhao Zheng @Kevin Buzzard
Rebilding python3 with lzma support did the trick.
Thanks to everyone for all the help.
Now, on to more interesting issues (I hope).

[Kevin Buzzard]

@Douglas Lewan I'm sorry it took you so long to get started. Lean is a project and not a finished product, and the community has worked hard to try and make the installation process as painless as possible, but unfortunately it still involves pain for some. If it's any consolation, this part is by far the most boring part, and if you can get the tutorial project running then our general experience is that you won't run into any more infrastructure issues -- the tutorial project is complex from an infrastructure point of view -- it has mathlib as a dependency, for example. If you can run it, you should now be able to run anything.

[Douglas Lewan]

Thanks. And I understand.
The spirit behind the GNU autoconf project might also be worth considering, although I have no idea how you would build a test in python to catch the .tar.xz issue. Python's test code may give a hint.
I've already started looking at the tutorial code. A "Nebenprojekt" (What's the right english word?) will be learning the documentation system and how to walk available modules. My experience has been that learning how a language's documentation works is one of the hardest parts to learning that language.

[Eric Wieser]

I assume we can make leanproject emit a better diagnostic message for this problem without too much work

[Patrick Massot]

I am very curious about this new trend. Can people explain why they choose to compile python instead of using prebuilt python? I can vaguely imagine people who would want a stripped down standard library for some reason, but here you seem surprised to discover you are missing part of the standard library. What's the story?

[Eric Wieser]

I've been in that position before when using a shared-usage linux machine to which I don't have sudo access, and on which the system python is way too out of date.

[Bolton Bailey]

The error described in this thread happens pretty often to me while I am editing mathlib in VSCode. Seemingly out of nowhere, I get a error on every lemma on every file I open which says
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

Restarting lean does not fix the problem. My other troubleshooting routine is to run leanproject get-mathlib-cache which gives me failed to fetch mathlib oleans. When I run lean --make src it seems to go off without a hitch. I can't discern any pattern in what causes this to start happening. Is the takeaway from this thread that I should try to reinstall elan?

[Bolton Bailey]

An interesting observation: restarting VSCode itself seems to fix the issue

[Kevin Buzzard]

Failed to fetch mathlib oleans just means that the mathlib commit you're working on isn't in the collection of compiled oleans that GitHub makes. It's easy to make that happen, eg edit a file in mathlib and then commit locally without pushing and waiting a few hours