Git necessary?

Stream: lean4

[Martin Dvořák]

Is it possible to use Lean 4 on Windows 10 without installing Git?

After a fresh install from within VS Code, I get the following error:
Lean4_fresh_install_error.png

I want to make the setup as easy as possible for my students. In particular, command line must be avoided. Most of them probably have Windows 10 on their PC. Is installing Git necessary? I know that Git can be used from GUI, but I would like to know whether they can use Lean 4 without installing Git at all.

[Jannis Limperg]

You can make mathlib a local dependency instead of having Lake fetch it from Git.

[Sebastian Ullrich]

I'm always surprised we don't hear more complaints about this, it's the same story with Lean 3 isn't it? It would be possible to teach Lake to download github.com dependencies as tarballs/zipballs instead, which is faster anyway even at --depth 1.

[Martin Dvořák]

Jannis Limperg said:

You can make mathlib a local dependency instead of having Lake fetch it from Git.

Then I'd have to distribute mathlib4 source code with my project. Or is there a third option?

[Patrick Massot]

Are you looking for an option where mathlib4 teleports onto your students hard drives? That seems difficult to arrange.

[Martin Dvořák]

Patrick Massot said:

Are you looking for an option where mathlib4 teleports onto your students hard drives?

Exactly!

[Martin Dvořák]

I hoped they could install everything by following prompts inside VS Code. If the students have to go to another website
https://gitforwindows.org/
to install another software, some of them will quit.

Is there an alternative? Can they install Git inside VS Code together with Elan?

[Shreyas Srinivas]

Doesn't it work if you just set up the project folder with mathlib + deps and cache already inside it, and then zip the folder and share it?

[Martin Dvořák]

I've slowly realized that I will have to change the workflow. The current instructions for my students are the following:
(1) Download and install VS Code.
(2) Install the lean4 extension inside VS Code.
(3) Download the course repository as a .zip file from GitHub and unpack it (students who know Git can clone instead).
(4) Open the project and then open one of the .lean files.
(5) Follow the pop-up in VS Code to download Elan and install everything automatically.

Unfortunately, step (5) does not install Git with it.

