Confused about proper way to set up git repo

Stream: new members

[mars0i]

I've ended up with git repos for which Mathlib wasn't installed correctly. So I follow the instructions here:
https://leanprover-community.github.io/install/project.html#updating-mathlib-in-your-project
and then everything works.

But now I have updated files lake-manifest.json, lakefile.lean, and lean-toolchain. And I don't want to commit them because I think that will mess up the same repo on my other computer. (Is that incorrect?)

I add those three filenames to .gitignore and then (this part I really don't understand--it's bizarre) git still thinks they need to be committed. I'm confused. This has never happened, and it doesn't seem to have anything to do with Lean. There's something I'm missing. Maybe I don't understand .gitignore syntax. It's never been a problem before. Surely I'm doing something silly.

I'm sure there are usual ways that others configure Lean projects to play nicely with git. What are standard practices?

(Many languages have a standard default .gitignore file in github that you can pull in when you create a git repo, but Lean doesn't.)

[Ruben Van de Velde]

Pretty sure lake new creates a gitignore

[Ruben Van de Velde]

You definitely don't want those three files ignored though

[Ruben Van de Velde]

The whole point of the "updating mathlib in your project" instructions is to update them

[Ruben Van de Velde]

Well, maybe not lakefile.lean

[Ruben Van de Velde]

Maybe it would help if you showed the diff, or explained what you mean by messing up the repo on your other computer

[Yaël Dillies]

mars0i said:

But now I have updated files lake-manifest.json, lakefile.lean, and lean-toolchain. And I don't want to commit them because I think that will mess up the same repo on my other computer. (Is that incorrect?)

I add those three filenames to .gitignore and then (this part I really don't understand--it's bizarre) git still thinks they need to be committed.

Putting a file in .gitignore doesn't mean "Don't look at my changes" but "Make as if the files don't exist". If the files already existed, that makes git thinks you have deleted them.

[Yaël Dillies]

mars0i said:

But now I have updated files lake-manifest.json, lakefile.lean, and lean-toolchain. And I don't want to commit them because I think that will mess up the same repo on my other computer. (Is that incorrect?)

It really shouldn't mess anything up with your other computer. If it does, then you've got bigger problems

[Eric Wieser]

Yaël Dillies said:

If the files already existed, that makes git thinks you have deleted them.

I don't think this is true?

[mars0i]

Thanks everyone for those replies.

@Ruben Van de Velde lake new foo creates a .gitignore file in foo/ , but it only contains "/.lake". Maybe that's all it should contain. I'll try committing those three files and see what happens, and report back.

@Yaël Dillies, @Eric Wieser, yes--I didn't expect the files to disappear. Sorry about that--I wasn't very clear. I meant that git status reports

Changes not staged for commit:
  (use "git add <file>..." to update what will be committed)
  (use "git restore <file>..." to discard changes in working directory)
    modified:   lake-manifest.json
    modified:   lakefile.lean
    modified:   lean-toolchain

even though .gitignore contains

/.lake
lake-manifest.json
lakefile.lean
lean-toolchain
.*.swp

Afaik, git should not report those files as modified and needing to be committed given that they are listed in .gitignore.

Anyway, I'll try committing them now and check see what happens when I get on the other computer. I don't know why mathlib stopped working in this repo. Before I reinstalled mathlib, the files all compiled except when I had import Mathlib at the top. Hadn't been long enough for me to expect bitrot :-) .

[mars0i]

lean-toolchain contains

leanprover/lean4:v4.11.0-rc2

Maybe there could be a problem if the other computer has a different version of lean4 installed? And then I have to make sure they're using the same version?

The entries in lake-manifest.json contain a field "rev" whose value is a hashcode or something like that. I wonder whether that depends on details of the installation?

Anyway, I'll find out soon.

[Ruben Van de Velde]

No, that's not how that works. Lake reads those files to figure out what versions of everything to use

[Eric Wieser]

You should certainly not have those files in your gitignore

[mars0i]

Syncing the config files via git worked. import Mathlib caused it to rebuild. That took about 7 hours--it's a slow machine--but now it's all fine. Thanks to everyone.

[Eric Wieser]

You should not have to wait 7 hours; lake exe cache get should take minutes and save you from a long build

[mars0i]

Thanks @Eric Wieser. I thought I remembered something like that, but didn't recall the details.

Part of the issue for me is that there are pretty good instructions for setting up Lean and Mathlib, but that doesn't mean that I know what following the instructions accomplishes. I haven't seen instructions for updating for new versions of either Lean or Mathlib. So it wasn't obvious that reinstalling mathlib creates new versions of config files, and that once those files are copied to a new instance of a repo, I should run lake exec cache get before using Mathlib. I'm sure this seems obvious and intuitive once one has used Lean for a while. I know that explaining to new users everything that installation routines do can be counterproductive. One point of those routines is to make it so that novices don't have to understand the underlying complexity, which may change over time anyway.

[Eric Wieser]

Yes, I guess something missing from the instructions is how to "recover from" an update after transferring a repo between machines.

[mars0i]

What would be helpful would be a short list of common tasks using lake or other tools. We have a set of steps to follow in a couple of different scenarios (use someone else's Lean project, start an entirely new project), and there is lake --help, but it's more difficult to know when to do things when you are not following one of the main scenarios. (e.g. When do I want to do lake update, and what will it do to my project, or to my computer? When and why do i do lake exe cache get?)

[Ruben Van de Velde]

I'd hope you can find some of that at https://github.com/leanprover-community/mathlib4/blob/5d151347c122037259fc129edd18732d0b148f15/README.md , but improvements to the docs are always welcome

[mars0i]

Thanks @Ruben Van de Velde . I've seen that page--it's linked from other setup pages, and links to them. But it doesn't fill in what I'm wondering about. I can't contribute yet--I'm still confused! I just try plausible things until I stop getting error messages. :-)

[mars0i]

In the first post above, I described a puzzling problem whose essence was that I was unable to commit the files that lake had created.

It turns out that the problem was that I had created my new Lean project inside of a larger project. That is definitely what I wanted to do. However, I didn't know that lake new and lake init set up a new git repo, including a .git directory and its contents. That means that when I ran git on the larger project, which now contained the subdirectory that lake created, git was unwilling to incorporate the new Lean project. It saw that the subdirectory had its own .git folder, and wouldn't do anything with the subdirectory.

The solution was to delete the .git folder that lake created, as explained here:
https://stackoverflow.com/questions/56873278/how-to-fix-error-filename-does-not-have-a-commit-checked-out-fatal-adding

(I can't blame Lake for this. It's just something I'd never encountered. Seems very weird if you don't know what's going on, but it's easy to fix once you understand the issue.)

[mars0i]

I'm working on notes for myself on how to set up a project in this way, and will post here for feedback when my understanding seems stable.

[Ruben Van de Velde]

Ah, I see. That's a case we didn't take into account. Do you think it would have helped if https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency noted that the lake new command creates a git repo, or is that not where you were looking? Also, I think lake itself should warn in that case, I'll check if there's an issue filed yet

[Ruben Van de Velde]

Commented on https://github.com/leanprover/lean4/issues/2758

[mars0i]

@Ruben Van de Velde, thanks for adding the comment in the issue, and for noting the remark about creating a git repo on that page. I probably looked at that page at some point, but I didn't use the command listed just above and probably didn't notice the mention of initializing a git repo. Not realizing I'd initialized a git repo caused lots of confusion on my part.

I would rather that the fact that a git repo is initialized be something that jumps out at you. I've got git projects using at least half a dozen languages, and this is the first time that the standard initialization tool also set up a git repo. It's not necessarily bad, but it's unexpected. On the other hand, it's not clear to me why lake should initialize a git repo. Is there some unusual git configuration that Lean needs?

It's not just embedded projects where this matters. In general, lake creating a git repository might not be what a user wants, even if they are going to put their project in git. It is the default behavior at this point, so my feeling is just that it should be very clear that it's the default, and it should be easy to disable it.

My procedure up until now has been, roughly:

• Start playing around with some code, then decide I ought to put it in a git repo.
• Create a repo on github.
• Clone the repo on git to my local machine.
• Maybe use the language's build or initialization tool to set up directories and some config files in the repo.
• Copy some of my source files into the local repo.
• git add the files.
• Push to github.

I don't think I should use that procedure with lake, though. I need to let lake initialize the git repo. So either I have to change my procedure, or lake needs to change. I'm happy to change, but I'm still not sure what to do. However, it would be better if I could just follow a procedure that works with every non-Lean project.

More specifically, I don't know enough about git to know what I should do to connect a Lean repo to a github repo. I did some investigation and tried some ideas that might work, but at this point I'm stuck wondering about the fact that if I create a repo on github, it initializes a .git directory, but lake is also doing that, and I don't know enough to know whether that's a problem. Maybe the answer is that it's not--either .git directory will work--since I know that I can delete the .git directory in a subsidiary Lean project, as discussed previously. There's probably a standard procedure for working with github that Lean users are used to, and I just don't know what it is.

(It's possible that there are lots of other languages where a similar procedure to Lean's is used, and I'm just not used to it. For all I know it's one of those Microsoft-ish culture vs. unix-ish culture things, and I just happen to have spent more time in the latter.)

[Eric Wieser]

Any of these workflows should work fine:

1. Github first

   • Create a repo on github
   • Clone that repo
   • Run lake init inside that repo
   • Push to github

2. Lake first

   • Create a repo with lake new
   • Create an empty repo on github. Don't tick the boxes about licenses / readme / gitignore.
   • Push to github

3. git first

   • Create a repo with git init
   • Create an empty repo on github. Don't tick the boxes about licenses / readme / gitignore.
   • Run lake init inside that repo
   • Push to github

[mars0i]

Excellent--thanks @Eric Wieser ! That's what I needed.

Does it seem reasonable to add that information to one of the setup information pages? I'd be happy to post a PR or edit or whatever's needed, if that would make sense.

[Chris Bailey]

mars0i said:

It's not necessarily bad, but it's unexpected. On the other hand, it's not clear to me why lake should initialize a git repo. Is there some unusual git configuration that Lean needs?

Cargo creates a git repo by default for new projects, but it does provide an additional option --vcs none to disable it. There's obviously a convenience factor that benefits probably a large majority of users, but aside from that I think the benefit is that you get a proper default .gitignore file.

[mars0i]

Ah, OK. I've never used Rust. But it's obviously something that a lot of people use.

[mars0i]

I guess that letting lake create the .gitignore avoids having to maintain default .gitignores on github and gitlab and whatever other sites people might use, or local company servers, etc.

[Chris Bailey]

I think it just prevents people (again probably the majority of users) from having to spend time figuring out what they should put in a Lean 4 .gitignore to not accidentally commit a bunch of build artifacts or dependency data.

[Chris Bailey]

But I agree an extra CLI flag like the --vcs none thing would be a welcome addition.

[Matthew Ballard]

You can make a RFC on the lean4 repository.

[Andrei Zabolotskii]

Hi all,
I'm new to Lean, and I've got a problem with a Github action.
I created a new project as described here https://leanprover-community.github.io/install/project.html#creating-a-lean-project using lake +leanprover/lean4:stable new my_project math. This guide says that I should create a folder MyProject and put files into that folder, but in fact lake has created the folder my_project instead. OK, I renamed that folder to MyProject, adjusted accordingly the import in my_project.lean and default_target in lakefile.lean, and then everything worked.
Then I pushed the project to Github. The project includes the file .github/workflows/lean_action_ci.yml created by lake, and its entire content is:

name: Lean Action CI

on:
  push:
  pull_request:
  workflow_dispatch:

jobs:
  build:
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v4
      - uses: leanprover/lean-action@v1

I guess this causes Github to run some checks. The thing is that the checks fail. The log says:

Run : Lake Build
Lake Build Output
  ✖ [?/?] Computing build jobs
  error: no such file or directory (error code: 2)
    file: ././././MyProject.lean
  Some required builds logged failures:
  - Computing build jobs
  error: build failed
  Error:  lake build failed

Indeed, there is no file MyProject.lean -- there is only my_project.lean.
What should I do to fix this error?

[Julian Berman]

What do you have in your my_project folder now? Renaming anything sounds suspicious. Specifically, here's what I get from running the command on the page:

⊙  lake +leanprover/lean4:stable new my_project math                                                                                                                                                                                                                                                                                                              julian@Mac
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.14.0
info: downloading component 'lean'
Total: 227.2 MiB Speed:  18.4 MiB/s
info: installing component 'lean'
info: downloading mathlib `lean-toolchain` file

~/Desktop
⊙  cd my_project                                                                                                                                                                                                                                                                                                                                                  julian@Mac

~/Desktop/my_project is a git repository on main
⊙  ls                                                                                                                                                                                                                                                                                                                                                             julian@Mac
MyProject  MyProject.lean  README.md  lakefile.toml  lean-toolchain

[Andrei Zabolotskii]

The files list is .gitignore my_project.lean lake-manifest.json lakefile.lean lean-toolchain README.md, and the folders are .github, .lake, and MyProject (which was called my_project before I renamed it). After creating the project I also ran lake update, as per the guide, which added more files, I guess.

[Ruben Van de Velde]

Oh, that's because you didn't follow the instructions

[Ruben Van de Velde]

Why did you run lake +leanprover/lean4:stable new my_project math rather than lake +leanprover/lean4:nightly-2024-04-24 new my_project math as instructed?

[Andrei Zabolotskii]

Cause stable means good, isn't it :flushed:

[Ruben Van de Velde]

Clearly not

[Andrei Zabolotskii]

:-D

[Andrei Zabolotskii]

Anyway, the answer to my question was to rename my_project.lean to MyProject.lean. lake normally creates MyProject.lean, as can be seen from Julian's message, and that's what lake did when I ran it again. Thanks!