Installation

Stream: LftCM22

[Sahana Balasubramanya]

I am in the process of installing Lean. Can I accept the default settings in the installation of VSCode? Or do any of them need to be changed?

[Heather Macbeth]

Summary of Rob's talk: make sure you have downloaded Lean and have the code for the textbook Mathematics in Lean downloaded to your computer and working correctly. Then you're ready to go for tomorrow!

[Heather Macbeth]

@Sahana Balasubramanya The default settings should be fine!

[Sahana Balasubramanya]

Awesome

[Sahana Balasubramanya]

@Heather Macbeth How do I download the code for the textbook, please?

[Rob Lewis]

To summarize my own talk:

• Install Lean
• leanproject get mathematics_in_lean
• code mathematics_in_lean

[Elif Sacikara (Alumni)]

Well, a while ago I was able to install formalising-mathematics-2022'' but now it doesn't recognise import tatics for instance. Furthermore, when I typed leanproject get mathematics_in_lean'' on the terminal first I get the error: in the terminal there is an error as 'leanproject' is not recognized as an internal or external command,
operable program or batch file

then now I got an error as ``leanproject : The term 'leanproject' is not recognized as the name of a cmdlet, function, script file, or operable
program. Check the spelling of the name, or if a path was included, verify that the path is correct and try again.
At line:1 char:1

• leanproject get mathematics_in_lean
• ~~~~~~~~~~~
  + CategoryInfo : ObjectNotFound: (leanproject:String) [], CommandNotFoundException
  + FullyQualifiedErrorId : CommandNotFoundException
  ''

[Sahana Balasubramanya]

Okay. I have gone through all the steps Rob listed. But I have a question: what should happen when I type in the command code mathematics_in _lean ? Currently another window of VSCode opens up, but I don't see anyt
hing else happening.

[Heather Macbeth]

@Sahana Balasubramanya That sounds perfect. code mathematics_in_lean means that you are asking VSCode to open Mathematics in Lean.

[Heather Macbeth]

Does it seem to be working? For example, if you click inside one of the proofs, do you see the "goal state" on the right?

[Rob Lewis]

You can browse the files in the project using the toolbar on the left. Open one and you should see output from Lean

[Sahana Balasubramanya]

I am currently seeing a 'Loading' message on the right hand side. Mybe one of you can zoom with me to take a look?

[Sahana Balasubramanya]

Okay, the goals just started to display! I guess it just needed some time to run.

[Sahana Balasubramanya]

Thank you both so much!

[Rob Lewis]

Sure thing!

[Sahana Balasubramanya]

Its really late here in Europe, so I'm going to sign out now. See you all tomorrow.

[Jackie Lang]

Hi all, I know it's early in the US, but maybe someone in Europe can help me. I believe I've done the installation and have Mathematics in Lean downloaded and working correctly on my computer. My problem is with mathlib. I have also downloaded this, but when I open it in VSCode, I get orange bars everywhere. It seems to be compiling(?) and it never stops. Yesterday it crashed my computer. Kevin tried to help me troubleshoot this yesterday, but nothing has worked. Any suggestions?

[Heather Macbeth]

A couple of things to try for orange bars:

• leanproject get-mathlib-cache (for a mathlib-dependent project like Mathematics in Lean) or leanproject get-cache (for mathlib itself) at the command line
• ctrl-shift-p "restart Lean" from within VSCode (on a mac, cmd-shift-p).

[Riccardo Brasca]

Also, make sure you have opened the folder created by leanproject, not only a single file.

[Jackie Lang]

Heather Macbeth said:

A couple of things to try for orange bars:

• leanproject get-mathlib-cache (for a mathlib-dependent project like Mathematics in Lean) or leanproject get-cache (for mathlib itself) at the command line
• ctrl-shift-p "restart Lean" from within VSCode (on a mac, cmd-shift-p).

We tried these yesterday to no avail.

[Jackie Lang]

Riccardo Brasca said:

Also, make sure you have opened the folder created by leanproject, not only a single file.

Can you say more about this? How do I know whether I'm in the folder created by lean project?

