New project gitignore

Stream: general

[Martin Dvořák]

When I create a new project, the file .gitignore contains:

/build
/lake-packages/*

Should .lake be there as well?

[Ruben Van de Velde]

What version of lake are you using to create it?

[Martin Dvořák]

I don't know how to find it out. This is what I did in immediate sequence when creating the project (probably wrong):

mdvorak@wngrad258 MINGW64 /c/Users/mdvorak/Documents
$ elan update
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2024-12-17
info: downloading component 'lean'
info: installing component 'lean'
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.14.0
info: downloading component 'lean'
info: installing component 'lean'

  leanprover/lean4:nightly updated - Lean (version 4.16.0-nightly-2024-12-17, x86_64-w64-windows-gnu, commit 64d3e9a48e54, Release)
   leanprover/lean4:stable updated - Lean (version 4.14.0, x86_64-w64-windows-gnu, commit 410fab728470, Release)

mdvorak@wngrad258 MINGW64 /c/Users/mdvorak/Documents
$ lake update self
error: unexpected arguments: self

mdvorak@wngrad258 MINGW64 /c/Users/mdvorak/Documents
$ lake update
error: no such file or directory (error code: 2)
  file: .\lakefile.lean

mdvorak@wngrad258 MINGW64 /c/Users/mdvorak/Documents
$ lake new matrix-tu-experimental math
info: Downloading lean-toolchain

PS: Now I did:

$ lake --version
Lake version 5.0.0-ffac974 (Lean version 4.15.0-rc1)

[Ruben Van de Velde]

Then it might be a lake bug

[Martin Dvořák]

Lake version 5.0.0-ffac974 is new enough?

[Ruben Van de Velde]

https://github.com/leanprover/lean4/commit/ffac974 is two weeks old, so I assume yes

[Ruben Van de Velde]

Though I don't see the bug in the code. You're sure this is the version you made the new project with?

[Martin Dvořák]

In the messed-up command sequence above, was I supposed to update Lake itself somehow? Or does elan update do everything on its own?

And regarding new projects, should both /lake-packages/* and /lake/* be there?

[Martin Dvořák]

Ruben Van de Velde said:

Then it might be a lake bug

Regarding reporting:
https://github.com/leanprover/lean4/issues/3345

[Ruben Van de Velde]

No, elan update should have (and did) updated your lake

[Ruben Van de Velde]

Heh, groundhog day

[Martin Dvořák]

I might have installed something incorrectly and it could be causing the same bug since.

[Kevin Buzzard]

FWIW

buzzard@brutus:~$ lake new matrix-tu-experimental math
buzzard@brutus:~$ more matrix-tu-experimental/.gitignore
/.lake
buzzard@brutus:~$

[Martin Dvořák]

Should .lake be the only gitignored folder?

[Julian Berman]

lake-packages doesn't exist on any recent lake (so I think yes?)

[Kevin Buzzard]

buzzard@brutus:~$ lake new matrix-tu-experimental math
buzzard@brutus:~$ ls matrix-tu-experimental/
lakefile.lean  lean-toolchain  MatrixTuExperimental  MatrixTuExperimental.lean

[Martin Dvořák]

And what does ls -a show?

[Kevin Buzzard]

buzzard@brutus:~/matrix-tu-experimental$ ls -la
total 32
drwxrwxr-x  4 buzzard buzzard 4096 Dec 17 14:17 .
drwxr-x--- 75 buzzard buzzard 4096 Dec 17 14:17 ..
drwxrwxr-x  7 buzzard buzzard 4096 Dec 17 14:17 .git
-rw-rw-r--  1 buzzard buzzard    7 Dec 17 14:17 .gitignore
-rw-rw-r--  1 buzzard buzzard  503 Dec 17 14:17 lakefile.lean
-rw-rw-r--  1 buzzard buzzard   29 Dec 17 14:17 lean-toolchain
drwxrwxr-x  2 buzzard buzzard 4096 Dec 17 14:17 MatrixTuExperimental
-rw-rw-r--  1 buzzard buzzard  178 Dec 17 14:17 MatrixTuExperimental.lean
buzzard@brutus:~/matrix-tu-experimental$

[Martin Dvořák]

Ah yes, but doing anything puts stuff into ./lake right? Hence your .gitignore is correct.

[Kevin Buzzard]

buzzard@brutus:~$ lake new matrix-tu-experimental math
buzzard@brutus:~$ cd matrix-tu-experimental/
buzzard@brutus:~/matrix-tu-experimental$ lake exe cache get
[stuff]
Completed successfully!
buzzard@brutus:~/matrix-tu-experimental$ ls -al
total 40
drwxrwxr-x  5 buzzard buzzard 4096 Dec 17 14:57 .
drwxr-x--- 75 buzzard buzzard 4096 Dec 17 14:57 ..
drwxrwxr-x  7 buzzard buzzard 4096 Dec 17 14:57 .git
-rw-rw-r--  1 buzzard buzzard    7 Dec 17 14:57 .gitignore
drwxrwxr-x  3 buzzard buzzard 4096 Dec 17 14:57 .lake
-rw-rw-r--  1 buzzard buzzard  503 Dec 17 14:57 lakefile.lean
-rw-rw-r--  1 buzzard buzzard 3128 Dec 17 14:57 lake-manifest.json
-rw-rw-r--  1 buzzard buzzard   29 Dec 17 14:57 lean-toolchain
drwxrwxr-x  2 buzzard buzzard 4096 Dec 17 14:57 MatrixTuExperimental
-rw-rw-r--  1 buzzard buzzard  178 Dec 17 14:57 MatrixTuExperimental.lean
buzzard@brutus:~/matrix-tu-experimental$ du -s .lake/
5202716 .lake/
buzzard@brutus:~/matrix-tu-experimental$

[Martin Dvořák]

All right! Should I report it as a (heisen)bug, or should I conclude that it is just a problem with my installation?

[Kevin Buzzard]

Well you're the only person with the problem, and it sounds like you've had the problem for nearly a year, so I suspect that the problem is at your end. Just delete your .elan directory and reinstall and see if that fixes the problem.

[Shreyas Srinivas]

what's your elan version?