Git question

Stream: new members

[Freek Wiedijk]

I decided to give Lean another try (the system is a bit impolite, but I'll try to ignore this). My current question is that in vscode on my arm debian after I create a fresh project I get a blue circle with a one on the git icon, and if I do "git status" it tells me "modified: .lake/packages/Cli (untracked content)". So what should I do to get rid of that blue one? My knowledge of vscode and git is not sufficient to decide what is the best approach for this.

[Gareth Ma]

Please open a "new conversation"

[Gareth Ma]

Screenshot-2024-04-25-at-12.55.04.png
By clicking this button

[Freek Wiedijk]

As will be clear I'm a newbie. How do I remove that message?

[Gareth Ma]

You can hover over a message and press either delete or "move message"

[Notification Bot]

5 messages were moved here from #new members > Floor division hell in asymptotics by Freek Wiedijk.

[Freek Wiedijk]

Gareth Ma said:

Screenshot-2024-04-25-at-12.55.04.png
By clicking this button

I don't see that button. Should I just change the topic before pressing the blue button on the right?
Screenshot-2024-04-25-at-13.58.18.png

[Ruben Van de Velde]

Okay, it worked

[Ruben Van de Velde]

Now that git message sounds a little odd. How did you create the new project?

[Freek Wiedijk]

I was using a web browser, but now installed an app. Let's see whether that works more easily for me.

[Freek Wiedijk]

And I still would like an answer to my git question :smile:

[Freek Wiedijk]

(deleted)

[Ruben Van de Velde]

Yeah, that's... a choice :)

[Ruben Van de Velde]

Ruben Van de Velde said:

Now that git message sounds a little odd. How did you create the new project?

So how about this?

[Freek Wiedijk]

Ah, I missed that reply, sorry. I did lake new lean4 math, then cd lean4, then lake update, then lake exe cache get, then git commit -a, then git status.

[Ruben Van de Velde]

Let me try that

[Freek Wiedijk]

Actually instead of git commit -a I clicked inside code, to get rid of the blue number on the git icon.

[Richard Osborn]

You need to add /.lake/ to your .gitignore file.

[Freek Wiedijk]

I can do that, but why did lake new ... not put it there? Currently the contents are:

/lake-packages/*```

[Ruben Van de Velde]

The location of dependencies changed, apparently this wasn't updated

[Freek Wiedijk]

Ruben Van de Velde said:

Let me try that

Did you get the same behavior, or does it have something to do with my setup?

[Richard Osborn]

Also, your git commit -a staged those files in .lake which isn't advisable.

[Ruben Van de Velde]

I did get the same outcome

[Ruben Van de Velde]

Which is really odd, because the other dependencies got added, but only Cli is still marked as pending change

[Freek Wiedijk]

Richard Osborn said:

Also, your git commit -a staged those files in .lake which isn't advisable.

I don't think it did, as it is "untracked content"?

[Ruben Van de Velde]

If you do git log --stat, I think you'll see that you added a number of things under .lake

[Freek Wiedijk]

Richard Osborn said:

You need to add /.lake/ to your .gitignore file.

Should this be /.lake/ or /.lake or /.lake/* or doesn't it matter?

[Ruben Van de Velde]

I'm not sure it matters, but mathlib uses /.lake/

[Freek Wiedijk]

Ruben Van de Velde said:

If you do git log --stat, I think you'll see that you added a number of things under .lake

Yes. mathlib for example! But apparently that had a different status from Cli. So should I start fresh, and add this /.lake/ line to .gitignore before making my initial commit?

[Richard Osborn]

just type git undo and you should be fine

[Ruben Van de Velde]

I would start fresh, yeah, but use the first command in https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

[Ruben Van de Velde]

That will get you a correct gitignore

[Freek Wiedijk]

Ruben Van de Velde said:

I would start fresh, yeah, but use the first command in https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

Okay, I'll do so, thanks for the help, and thanks for the pointer to the correct command. The lake update and lake exe cache get are still correct, and should be given explicitly after?

[Ruben Van de Velde]

I think lake update will not do anything at this point, because lake new should get the newest version of mathlib anyway, but it won't hurt

[Ruben Van de Velde]

Definitely use lake exe cache get to get a precompiled version of mathlib

[Freek Wiedijk]

It's taking time, so I think it's doing something. I think mathlib was not downloaded yet.

[Ruben Van de Velde]

Oh yes, it looks like I was wrong and lake update does do something at this point

[Freek Wiedijk]

git status now says:

On branch master

No commits yet

Untracked files:
  (use "git add <file>..." to include in what will be committed)
        .gitignore
        Lean4.lean
        Lean4/
        lake-manifest.json
        lakefile.lean
        lean-toolchain

nothing added to commit but untracked files present (use "git add" to track)

Which of those should I add to .gitignore, and which should I git add? Or can I just go into code, and will it do the right thing for me?

[Freek Wiedijk]

I guess the Lean4 stuff is because I called the project lean4?

[Ruben Van de Velde]

Yes, exactly. You should add all of those

[Freek Wiedijk]

And the lean-toolchain file says leanprover/lean4:v4.7.0. Does that mean that the project won't automatically move versions if a newer version of lean4 comes out?

[Ruben Van de Velde]

That's correct

[Freek Wiedijk]

So what is the lake command to move to a newer lean?

[Freek Wiedijk]

Or to pull the most recent version of mathlib for that matter?

[Richard Osborn]

I believe you just need to edit that file (and run lake update)

[Ruben Van de Velde]

lake update will update mathlib, and I think it now automatically updates lean-toolchain to match mathlib

[Freek Wiedijk]

That sounds great, thanks for all the help.

[Freek Wiedijk]

Sorry for all the questions, but as this is a newbie channel, I hope I shouldn't feel too embarrassed about it.

[Ruben Van de Velde]

Lean4 is still changing quite a lot in ways that need accompanying mathlib changes, so you want to use a matching version

[Ruben Van de Velde]

No worries, that's what this stream is for

[Freek Wiedijk]

So I should just do lake update occassionally? I'll try to remember that.

[Freek Wiedijk]

If I do lake update I get:

warning: Qq: ignoring missing dependency manifest './.lake/packages/Qq/lake-manifest.json'
warning: Cli: ignoring missing dependency manifest './.lake/packages/Cli/lake-manifest.json'

Should I worry about that? I like my life to be warning-free.

[Freek Wiedijk]

But maybe being warning-free is something a Lean-user should not aspire to? :smile:

[Marc Huisinga]

By the way, a way to go through all these steps without the terminal is to open VS Code, open an empty text document and then click the following button:
image.png

That should set up your project depending on Mathlib for you with the correct toolchain, run lake update, lake exe get cache and create an initial commit with all these files.

[Freek Wiedijk]

Good to know, I'll try that next time :smile:

[Marc Huisinga]

Freek Wiedijk said:

If I do lake update I get:

warning: Qq: ignoring missing dependency manifest './.lake/packages/Qq/lake-manifest.json'
warning: Cli: ignoring missing dependency manifest './.lake/packages/Cli/lake-manifest.json'

Should I worry about that? I like my life to be warning-free.

No, you don't need to worry about it. I should probably just go ahead and add a lake-manifest.json file to lean4-cli already!

[Freek Wiedijk]

Just an empty file?

[Marc Huisinga]

To be clear, this is nothing you should do, but something that I should do for the repository behind Cli.
It won't be quite an empty file, but close to one :-)

[Freek Wiedijk]

And not for Qq? So how do I get rid of those warnings then?

[Mario Carneiro]

these are issues in the upstream dependencies. Honestly it's not great that lake is bugging users about it, because there is nothing you can do to fix it short of forking the dependency

[Marc Huisinga]

Or, less drastically, bug the maintainer to fix it

[Freek Wiedijk]

Like I said at the very start: occasionally impolite :smile: I'll ignore the warnings then for now. Thanks for all the help!

[Freek Wiedijk]

Marc Huisinga said:

Or, less drastically, bug the maintainer to fix it

Which apparently I have just done :grin:

[Mario Carneiro]

By the way, the issue you had with lake-packages showing up in the gitignore instead of .lake is evidence that you used an old lake version to run lake new

[Mario Carneiro]

which makes sense, this is a frequent issue for people coming back to lean after a hiatus

[Freek Wiedijk]

That's probably true then. So how do I update my lake?

[Mario Carneiro]

elan update stable IIRC

[Freek Wiedijk]

And should I update my lean4 too?

[Mario Carneiro]

it does both

[Mario Carneiro]

although for lean itself it doesn't matter as much because once you are in a project the lean-toolchain file overrides whatever you have set locally

[Mario Carneiro]

lake new is special because it's the only lean command you are likely to run outside the context of a project

[Freek Wiedijk]

So are there two lean4s then, one for my system and one for my project? That seems wasteful. Can I get rid of the global one then?

[Mario Carneiro]

there are much more than two :)

[Mario Carneiro]

elan holds all versions of lean that you have had cause to use, you can see them with elan toolchain list

[Freek Wiedijk]

Guest. I'll be back later.

[Mario Carneiro]

The lean version used by your project is not stored in the project, it is stored in the .elan folder. So if you have multiple projects on the same version of lean you won't have two leans installed for those, but if you have two projects with different versions of lean then elan will cache them both

[Freek Wiedijk]

Ah yes, I see a lot of junk in that .elan/toolchains:

leanprover-community--lean---3.51.1     leanprover--lean4---v4.3.0-rc1
leanprover--lean4---nightly             leanprover--lean4---v4.7.0
leanprover--lean4---nightly-2023-02-04  leanprover--lean4---v4.7.0-rc2
leanprover--lean4---nightly-2023-06-20  stable
leanprover--lean4---stable

Is there a way to remove unused versions to clean up some space on my system?

[Freek Wiedijk]

I see a stable and a leanprover--lean4---stable and a lot of versions. I would have expected those stables to be symbolic links, but they aren't? Which versions are those then?

[Freek Wiedijk]

And the executables in ~/.elan/bin all seem links to the same file. Is that in one of those toolchains as well?

[Freek Wiedijk]

Sorry, but I'd like to have some idea what Lean is sprinkling around my system :smile:

[Kevin Buzzard]

Do you know about .mathlib?

[Marc Huisinga]

Freek Wiedijk said:

I see a stable and a leanprover--lean4---stable and a lot of versions. I would have expected those stables to be symbolic links, but they aren't? Which versions are those then?

They're whatever version the respective toolchain resolved to at the time of installation. Improving this is https://github.com/leanprover/elan/pull/106, but unfortunately nobody has extensively tested this change yet, and Sebastian hasn't had time to work on Elan for a while.

[Freek Wiedijk]

Kevin Buzzard said:

Do you know about .mathlib?

Ah, another unexpected hidden directory in my homedir... That's just 250M, the mathlib of the project is in .lake/packages/mathlib, I think? That's why I want just one project (with subdirectories for my actual project), which is why I called it lean4 instead of something meaningful.

[Marc Huisinga]

Freek Wiedijk said:

And the executables in ~/.elan/bin all seem links to the same file. Is that in one of those toolchains as well?

.elan/toolchains contains the toolchains, .elan/bin is what is called when you call lean, lake etc., which then calls the correct toolchain binary (e.g. in a folder with a lean-toolchain file, it uses the one designated in that file).

[Freek Wiedijk]

I see, thanks, that makes sense.

[Freek Wiedijk]

So if I just delete all toolchains from .elan/toolchains apart from the one that is in the lean-toolchain file of my project, will I break anything?

[Freek Wiedijk]

Those files in ~/.elan/bin are 12M, that's a lot of binary for such shallow functionality (just finding the right toolchain, and invoking what's there?) I guess they're programmed in Lean? :smile:

[Freek Wiedijk]

(deleted)

[Marc Huisinga]

I think I'd make sure that your default toolchain is the same as the one in your project first (elan show tells you what it is and you can set it with elan default <...>), but after that, deleting unused toolchains should be fine.
Alternatively, you can also use elan toolchain uninstall <...> to uninstall toolchains from the CLI.

Freek Wiedijk said:

Those files in ~/.elan/bin are 12M, that's a lot of binary for such shallow functionality. I guess they're programmed in Lean? :smile:

Elan is a Rust project and was originally forked from rustup.

[Freek Wiedijk]

Will the elan toolchain uninstall ... do more than just removing those directories (like update some configuration files)?

[Freek Wiedijk]

And, as Kevin pointed out: can I just clean out the .tar.gzs in .mathlib? Is that Lean3 or Lean4 stuff?

[Marc Huisinga]

Freek Wiedijk said:

Will the elan toolchain uninstall ... do more than just removing those directories (like update some configuration files)?

I don't think so. I'm pretty sure that I've used both in the past before.

[Mario Carneiro]

elan toolchain uninstall removes the directory from .elan/toolchains and also removes a file from update-hashes. If you do only the former without the latter then elan will enter a bad state, this is a common issue since it's natural to nuke the big folder and forget to clean up the config (not sure if there is an issue tracking this though or if it has since been fixed)

[Freek Wiedijk]

Ouch! I just deleted all those subdirs. If I delete the corresponding ones from update-hashes I'm fine again?

[Mario Carneiro]

I believe so

[Freek Wiedijk]

Okay, thanks, I'll do so now then.

[Freek Wiedijk]

ls -ld */* in .elan now says:

-rwxr-xr-x 7 freek freek 12136504 Apr 25 14:40 bin/elan
-rwxr-xr-x 7 freek freek 12136504 Apr 25 14:40 bin/lake
-rwxr-xr-x 7 freek freek 12136504 Apr 25 14:40 bin/lean
-rwxr-xr-x 7 freek freek 12136504 Apr 25 14:40 bin/leanc
-rwxr-xr-x 7 freek freek 12136504 Apr 25 14:40 bin/leanchecker
-rwxr-xr-x 7 freek freek 12136504 Apr 25 14:40 bin/leanmake
-rwxr-xr-x 7 freek freek 12136504 Apr 25 14:40 bin/leanpkg
drwxr-xr-x 7 freek freek     4096 Apr 25 13:44 toolchains/leanprover--lean4---v4.7.0
-rw-r--r-- 1 freek freek       67 Apr 25 13:44 update-hashes/leanprover--lean4---v4.7.0

I hope I didn't delete too much :smile:

[Mario Carneiro]

What happens if you run lake --help outside a lean project?

[Freek Wiedijk]

Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)