[Johan Commelin]

Did you start the project from the command line, with code path/to/the_project?
Or did you open it from withing VSCode?

[Johan Commelin]

From within VSCode it is important to use Open Project instead of Open File. (In particular, Ctrl-O or Cmd-O do the wrong thing.)

[Jackie Lang]

I opened it from within VSCode. I click on "open..." and then it brings up a Finder window, and I click on the mathlib folder. Is that wrong?

[Riccardo Brasca]

It's Open Folder (at least in my VSCode), ctrl K - O should also work.

[Jackie Lang]

Yes, I think that's what I've been doing

[Johan Commelin]

If you cd path/to/the_project and run leanproject build I suppose it also starts building like crazy?

[Riccardo Brasca]

That looks good. You did leanproject get blahblah?

[Johan Commelin]

It should finish in < 20s. But it looks like it is just completely ignoring the cache that you downloaded.

[Jackie Lang]

It is taking much longer than 20s.

[Thomas Browning]

One silly option is just to delete the project, and run leanproject new blah again

[Jackie Lang]

blah = mathlib?

[Thomas Browning]

Whatever the name of your project is

[Riccardo Brasca]

It depends on the project, but surely not mathlb.

[Thomas Browning]

e.g., blah = my_first_mathlib_project

[Riccardo Brasca]

