Zulip Chat Archive

Stream: new members

Topic: Ruihua Wang

Ruihua Wang (Jun 13 2021 at 22:00):

Hi, I'm Ruihua Wang, a PhD student majoring in algebraic geometry in Leiden. I get to know the leanprover by accident and find it really interesting.

I already download stuffs related to it following the instruction. When I open the files used in Prof. Buzzard's course(For example, Part_A_logic.lean) in VS code, it tells me that there are 8 errors. And it seems that many of these error is due to "can't find 'tactic' in the search path", may I know how to solve it?

Ruihua Wang (Jun 13 2021 at 22:12):

error.PNG

Here is the screen shot of the errors. I know very little about computer, so maybe this is a very stupid question, sorry for that.

Kevin Buzzard (Jun 13 2021 at 22:13):

Did you follow the link in the error which gives you a list of common reasons for why this is happening?

Ruihua Wang (Jun 13 2021 at 23:07):

Kevin Buzzard said:

Did you follow the link in the error which gives you a list of common reasons for why this is happening?

Thanks for your reply! And sorry that I failed to follow it due to my poor knowledge about computer. This is a screenshot for that link.
Since I'm trying to open a file written by you, I guess it shouldn't be a bare file? Then, for the second one, which directory does it talk about and where should I running the code, git or VS code?

I feel kind of guilty for asking this questions. Are there any videos about how to use lean for the first time which I can follow directly? I only find a video about how to install Lean. link.PNG

Andrew Ashworth (Jun 13 2021 at 23:22):

well, from the course repo notes at https://github.com/ImperialCollegeLondon/formalising-mathematics

Andrew Ashworth (Jun 13 2021 at 23:22):

it says you can use the web browser version just to get started

Andrew Ashworth (Jun 13 2021 at 23:27):

I am not aware of videos, just https://leanprover-community.github.io/

Kevin Buzzard (Jun 13 2021 at 23:27):

Did you open a file in VS Code instead of using "open folder" to open an entire project?

Kevin Buzzard (Jun 13 2021 at 23:28):

That's my guess

Kevin Buzzard (Jun 13 2021 at 23:28):

The project should be configured correctly because you downloaded it from GitHub

Ruihua Wang (Jun 13 2021 at 23:32):

Kevin Buzzard said:

The project should be configured correctly because you downloaded it from GitHub

Thanks so much! Problems solved!

Ruihua Wang (Jun 13 2021 at 23:32):

Andrew Ashworth said:

I am not aware of videos, just https://leanprover-community.github.io/

Problems solved and thank you all the same!

Alex J. Best (Jun 14 2021 at 00:44):

@Scott Morrison made a few different demo videos I think, such as https://www.youtube.com/watch?v=b59fpAJ8Mfs&ab_channel=leanprovercommunityleanprovercommunity that can be really helpful to see how things go proving in lean.

Johan Commelin (Jun 14 2021 at 04:56):

Ruihua Wang said:

Hi, I'm Ruihua Wang, a PhD student majoring in algebraic geometry in Leiden.

Cool! I studied in Leiden. There are several other algebraic geometers in Leiden that have shown interest in Lean: David Holmes, Peter Bruin, Jesse Vogel, Pim Spelier, Daan van Gent.

Ruihua Wang (Jun 14 2021 at 09:07):

Johan Commelin said:

Ruihua Wang said:

Hi, I'm Ruihua Wang, a PhD student majoring in algebraic geometry in Leiden.

Cool! I studied in Leiden. There are several other algebraic geometers in Leiden that have shown interest in Lean: David Holmes, Peter Bruin, Jesse Vogel, Pim Spelier, Daan van Gent.

Hi, nice to meet you! David is my supervisor :)

Ruihua Wang (Jun 22 2021 at 16:51):

question.PNG

May I know why the inforview keeps being loading?

Kevin Buzzard (Jun 22 2021 at 16:57):

Not enough info :-) Do you have a fully compiled Lean project and did you open the project folder using VS Code's "Open folder" functionality?

Ruihua Wang (Jun 22 2021 at 17:12):

Kevin Buzzard said:

Not enough info :-) Do you have a fully compiled Lean project and did you open the project folder using VS Code's "Open folder" functionality?

Yes, I think I follow the instruction. Actually, it works well last time(with your help). But it just fails today, and I even tried to download a new compiled project, still being 'loading'.

Ruihua Wang (Jun 22 2021 at 17:13):

Q2.PNG

This is a full screen shot.

Johan Commelin (Jun 22 2021 at 17:23):

@Ruihua Wang Can you open a terminal, go to your project directory, and type leanpkg build?

Johan Commelin (Jun 22 2021 at 17:24):

(If you don't know what a terminal is, I can explain.)

Johan Commelin (Jun 22 2021 at 17:24):

leanpkg build should finish in a couple of seconds. If it takes longer, something is wrong.

Johan Commelin (Jun 22 2021 at 17:25):

One possibility is that without realizing it, you made a small change to some file in mathlib. Or something like that. And then it needs to recompile everything, everytime you open VScode.

Ruihua Wang (Jun 22 2021 at 17:28):

Johan Commelin said:

One possibility is that without realizing it, you made a small change to some file in mathlib. Or something like that. And then it needs to recompile everything, everytime you open VScode.

Q3.PNG