USAGE:
  lake [OPTIONS] <COMMAND>

COMMANDS:
  new <name> <temp>     create a Lean package in a new directory
  init <name> <temp>    create a Lean package in the current directory
  build <targets>...    build targets
  exe <exe> <args>...   build an exe and run it in Lake's environment
  clean                 remove build outputs
  env <cmd> <args>...   execute a command in Lake's environment
  update                update dependencies and save them to the manifest
  upload <tag>          upload build artifacts to a GitHub release
  script                manage and run workspace scripts
  scripts               shorthand for `lake script list`
  run <script>          shorthand for `lake script run`
  serve                 start the Lean language server

OPTIONS:
  --version             print version and exit
  --help, -h            print help of the program or a command and exit
  --dir, -d=file        use the package configuration in a specific directory
  --file, -f=file       use a specific file for the package configuration
  --quiet, -q           hide progress messages
  --verbose, -v         show verbose information (command invocations)
  --lean=cmd            specify the `lean` command used by Lake
  -K key[=value]        set the configuration file option named key
  --old                 only rebuild modified modules (ignore transitive deps)
  --rehash, -H          hash all files for traces (do not trust `.hash` files)
  --update, -U          update manifest before building
  --reconfigure, -R     elaborate configuration files instead of using OLeans

See `lake help <command>` for more information on a specific command.