I mean, you probably don't work to work on mathlib now. Maybe leanproject get mathematics_in_lean?
`

[Riccardo Brasca]

If you want to do the tutorial

[Jackie Lang]

I don't know think I have a project. All I've done is download mathlib. Then I click somewhere within the Lean code and orange bars appear everywhere.

[Riccardo Brasca]

Ah, you modified a file, that's the reason. Do you want to do the tutorial, right?

[Jackie Lang]

I think the tutorial is working fine. Last night I was just trying to get to a thing in mathlib that Kevin had created.

[Riccardo Brasca]

When you get any project you also get mathlib, the project will depend on it

[Jackie Lang]

I see, so I don't need to have a separate folder called mathlib?

[Riccardo Brasca]

No. If you want to probe class field theory, do leanproject new cft.

[Thomas Browning]

If you run leanproject get mathematics_in_lean (or leanproject new cft, or similar), mathlib will be somewhere in the project (often in a subfolder called _target)

[Jackie Lang]

Riccardo Brasca said:

No. If you want to probe class field theory, do leanproject new cft.

And where should I be when I do this? Does it matter?

[Riccardo Brasca]

It will create a folder cft, containing mathlib. You can create a new file cft.lean under src and start working. The first lines of the file will be something like import number_theory.padics.padic_numbers to be able to use the results in mathlib.

[Riccardo Brasca]

It doesn't matter where you do it. Any project has its own mathlib folder inside

[Jackie Lang]

Okay, let me try this

[Riccardo Brasca]

So there is no "mathlib installation"

[Riccardo Brasca]

Not a "global" one at least. Any folder created by leanproject contains its own mathlib.

[Jackie Lang]

That is very helpful. Thank you!

[Riccardo Brasca]

And remember to not touch any file in mathlib (meaning in the folder _target): if you do it then you need to recompile everything, and in practice you get the orange bar.

[Johan Commelin]

(If you do touch a file in mathlib, don't panic. It can be fixed with a few commands.)

[Jackie Lang]

I have another question that is more of a VSCode question. In the mathematics_in_lean tutorial, it says that I should be able to do things like git pull and leanproject get-mathlib-cache within the mathematics_in_lean folder. [Side question: how do I make commands appear in little boxes in Zulip for easy reading?] When I tried this, I got a permission denied error. Someone told me to put sudo in front of git pull. I was then prompted to enter my password and it all worked. This person said there should be a way to work in "admin mode" so that I don't have to enter my password all the time, but doesn't know how to do that. Does anyone here know?

[Johan Commelin]

```
code goes here
```

[Johan Commelin]

Hmm, are you on Windows/Mac/Linux? Usually a git pull shouldn't require sudo.

[Jackie Lang]

I'm on a Mac

[Johan Commelin]

Do you only need sudo from withing VSCode, or also when you are in a regular terminal?

[Johan Commelin]

(I don't know too much about Mac's. Except that they are pretty close to Linux.)

[Jackie Lang]

I also need sudo in a regular terminal when I try git pull.

[Johan Commelin]

@Jackie Lang what does ls -al output inside your project folder?

[Johan Commelin]

It might be that somehow it didn't pull the repo as files owned by your user, but somehow they ended up being owned by root or so

[Jackie Lang]

I think this is essentially what happened. I typed sudo chown -R $USER mathematics_in_lean while in the folder containing mathematics_in_lean and that seems to have fixed it. (I was not the one to figure this out!)

[Johan Commelin]

Great. I saw on the interwebs that other Mac users had to do similar things with git projects (-;

[Ryan McCorvie]

Do you have advice about how to organize navigation in the VS environment? I suppose its not an issue if I am typing in tactics, I was confused at first by the fact that I got different messages at the end of the line than the beginning. Do lean powerusers have a typical way to click around a file to see the messages? Also what messages do you typically display? I see a lot of old messages in the "all messages" section, do you usually keep this open? leanprover1.png

[Rob Lewis]

I usually hide the "All Messages" part and read them line by line. The breadcrumbs (colored dots on the scroll bar) are useful for identifying where errors are.

[Rob Lewis]

The first thing I do when setting up a VSCode instance is to disable the minimap (the tiny copy of your file left of the breadcrumbs)

[Jireh Loreaux]

I agree with Rob that I usually hide "All Messages". Although to see them in the file is kind of nice, as with the VS code extension errorlens that Johan mentioned in the last talk. You might consider installing that.

[Jireh Loreaux]

To answer your other question, about how to click around: I almost always click at the end of the line (at or after the comma), and that keeps things consistent for me. Clicking in the middle of a line can sometimes display weird information (although sometimes this can be helpful)

[Ryan McCorvie]

The integration of Lean in VS seems very nice, but does anyone use any other development environment? In the past I've used sublimetext to write latex, html and python, so I'm used to a lot of the shortcuts there. However, it doesn't seem to even have lean highlighting, so that doesn't seem like a productive route.

[Jireh Loreaux]

There are also Lean extensions for Emacs and Vim (or maybe it's NeoVim?). I don't think there are any for sublime text, but maybe someone will correct me.

[Rob Lewis]

There's support for emacs and neovim

[Ryan McCorvie]

I guess what confused me about getting different feedback when the cursor on different parts of the same line is that I'm used to working in a buffer tied to a REPL, so you send entire lines in your buffer to be evaluated. However, the lean VS environment to evaluate the whole file? For example, I don't have to tell it to evaluate the load library lines at the top, it does it just by loading the file. Is that right?

[Rob Lewis]

That's right, the whole file gets checked, and when you make changes, everything below will be re-checked. You can change this to, say, only check up to the lines you're looking at. (Click on "Lean :check: (checking visible files)" or similar on the bottom toolbar.) I think the default option is the best behaved and least confusing.

[Ryan McCorvie]

Oh, there's a native app for zulip on windows, macos and iphone. Installed.

[Flo (Florent Schaffhauser)]

Hi! I tried to do a git pull for mathematics_in_lean from VS Code (on Mac OS X), but I could not find how to do it, and I did not want to mess up anything. Does anyone have a hint? Kevin was helping me but the Zoom chat closed and I could not save the indications.

It worked from command line, though, so I have been able to see the new material uploaded by Patrick. I'm just curious for next time.

Also, after a git pull, what is recommended we do with the copy of src that we were practicing on? Keep it or get rid of it? Thanks!

[Jackie Lang]

@Flo (Florent Schaffhauser) When you try git pull, is it telling you that you don't have permission to do something? If so, I had that problem and had to change the permissions on my mathematics_in_lean folder. If it is anything else I probably can't help. If this sounds like the problem, see here: https://leanprover.zulipchat.com/#narrow/stream/330515-LftCM22/topic/Installation/near/289304315