Mathematics in Lean help with problem

Stream: new members

[Mustafa]

Hello, I'm currently doing the Mathematics in Lean course and keep running into a problem. Every time I edit the lean files (currently in C02_Basics/S01_Calculating.lean), lean just stops working. I have to keep restarting the file and server for it to work again. I followed the installation instructions on Mathematics in Lean with no issues. I have uploaded an image which is what always happens when I make an edit in the code. Just yellow lines and it stays like that. Can anyone please help me?
Screenshot 2024-11-04 133900.png

[Martin Dvořák]

Do you have Infoview somewhere?

I find it weird that the filetree does not contain lakefile and so on. Try going one folder up.

[Mustafa]

Martin Dvořák said:

Do you have Infoview somewhere?

I find it weird that the filetree does not contain lakefile and so on. Try going one folder up.

Hello. Yes I do have a lakefile, it's in the same directory of mathematics_in_lean, and I do have an Infoview. I'm not sure why it doesn't show
Screenshot 2024-11-04 135953.png
Screenshot 2024-11-04 135958.png

[Daniel Weber]

The folder you opened in vscode is the MIL folder — try opening the folder containing it

[Yan Yablonovskiy]

Mustafa said:

Hello, I'm currently doing the Mathematics in Lean course and keep running into a problem. Every time I edit the lean files (currently in C02_Basics/S01_Calculating.lean), lean just stops working. I have to keep restarting the file and server for it to work again. I followed the installation instructions on Mathematics in Lean with no issues. I have uploaded an image which is what always happens when I make an edit in the code. Just yellow lines and it stays like that. Can anyone please help me?
Screenshot 2024-11-04 133900.png

Generally its recommended you copy the MIL folder and edit/work in that folder; so its easier to update.

[Philippe Duchon]

If your copy of the MIL folder is obtained by a git clone command, VScode will see this and pester you to update when the source is changed - but if you do, of course any answers to the exercises you wrote directly in the same folder will create conflicts when you update, and you risk losing your work. This is why making a local copy is a good idea: you will continue working on slightly outdated exercises, but you won't lose your progress.

[Mustafa]

Ok I've gone one folder up. So I should only copy the MIL folder and place it outside the mathematics_in_lean folder? Or do you mean make a duplicate of MIL inside the mathematics_in_lean folder but change the name? I've tried both but I get the same error:

unknown module prefix 'MIL'

No directory 'MIL' or file 'MIL.olean' in the search path entries

Screenshot 2024-11-04 135958.png

[Mustafa]

I don't know what to do anymore. Lean is just slow and freezes for me. I have to constantly restart the server and file and even then sometimes it still doesn't work

[Daniel Weber]

What OS are you using?

[Mustafa]

I'm using windows 10

[Marc Huisinga]

@Patrick Massot It's possible that @Mustafa is experiencing similar issues as this student. These issues should be fixed on v4.13.0-rc4, v4.13.0 and v4.14.0-rc1, so updating MiL to one of these versions might resolve them.

Also, would it be an option for MiL to track Mathlib stable releases instead of RCs?

[Mustafa]

Marc Huisinga said:

Patrick Massot It's possible that Mustafa is experiencing similar issues as this student. These issues should be fixed on v4.13.0-rc4, v4.13.0 and v4.14.0-rc1, so updating MiL to one of these versions might resolve them.

Also, would it be an option for MiL to track Mathlib stable releases instead of RCs?

Thank you. So far lean is working

[Patrick Massot]

Yes, it feels very reasonable to track only stable releases. This will be painful when we want to add new chapters and need to tweak Mathlib, but this is not so frequent.

[Patrick Massot]

I will try to bump MIL to v4.13.0 very soon.