[Mario Carneiro]

in that case I think you're good

[Mario Carneiro]

elan will automatically install new toolchains as needed if you try to compile a project on a different version

[Mario Carneiro]

it's rare to need to do elan toolchain install directly

[Freek Wiedijk]

Freek Wiedijk said:

And, as Kevin pointed out: can I just clean out the .tar.gzs in ~/.mathlib? Is that Lean3 or Lean4 stuff?

So can I remove those files, that look like they're intermediate files for installing something?

[Mario Carneiro]

I don't think anything in lean 4 uses .mathlib. IIRC that's the path used for leanproject get-cache which is lean 3

[Freek Wiedijk]

Mario Carneiro said:

I don't think anything in lean 4 uses .mathlib. IIRC that's the path used for leanproject get-cache which is lean 3

I'm not interested in Lean 3. So I'll remove that directory then.

[Mario Carneiro]

However you should watch .cache/mathlib, which contains mathlib4 cache files

[Mario Carneiro]

in both cases it's just a cache, you can freely delete things and they will just be re-downloaded if needed

[Freek Wiedijk]

One gigabyte! Okay, so I'll remove those files also then.

[Mario Carneiro]

IIRC there are about 400 MB of cache files downloaded for one mathlib

[Mario Carneiro]

and these unpack to about 4 GB inside each mathlib-depending project

[Mario Carneiro]

(yes, lean4+mathlib is chunky)