Git commit after project creation

Stream: lean4

[Patrick Massot]

@Marc Huisinga after project creation, a git repository is created but with no commit at all. Could you add to the creation script a step that does git add * .gitignore && git commit -m "Project initialization."?

[Patrick Massot]

I used the command with my students yesterday in order to start their mid-term projects and that step felt like boilerplate that should not be done by a human.

[Henrik Böving]

Patrick Massot said:

Marc Huisinga after project creation, a git repository is created but with no commit at all. Could you add to the creation script a step that does git add * .gitignore && git commit -m "Project initialization."?

If you were to run this on a students machine who has never used git before the git commit -m will fail because it is going to ask them about their name and email address so that would have to be configured a priori

[Patrick Massot]

Surprisingly, I didn't observe that.

[Patrick Massot]

But I agree it is really crazy that installing git does not include asking for an editor, a name and a email.

[Patrick Massot]

So I guess we would need to fix that. The project creation script could check whether git is correctly configured and ask questions if not.

[Eric Wieser]

The script could set the author to "Lean VSCode extension" or "leanprover-community-bot" for the purpose of that single commit (via GIT_{COMMITTER,AUTHOR}_{NAME,EMAIL})

[Patrick Massot]

That's also a possibility.

[Scott Morrison]

@Patrick Massot, this request probably deserves an issue on the vscode-lean4 repo, as it's not trivial to even decide what should happen.

[Marc Huisinga]

Yes, please create an issue for this. In the long term, I want to add better general support for detecting broken or incomplete setups and fixing them, but in the short term it may be fine to set the author as Eric described.