Skip to content

Commit

Permalink
doc: move description of dependencies to the front (#385)
Browse files Browse the repository at this point in the history
  • Loading branch information
mhuisi authored Jan 15, 2024
1 parent a4f66b5 commit ea2e4f3
Show file tree
Hide file tree
Showing 3 changed files with 12 additions and 12 deletions.
10 changes: 5 additions & 5 deletions vscode-lean4/media/guide-installDeps-linux.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
## Dependencies Needed by Lean 4
[Git](https://git-scm.com/) is a commonly used [Version Control System](https://en.wikipedia.org/wiki/Version_control) that is used by Lean to help manage different versions of Lean formalization packages and software packages.

[curl](https://curl.se/) is a small tool to transfer data that is used by Lean to download files when managing Lean formalization packages and software packages.

## Installing Required Dependencies
1. [Open a new terminal](command:workbench.action.terminal.new).
2. Depending on your Linux distribution, do one of the following to install Git and curl using your package manager:
Expand All @@ -7,11 +12,6 @@
3. When prompted, type in your login credentials.
4. Wait until the installation has completed.

## Dependencies Needed by Lean 4
[Git](https://git-scm.com/) is a commonly used [Version Control System](https://en.wikipedia.org/wiki/Version_control) that is used by Lean to help manage different versions of Lean formalization packages and software packages.

[curl](https://curl.se/) is a small tool to transfer data that is used by Lean to download files when managing Lean formalization packages and software packages.

## Restricted Environments
If you are in an environment where you cannot install Git or curl, for example a restricted university computer, you can check if you already have them installed by [opening a new terminal](command:workbench.action.terminal.new), typing in `which git curl` and pressing Enter. If the terminal output displays two file paths and no error, you already have them installed.

Expand Down
10 changes: 5 additions & 5 deletions vscode-lean4/media/guide-installDeps-mac.md
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
## Dependencies Needed by Lean 4
[Git](https://git-scm.com/) is a commonly used [Version Control System](https://en.wikipedia.org/wiki/Version_control) that is used by Lean to help manage different versions of Lean formalization packages and software packages.

[curl](https://curl.se/) is a small tool to transfer data that is used by Lean to download files when managing Lean formalization packages and software packages.

## Installing Required Dependencies
1. [Open a new terminal](command:workbench.action.terminal.new).
2. Type in `/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"` and press Enter to install [Homebrew](https://brew.sh/), a package manager for macOS.
3. Follow the instructions in the terminal.
4. Type in `brew install curl git` and press Enter.
5. Wait until the installation has completed.

## Dependencies Needed by Lean 4
[Git](https://git-scm.com/) is a commonly used [Version Control System](https://en.wikipedia.org/wiki/Version_control) that is used by Lean to help manage different versions of Lean formalization packages and software packages.

[curl](https://curl.se/) is a small tool to transfer data that is used by Lean to download files when managing Lean formalization packages and software packages.

## Restricted Environments
If you are in an environment where you cannot install Homebrew, Git or curl, for example a restricted university computer, you can check if you already have them installed by [opening a new terminal](command:workbench.action.terminal.new), typing in `which git curl` and pressing Enter. If the terminal output displays two file paths and no error, you already have them installed.

Expand Down
4 changes: 2 additions & 2 deletions vscode-lean4/media/guide-installDeps-windows.md
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
## Installing Required Dependencies
[Git](https://git-scm.com/) is a commonly used [Version Control System](https://en.wikipedia.org/wiki/Version_control) that is used by Lean to help manage different versions of Lean formalization packages and software packages.

1. Install [Git](https://git-scm.com/download/win). You can keep all settings in the installer at their default values.
2. Wait until the installation has completed.
3. Restart VS Code and re-open this guide.

[Git](https://git-scm.com/) is a commonly used [Version Control System](https://en.wikipedia.org/wiki/Version_control) that is used by Lean to help manage different versions of Lean formalization packages and software packages.

## Restricted Environments
If you are in an environment where you cannot install Git and it is not already installed, for example on a restricted university computer, there is currently no option to try Lean 4 with a local installation. If you want to try out Lean 4 regardless, you can read [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) and do the exercises with [an online instance of Lean 4 hosted using Gitpod](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). Doing so requires creating a GitHub account. Alternatively, you can also [play the Natural Number Game](https://adam.math.hhu.de/#/g/hhu-adam/NNG4) or [try a single-file version of Lean 4 in your web browser](https://live.lean-lang.org/).

0 comments on commit ea2e4f3

Please sign in to comment.