Mathlib.dmg installation?

Stream: general

[Alex Kontorovich]

We've had a few more experiences at the Simons workshop of mathematicians trying to install Lean+Mathlib locally, and it's still full of paper cuts. If we want lots of mathematicians to work formally (whether to contribute to Mathlib or not!), and to do this on their own, it would really help to be able to download Mathlib the same way I now download Mathematica. I would google "Mathlib", find a website called https://mathlib.org (not "lean prover dash community dot github io" etc...), and there would be a big, prominent button right at the top called "Download Mathlib v4.20.1" (or whatever). When I click that button, my Mac would download a file called Mathlib.dmg. I double click on that, and I see an app called Mathlib and an arrow for me to drag it into my Applications folder (or maybe there's a longer installation process, but installation is completely managed by some script). I then go to my Applications folder, double click on Mathlib, and the app opens up. Secretly (I don't want to know any of this, I just want it to work!) the app is just a wrapper of VSCode, configured to come with the Lean4 extension installed, and Mathlib downloaded, including the oleans.

I asked an LLM how this could be implemented, and this was its response (way above my paygrade to tell if it's right, but doesn't seem impossible for someone with some coding chops?):

Here's a step-by-step approach for creating a Mac installer:

Phase 1: Prepare the Bundle

Step 1: Set up a clean Lean/Mathlib environment

# Start fresh
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
elan install leanprover/lean4:stable
lake new mathlib_bundle
cd mathlib_bundle
# Add mathlib dependency to lakefile.lean
lake update
lake exe cache get  # Download precompiled oleans

Step 2: Download and customize VS Code

• Download VS Code for Mac from Microsoft
• Install the Lean 4 extension
• Configure default settings (theme, keybindings, workspace layout)
• Export the configuration files (settings.json, keybindings.json, etc.)

Phase 2: Create the Application Bundle

Step 3: Build the app structure

mkdir -p Mathlib.app/Contents/{MacOS,Resources,Frameworks}

Step 4: Copy VS Code into your bundle

# Extract VS Code and put it in your app
cp -r "/Applications/Visual Studio Code.app/Contents/" Mathlib.app/Contents/

Step 5: Bundle Lean + Mathlib

# Copy your prepared Lean environment
cp -r ~/.elan Mathlib.app/Contents/Resources/
cp -r your_mathlib_project Mathlib.app/Contents/Resources/mathlib_workspace

Step 6: Create launch script Create Mathlib.app/Contents/MacOS/Mathlib:

#!/bin/bash
export LEAN_PATH="$PWD/../Resources/.elan"
export PATH="$PWD/../Resources/.elan/bin:$PATH"
cd "$PWD/../Resources/mathlib_workspace"
exec "$PWD/../MacOS/Electron" .

Step 7: Create Info.plist Create Mathlib.app/Contents/Info.plist with app metadata.

Phase 3: Package as DMG

Step 8: Create the DMG

hdiutil create -size 2g -fs HFS+ -volname "Mathlib" temp.dmg
hdiutil attach temp.dmg
cp -r Mathlib.app /Volumes/Mathlib/
# Add background image, arrange icons nicely
hdiutil detach /Volumes/Mathlib
hdiutil convert temp.dmg -format UDZO -o Mathlib.dmg

Key files you'll need to customize:

• Modify the VS Code settings to point to your bundled Lean
• Update the Lean extension configuration to use your workspace
• Set default file associations for .lean files

The trickiest part is ensuring the bundled Lean installation works with relative paths and doesn't depend on system-wide installations. You might need to patch some configuration files or use environment variables to redirect paths.

This approach essentially creates a portable VS Code installation with everything pre-configured and bundled.

[Marc Huisinga]

Could you say more about which paper cuts you encountered with the installation? We probably want to fix these regardless.

[Aaron Liu]

Do you want it to also set up a fresh Lean project that depends on mathlib?

[Alex Kontorovich]