I see two options how to make it work despite of no previous Git installation on their computer:
(a) Add an additional step to download and install Git (doesn't matter when; it can be step (6) for example).
(b) Upload my project as a .zip file including a copy of Std and Mathlib as local dependencies to a different website (and change step (3) to download from that website).

Is there a third option I didn't consider?

[Shreyas Srinivas]

Maybe you could ask students to install git. It is as useful as learning latex if not more, even for mathematics students, especially when writing papers.

[Martin Dvořák]

You suggest (a), don't you?

[Shreyas Srinivas]

Martin Dvořák said:

You suggest (a), don't you?

Yes. My reasoning is that they will need it sooner or later. It also has uses beyond lean for anyone producing anything on machine which is text based.

[Martin Dvořák]

In fact, they will not learn any Git skills; they will just install Git and the Lean file will suddenly compile, instead of the error from the original post.

[Martin Dvořák]

Potentially I could add the Git installation step before step (3) and make them git clone instead of downloading the .zip file from GitHub. However, I am worried that even more students would quit then.

[Shreyas Srinivas]

Martin Dvořák said:

In fact, they will not learn any Git skills; they will just install Git and the Lean file will suddenly compile, instead of the error from the original post.

I don't see this as a negative. I never learnt git beyond what I could by googling what I wanted to do for a few years. Even learning git add, git commit, etc is a good start. They'll pick up on the rest as the need arises.

[Patrick Massot]

Shreyas Srinivas said:

Maybe you could ask students to install git. It is as useful as learning latex if not more, even for mathematics students, especially when writing papers.

This claim is completely wrong. Almost all professional mathematicians know LaTeX and almost none of them know git. This is even true is the super computer nerd-biased sample of mathematicians interested in Lean (look at how many people struggle with git when they arrive here).

[Yaël Dillies]

It's not because nobody does it that it isn't useful.

[Patrick Massot]

What I wrote proves that LaTeX is necessary and git isn't.

[Martin Dvořák]

Shreyas Srinivas said:

Even learning git add, git commit, etc is a good start.

I am not talking about teaching them git add and git commit. I am talking about just having Git installed on their computer.

[Patrick Massot]

I really like git, I have been using it long before using Lean, and I was using svn before. But it simply isn't necessary for mathematicians.

[Yaël Dillies]

Patrick Massot said:

What I wrote proves that LaTeX is necessary and git isn't.

Agreed, and that's not what Shreyas said.

[Shreyas Srinivas]

Patrick Massot said:

This claim is completely wrong. Almost all professional mathematicians know LaTeX and almost none of them know git. This is even true is the super computer nerd-biased sample of mathematicians interested in Lean (look at how many people struggle with git when they arrive here).

I am not saying it is necessary. I am saying it is very useful

[Patrick Massot]

You wrote "It is as useful as learning latex if not more", which is simply false.

[Patrick Massot]

It's not a big deal, I only wanted to inform you that you have a big misconception here.

[Martin Dvořák]

No matter whether students install Git first (and then VS Code) or VS Code first (and then Git), they will not have to "show VS Code where Git is", right?

[Shreyas Srinivas]

Patrick Massot said:

You wrote "It is as useful as learning latex if not more", which is simply false.

I mean more useful than in the following two senses:

1. It is useful beyond latex. If you want to code in addition to organising writing work, which a lot of applied math people do these days (I recall in my MFoCS days that the MMSc people in Oxford hardly ever proved things. Simulations were their bread and butter, at least some of them).
2. It would significantly improve the drafting process with Latex for everything from assignments to papers.

[Eric Wieser]

Maybe you could ask students to install git. It is as useful as learning latex if not more

Ignoring the value judgment in the second half of this quote; in my experience almost all the students using LaTeX in my lab hasn't actually installed LaTeX. Overleaf has gotten a pretty good monopoly

[Patrick Massot]

Ok, I won't try to get you out of your imaginary world then.

[Martin Dvořák]

Martin Dvořák said:

No matter whether students install Git first (and then VS Code) or VS Code first (and then Git), they will not have to "show VS Code where Git is", right?

They just have to install both on the same computer and, poof, it will magically work, right?

[Shreyas Srinivas]

I am sorry, I am not trying to argue against your point. You are almost certainly correct about how students work in practice. I am just pointing out that the grass is greener on the other side

[Shreyas Srinivas]

Martin Dvořák said:

They just have to install both on the same computer and, poof, it will magically work, right?

This has been my experience on linux and mac.

[Martin Dvořák]

Shreyas Srinivas said:

This has been my experience on linux and mac.

Thanks! Can somebody confirm that Windows 10 with https://gitforwindows.org/ works the same way?

[Yaël Dillies]

It does.

[Yaël Dillies]

I forgot my laptop charger in Cambridge over the holidays, so I had to install the whole python, git, elan, leanproject, lake thing over again on two different computers, and both time the git installer Just Worked.

[Martin Dvořák]

Nevertheless, I am a bit unhappy that I will force students to install Git in addition to VS Code with then lean4 extension and Elan.

However, it is probably the lesser evil, isn't it?

[Yaël Dillies]

Well, you can always learn how to write installers. That would be useful to the whole community but I have no idea how hard it is.

[Martin Dvořák]

On which level would it be best to do it?
(a) Installer installs all of VS Code, Git, and the Lean ecosystem.
(b) Elan installs Git in addition to the things it currently installs.
(c) VS Code lean4 extension installs Git in addition to Elan upon opening a Lean file.

[Eric Wieser]

The problem with any of these options is that they can easily make a mess of systems that already have vscode or git

[Huỳnh Trần Khanh]

I'm a Coq user. OPAM always does a check to find installed version control software and prints warnings. Lake should print a message telling users to install Git instead of a command not found message. standard disclaimer: not expert advice, merely my opinion

[Martin Dvořák]

If I want a setup that uses .olean files instead of building Mathlib on my (student's) computer (which are downloaded by a different program afaik), do I nevertheless need to download the .lean files using Git?

[Martin Dvořák]

I added Git installation as the first step for my students who want to have Lean on their computer.

[Joe Hendrix]

Has anybody tried libgit2 or perhaps another git library? Lake could potentially be linked against a git library to avoid the command line dependency.

[Henrik Böving]

But how are you going to get libgit2 onto a windows machine without an additional install procedure?

[Joe Hendrix]

@Henrik Böving I was thinking if lake used a git library, the build of it that elan uses could be statically linked against that library. Elan could also download git, but that seems a little stranger.