Where do proof steps show up?

Stream: new members

[Fernando Martin]

Hello, I have just set Lean up using the Mathematics in Lean tutorial. I'm trying to follow the text and it says that Lean displays the state of a proof on a separate VSCode window. Where does this show up? I can't find it, should this pop up in the 'Lean Goal' tab? Thanks!

[Patrick Massot]

The Lean goal tab is where Lean displays the state of a proof.

[Patrick Massot]

Can you share a screenshot?

[Dan Stanescu]

Hover your cursor over these icons in the upper right corner of your main window. Screen-Shot-2020-05-31-at-3.38.57-PM.png

[Dan Stanescu]

The fourth from the left, when pressed, will bring up the Lean goal window pane.

[Bryan Gin-ge Chen]

The Lean goal window should open automatically by default when you open a Lean file.

[Dan Stanescu]

@Bryan Gin-ge Chen I think that, when loading MiL, the Lean documentation opens up instead.

[Bryan Gin-ge Chen]

Ah, I see.

[Fernando Martin]

Thank you for your quick replies! I'm not entirely sure about what I did, but it started working (it does show up on the Lean goal tab now, but it didn't previously and I cannot reproduce the bug anymore)

[Kevin Buzzard]

I've had the same experience as Dan

[Fernando Martin]

Sorry to bother again, but I have run into a similar problem. I was able to follow the tutorial right until now, but I've reached a certain part that requires importing the exponential and logarithm definitions from the analysis.special_functions library. The Lean goal tab stops working when I try to import this. Here's a screenshot: image.png

[Fernando Martin]

It looks like it is using up most of the computer's resources as well... image.png Any pointers? Thanks!

[Bryan Gin-ge Chen]

The orange bars to the left of the editor window mean that Lean is busy. Did you use leanproject to get the olean files for mathlib? If not, your computer is compiling all of the Lean files on the fly, and this will take a long time.

[Fernando Martin]

Thanks for your reply Bryan. I don't think I did, I only followed the installation steps described in https://leanprover-community.github.io/install/windows.html. It looks as if I should run leanproject get-mathlib-cache but I'm getting an Invalid code repository error when doing so. Not sure how to proceed from here.

[Bryan Gin-ge Chen]

I just tried installing the tutorial from scratch using leanproject get mathematics_in_lean and then clicking on the first "try it" that had "analysis" in it. After a few seconds, the orange bars went away and the goal window worked.

[Fernando Martin]

(btw this explains why I wasn't able to see the proof state before, but after a while I could :) )

[Bryan Gin-ge Chen]

Did you initially download the tutorial using leanproject?

[Fernando Martin]

Yes, it run and returned the following error:

[Fernando Martin]

Cloning from https://github.com/leanprover-community/mathematics_in_lean.git [WinError 2] The system cannot find the file specified

[Bryan Gin-ge Chen]

Where are you running leanproject get-mathlib-cache from? You should be able to run it from the root of the mathematics_in_lean repository.

[Fernando Martin]

in any case I was able to use the tutorial so I thought that it was succesful, but now I'm not entirely sure

[Fernando Martin]

I'm running it from the same directory I ran leanproject get mathematics_in_lean in

[Fernando Martin]

which I guess is its root

[Bryan Gin-ge Chen]

If you run leanproject get mathematics_in_lean then that creates a subdirectory mathematics_in_lean. That subdirectory is the root of the mathematics_in_lean project.

[Bryan Gin-ge Chen]

So you may have to enter mathematics_in_lean first, with cd mathematics_in_lean and then run leanproject get-mathlib-cache from there.

[Fernando Martin]

:) thanks a lot for your patience Bryan, that did the trick