Papercut # 1: Where's Waldo (what link to press for installation) on the landing page?
image.png

[Alex Kontorovich]

Papercut # 2: If you find the link to installation (bottom of last image), you land on this page. How quickly do your eyes go to the "instructions in the official Lean project"?
image.png

[Aaron Liu]

Alex Kontorovich said:

Papercut # 2: If you find the link to installation (bottom of last image), you land on this page. How quickly do your eyes go to the "instructions in the official Lean project"?
image.png

Very fast, since you put a big red circle around it

[Alex Kontorovich]

Papercut # 3: Now I've clicked three links, and the first step in the Quickstart is to... click another link (to download VSCode), and go to another page (which doesn't pop out in a new tab, so I've lost the leanprover page and will need to find it again when VSCode installation is done).
image.png

[Alex Kontorovich]

Papercut # 4 : If I managed to download and install VSCode, and again find the same 3 clicks to get back to the leanprover installation page, the instructions are ... to follow more instructions elsewhere!?!
image.png

[Bolton Bailey]

Alex Kontorovich said:

Papercut # 1: Where's Waldo (what link to press for installation) on the landing page?
image.png

There's also an "installation" header on the left side bar, which is where I would expect people to look for it.

[Aaron Liu]

Bolton Bailey said:

Alex Kontorovich said:

Papercut # 1: Where's Waldo (what link to press for installation) on the landing page?
image.png

There's also an "installation" header on the left side bar, which is where I would expect people to look for it.

Yes, but unfortuanately that's off to the side and hidden away if your screen isn't wide enough

[Alex Kontorovich]

The three topics under the "installation" header are:

• "Getting Started" (sounds like it'll be an introduction, not download instructions),
• "online version" (great, but now I'm at the point that I actually want to install it on my machine and use it), and
• "using lake" (???).

[Shreyas Srinivas]

One question I immediately have on seeing this dmg idea is : how many vscode copies are people going to install if they unpack this dmg? Everytime users start a project?

[Bolton Bailey]

It is a bit :upside_down: that there is a subheading under "installation" that says "(no installation)"

[Shreyas Srinivas]

Also, if this is a workshop, I would say that setting up a sample "template" repository on github is the best way to go.

[Shreyas Srinivas]

For instance if you want all the blueprint and CI bells and whistles, go to this link : https://github.com/pitmonticone/LeanProject

[Shreyas Srinivas]

create your own repository by clicking on "use this template"

[Shreyas Srinivas]

and then open your repository in codespaces (the green button just above the code files on the top like so:

[Shreyas Srinivas]

Screenshot from 2025-06-24 17-38-00.png

[Shreyas Srinivas]

(CC : @Pietro Monticone : could we have the devcontainers set up to make codespaces work with everything by default on the template)?

[Bolton Bailey]

Shreyas Srinivas said:

and then open your repository in codespaces (the green button just above the code files on the top like so:

I don't see the second green button over the file listing when I visit this repository

[Shreyas Srinivas]

The key limitation is that github will want you to pay for using this service after some point. But this is often much longer than a workshop

[Shreyas Srinivas]

The second green button from the left? the one that gives you the clone link?

[Bolton Bailey]

Screenshot 2025-06-24 at 11.40.35 AM.png
This is what I see

[Bolton Bailey]

Ah is it the other tab in the clone button, ok I see that.

[Bolton Bailey]

I thought you were saying the right hand green button was what I needed.

[Shreyas Srinivas]

I have an extra button on mine. But you also have the green button.
show.jpg

[Shreyas Srinivas]

Anyway, this particular repository doesn't appear to be setup to fetch the cache and install the lean extension. But fixing this wouldn't be too difficult.

[Mario Carneiro]

Both the lean and community web pages have issues here. lean-lang.org has this entirely-too-big logo
image.png

Compare with vscode:
image.png

Front and center is a one click install

[Mario Carneiro]

I think one reason we are hesitant to put the big press-me button on lean websites is because installation is actually a somewhat subtle business; it depends on whether you want to have vscode bundled with lean or if you already have your own vscode or vscodium or something else. We would need to have a transition path for people who picked the wrong choice at the start

[Mario Carneiro]

maybe a few options are okay?

[Lean + Mathlib + VSCode bundle] [Lean + Mathlib, I already have VSCode]
subheader mini text: [I use another editor] [Lean only] [detailed instructions]

[Mario Carneiro]

or maybe it would be better to have a single button to start but then it runs an installer script that gives you more options after it notices e.g. that you already have vscode installed

[Bolton Bailey]

(website#657) to address the install-without-installation issue

[Matthew Ballard]

Related question: what happened with WASM?

[Marc Huisinga]

Matthew Ballard said:

Related question: what happened with WASM?

#general > Pitch for Webassembly support (and follow-up projects) @ 💬

[Alex Kontorovich]

Shreyas Srinivas said:

One question I immediately have on seeing this dmg idea is : how many vscode copies are people going to install if they unpack this dmg? Everytime users start a project?

What I'm proposing is a completely different usage of Lean+Mathlib from what almost everyone on Zulip is doing. The vast majority of the people here are looking to contribute to Mathlib. It is extremely important to have big, beautiful, interconnected libraries on top of which to do mathematics. But some people (in fact probably the vast majority of mathematicians?), if they want to interact with Lean at all, will just want to do math in a formal system, without worrying about doing it in the "right" generality or with perfectly written code. And I think we should encourage/support this as well.

Compare to how I currently use Mathematica: There's a big library of functions that allow quick computations; I open a new file, define new functions, compute something, do whatever I want. Then later I open a new file for some other reason and start over. Maybe I'll import my old file in the new file, if I want to reuse a computation (or just copy-paste). I'm not PRing my work to Mathematica (nevermind that they're not open source), but when I write a paper, I can add a link to a github page storing my Mathematica file, so others can check that I've done what I claimed.

This discussion is also motivated by this slide in my "Big Proof" talk...
image.png

[Alex Kontorovich]

That is, vastly more mathematicians can/should be doing research on top of Mathlib, without necessarily contributing what they do to Mathlib. (This has all kinds of issues. Version tracking, stability across time, etc. Other people can come later, and get whatever was done into Mathlib...)

[Alex Kontorovich]

But we have to meet them where they are, not insist that they develop a whole slew of new skills they don't currently have / want...

[Julian Berman]

This is maybe asking for something similar to trylean (which existed for Lean 3 and I think doesn't / hasn't for Lean 4 yet) isn't it? C.f. a recent #general > trylean bundle for lean4

[Julian Berman]

(Random mac software info by the way is that if you don't know how to make a DMG but want to make one anyway to try this / something out, I think https://c-command.com/dropdmg/ is the usual software for doing so if you're not going to figure out how to do it manualy -- though it's not free!)

[Alex Kontorovich]

Is trylean similar to just live.lean-lang.org / codespaces / gitpod? Those are good, but if the internet is going slowly, it gets frustrating. It'd be nice to have something people can quickly download and run locally, even if it's not the "professional" workflow...

[Julian Berman]

trylean was run locally (at least as far as I know -- I haven't used it I just recall seeing it discussed a few times), so not like the web services like live.lean-lang or gitpod -- to my read it's something sort of exactly what your first message says modulo some details like precisely whether VSCode is fully hidden from the user and called Mathlib or whatever. Patrick Massot I'm sure will have info/opinions on this topic broadly

[Mario Carneiro]

yes you are describing exactly what trylean is supposed to be

[Yaël Dillies]

@Jz Pan made a Try4Lean bundle

[Shreyas Srinivas]

Alex Kontorovich said:

Shreyas Srinivas said:

One question I immediately have on seeing this dmg idea is : how many vscode copies are people going to install if they unpack this dmg? Everytime users start a project?

What I'm proposing is a completely different usage of Lean+Mathlib from what almost everyone on Zulip is doing. The vast majority of the people here are looking to contribute to Mathlib. It is extremely important to have big, beautiful, interconnected libraries on top of which to do mathematics.

But some people (in fact probably the vast majority of mathematicians?), if they want to interact with Lean at all, will just want to do math in a formal system, without worrying about doing it in the "right" generality or with perfectly written code. And I think we should encourage/support this as well.

Compare to how I currently use Mathematica: There's a big library of functions that allow quick computations; I open a new file, define new functions, compute something, do whatever I want. Then later I open a new file for some other reason and start over. Maybe I'll import my old file in the new file, if I want to reuse a computation (or just copy-paste). I'm not PRing my work to Mathematica (nevermind that they're not open source), but when I write a paper, I can add a link to a github page storing my Mathematica file, so others can check that I've done what I claimed.

This discussion is also motivated by this slide in my "Big Proof" talk...
image.png

I am not one of those people who regularly contributes to mathlib. In fact most lean projects I am aware of are in the CS domain and we share the same interests that you mentioned. In some areas of CS it is common to use theorem provers as notebooks or whiteboards. So I relate to this.

The way I solve this issue currently is to have a math downstream project that I call scratch. It serves as my notebook for every little experiment that I do. The trylean bundle some have suggested here is the closest approach that works offline with less setup time than the scratch project approach.

[Shreyas Srinivas]

You mentioned dmg. I assume you are on a recent Mac. In that case gitpod desktop might work. I hope they get it working on other OSes

[Dan Velleman]

I agree with @Alex Kontorovich . I'll add one more feature of the installation process that I find unsatisfactory. The Setup Guide asks me to open a terminal and type /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)". I'm told that this will install something called Homebrew. Then I'm told to make sure I add brew to my PATH.

I suspect that the average mathematician who uses a Mac never uses the command line. They may not know what a terminal is. The command they are asked to type is complete gibberish. They are likely to wonder: Is it safe? If I get it wrong will it completely screw up my computer? The fact that what is being installed is called "homebrew" doesn't instill confidence--it doesn't sound like a reliable, professional piece of software. And what's a PATH, and what does it mean to add something to it?

I would guess that many mathematicians would stop at this point and decide that it's not worth it to try to install Lean.

[Jz Pan]

Yaël Dillies said:

Jz Pan made a Try4Lean bundle

It's here #general > My version of offline mathlib help and TryLean4 Windows @ 💬 it's a complete standalone installation of VSCode+git+elan+lake+lean+mathlib with a demo project importing mathlib, configured with launch script + environment variables so it doesn't write to default user config directory. But currently it only works on Windows.

[Jz Pan]

"complete standalone installation" means that you can run lake update at the expense that it needs Internet connection. Otherwise it's completely offline.

[Julian Berman]

Dan Velleman said:

I suspect that the average mathematician who uses a Mac never uses the command line. They may not know what a terminal is. The command they are asked to type is complete gibberish. They are likely to wonder: Is it safe? If I get it wrong will it completely screw up my computer? The fact that what is being installed is called "homebrew" doesn't instill confidence--it doesn't sound like a reliable, professional piece of software. And what's a PATH, and what does it mean to add something to it?

As of very recently Homebrew has a .pkg installer. I haven't tried it yet, but probably one of us should, at which point that instruction should go away in favor of "click this link and then click the pkg installer" and then there's no terminal. (EDIT: this regardless of the fact that yeah I agree with lots of the other papercut suggestions, I'm sure PRs are welcome.)

[Marc Huisinga]

Another option might be to throw out the use of Homebrew entirely and replace it with Apple Command Line Tools (i.e. xcode-select --install). I'm not a macOS user - my understanding is that Apple Command Line Tools can be significantly out-of-date, but perhaps having a git that's a couple of years old is not a deal-breaker? Are there any other potential caveats that I am missing?

I'm definitely happy to replace the macOS instructions with something simpler that works similarly well.

[Shreyas Srinivas]

I think the solution here is to build a cross platform GUI installer that checks everything and allows starting a scratchpad math project in a standard directory (so that people don’t go looking for the vscode icon)

[Vlad Tsyrklevich]

Do we actually need homebrew? https://leanprover-community.github.io/install/macos.html gives a one-liner you can run in the terminal and I don't see anything in that script that requires it, but perhaps its downstream?

[Shreyas Srinivas]

@Alex Kontorovich : I must mention that my suggestion is only a band aid. It will get the basic setup installed. A graphical interface is necessarily limited and cannot cover every edge case scenario. In case something goes wrong, there is bound to be some suggestion to "paste and run the following command in a terminal". Lean exists and works in an ecosystem of other software and can only hide this to some extent and not reinvent the wheel. I would classify things like using CLI and git as essential (though imperfect) tools of the trade that can be hidden, but only upto a point.

[Floris van Doorn]

Bolton Bailey said:

(website#657) to address the install-without-installation issue

website#663 goes further and addresses papercuts 1, 2 more (though probably not perfectly), and removes one click from papercut 3.

[Kim Morrison]

Just noting a critical step of preparing "one click" installers that has been a hurdle before: whoever makes it also needs to make the CI tests that verify that it still works! Convincingly doing this for one click installers is challenging. But without this, they rot and cause havoc.

[Marc Huisinga]

Vlad Tsyrklevich said:

Do we actually need homebrew? https://leanprover-community.github.io/install/macos.html gives a one-liner you can run in the terminal and I don't see anything in that script that requires it, but perhaps its downstream?

It's not clear to me whether Git is always installed on macOS. From what I can find, the pre-installed one needs to be activated e.g. by calling git version on the command line once and then choosing to install it, i.e. it is not ready-to-go out of the box? I'd be grateful if a macOS expert could chime in.

[Julian Berman]

It's not preinstalled, it's just installed with CLT

[Marc Huisinga]

Thanks :-) Then I assume the linked installation script on the community website is incomplete, too?

[Julian Berman]

As for that script -- it's been awhile since I'd looked at it, it certainly used to use homebrew to install CLT then to install both elan and VSCode. I knew that it was changed at some point to no longer use brew to install elan (though I don't recall why). I didn't know it no longer was being used to install VSCode (EDIT: looks like https://github.com/leanprover-community/mathlib4/commit/006e993bcecfe563273d5066c8a4b36f81a6306c was what did it with the commit message saying explicitly it was to avoid needing homebrew). As a user that makes me uncomfortable but I'm not the target audience, so for the audience Alex was talking about they for sure don't care...

[Julian Berman]

Marc Huisinga said:

Thanks :-) Then I assume the linked installation script on the community website is incomplete, too?

Possibly, do we not have CI for it, I guess even if we did it's tricky because GH Actions runners have homebrew preinstalled, presumably there's some way of getting something more vanilla...

[Marc Huisinga]

Julian Berman said:

It's not preinstalled, it's just installed with CLT

Are there any caveats you can think of for replacing our instructions to install brew and installing Git through it with instructions to install CLT?

[Julian Berman]

No that seems reasonable sounding to me I think

[Marc Huisinga]

Thanks. I'll do that after my vacation then. It's probably not a good idea to make significant changes to our installation process in VS Code just before I leave for a couple of weeks.

[Alex Kontorovich]

This was certainly another papercut! We had installed VSCode and the lean extension. Then we needed to install Git. But to get Git, we needed to install Homebrew. Argh! Again, many layers of recursion, each a failure point... Ideally the script would check: is Homebrew installed? (If not, install it.) Is Git installed? (If not, install it) etc...

[Dan Velleman]

To me, this is the worst papercut of all. I don't mind asking users to install VSCode themselves. That installation is easy--it works the way users expect. It's probably a good thing for new users to understand that, when they are using Lean, the application they will be running is VSCode. So it makes sense to say to them "you're going to need VSCode, so install that first." And installing the lean extension is also easy--just click on an "install" button and it's done. It's the rest of the installation that is suddenly much harder and confusing. If we could just automate that, I'd be happy.

[Marc Huisinga]

@Dan Velleman Is it just the dependency step that you find to be difficult, or is installing Elan and setting up a Lean project difficult as well (i.e. the steps after that)?

[Dan Velleman]

@Marc Huisinga For me, the most important thing is that installing the dependencies and Elan should be a single, automated step. It would be best if users didn't need to open a terminal at all, and if they didn't need to know anything about homebrew, git, and curl.

Setting up a Lean project could be included in that step too, but I think that's less important. Different users may want different things--some will want to open an existing project (perhaps a project that comes with the book they are reading) and some will want to create a new project, either depending on Mathlib or not. We already have the "New Project" and "Open Project" commands in VSCode. I haven't played with those much, but if they're user-friendly enough, then perhaps there is no need to include setting up a project in the installation step. After all, installing Lean and setting up a project are, conceptually, two different things.

[Marc Huisinga]

Thanks :-)

I think we could combine those steps on macOS and provide a detailed description on the side of what the combined installation button does for users who like to understand what will be installed by a single button press.
It'll be a bit trickier on Windows, since everyone usually uses the Git GUI installer. I suppose we could install Git through winget nowadays, though?
Linux will be very distro-dependent, but perhaps we could special-case it for a bunch of common distros.

I'll look into these in a couple of weeks when I'm back from vacation.

[Niels Voss]

I noticed that Lean ships with a leanc program which is just an isolated version of clang. This gave me the idea (and this is just an idea, not a proposal) that we could do the same for git, and make a leangit program available in PATH instead of requiring the user to install their own. The idea is that only lake would use leangit, and if someone wanted to contribute to mathlib they would install their own version of git much later when they aren't being overwhelmed by the installation process for Lean

Pros:

• Easier installation process, and we don't have to worry about checking whether the user already has git installed. Some users have git installed but not added to PATH, which might be hard to detect.
• leangit goes away when uninstalling Lean. I'm often uncomfortable when programs install their own system dependencies that aren't isolated to the directory of the program I install.
• Users may or may not want to customize the installation settings for git, especially on Windows, and this deprives them of the ability to do so. For example, users might want/not want Unix utilities added to PATH.

Cons:

• This increases the size of Lean. I just checked, and the portable (aka "thumbdrive edition") version of git for windows is 64MB compressed/416 MB uncompressed (probably because it bundles a Unix environment). Lean is about 1.7 GB right now, so this would increase the size of Lean by about 25% (on Windows, probably less on other OSes where git takes up less space). This cost would be per toolchain as well.
• Giving users the ability to configure whether they want Lean to manage the git installation might cause more issues than it solves.
• User who install a newer version of Lean which would manage git but then want to check out a project using an older version of Lean would still need to install git manually.
• There's the question of whether leangit should share the users git config and login credentials.

[Shreyas Srinivas]

Please let's not have a lean managed git (or vscode for that matter) for all the cons you listed above plus the fact that it doesn't actually save any trouble users might have with git CLI. The standard git installation can at least be updated through the package manager

[Niels Voss]

From my understanding, the reason users need to install git is because Lake needs it to download dependencies like Batteries, Aesop, and Mathlib. I would say that many new users to Lean have no idea what git even is. If Lake didn't need git I would say that we shouldn't tell people to install git at all unless they plan on contributing to (not just depending on) mathlib. So, users would not interface with leangit at all directly, the same way they don't interface with leanc.

Also, I know git is pretty good on backward compatibility, but wouldn't it be more stable if any two users with the same version of lake were also guaranteed to have the same version of git?

[Niels Voss]

Actually, does anyone have a rough estimate of what percent of new Lean users need to clone a git repository themselves (e.g. contributing to Mathlib, FLT, or MIL) the moment they install Lean, as opposed to starting a new project for a class or just making some scratch files that depend on Mathlib?

[Shreyas Srinivas]

I think the problems with a lean managed anything are best exemplified by the Isabelle managed vscodium that is unusable for anything except Isabelle (arguably even for Isabelle). Every year they package a specific version of vscodium. You can’t install any incompatible extensions on it. Even more if you perform manual installation, as vscode moves ahead roughly one version per month, managing the extension can become difficult.

[Shreyas Srinivas]

There are plenty of good tooling options for git+github like GitHub desktop for example, that may not work so well or require custom configuration to work with lean git. Git installation is not as hard as it used to be. Just bundling platform specific install scripts behind a GUI would be better.

[Alex Kontorovich]

The rest of the conversation is over my head, but I'll just chime in with: Git installation may have been even more difficult in the past, but it's still very difficult now for pure mathematicians who just want to "prove some theorems" and are immediately turned off when, after overcoming the VSCode and Lean4 extension instructions, they then have to figure out how to install Homebrew, to install Git...

[Niels Voss]

Yeah I definitely agree Lean should not manage a VSCode install (except maybe in the try Lean bundle). The difference is that leangit would be an implementation detail of lake so it wouldn't need to be updated regularly, whereas a Lean managed VSCode would be bad because it is not an implementation detail

[Mario Carneiro]

If the only thing you are doing is downloading dependencies, lake could plausibly support that without git, by just downloading the source tarball. For creating a new project it needs git though; it could proceed without creating a git project but this sounds like a configuration error in the making

[Niels Voss]

What's the problem with making a lake project without git?

If Lean could operate without depending on git, that might be for the best, although that sounds like a lot of work to make happen and it might not be worth it. (One issue is that lake might current rely on git for downloading private dependencies)

[Jz Pan]

But how to download or update mathlib dependencies without git?

[Kenny Lau]

Maybe we can host weekly releases :slight_smile:

[Shreyas Srinivas]

You will end up reinventing a half baked version of git

[Shreyas Srinivas]

Providing a uniform gui installer solves the installation problem, but the fact remains that git is a tool of this trade and sooner or later basic proficiency in it will become important.

[Shreyas Srinivas]

For the use case Alex is describing, a trylean bundle or installer is the best bet and it won’t be foolproof by a long shot.

[Niels Voss]

Shreyas Srinivas said:

the fact remains that git is a tool of this trade and sooner or later basic proficiency in it will become important.

That's fair, but I think the idea is that you should be able to learn Lean first and the learn git later. Plus some people I know only use GitHub desktop and don't ever install a CLI version of git, and I think that's perfectly valid.

But yeah I agree that there are some problems with the Lean managed git. The universal installer fixes some of them, but I hope that if this is the approach we use, the installer remains transparent about what it is actually installing (a message like "We will now automatically install git, a program that Lean needs to use Lean libraries like Mathlib" would suffice) and have a plan to deal with esoteric git installations on windows (for example, one of the options during the Git for Windows install is to not add git to PATH and only make it available in git bash)

[Mauricio Collares]

The obvious-but-hard solution is to ship libgit2 with Lean and have Lake use that instead of running git.exe. Creating libgit2 bindings for Lean seems like a fun project.

[Shreyas Srinivas]

Mauricio Collares said:

The obvious-but-hard solution is to ship libgit2 with Lean and have Lake use that instead of running git.exe. Creating libgit2 bindings for Lean seems like a fun project.

That would be lovely as long as the developer commits to maintain the bindings and keep them compatible with the latest version of libgit2

[Jz Pan]

Have you heard SWIG? It is a software which automatically generates bindings of C/C++ library to other languages. Maybe we can add a Lean4 support to it, or reimplement it using Lean.