We have installation instructions for Windows, Linux, and macOS.
These directions are adapted from the leanprover-community web page.
Windows
These instructions are also covered in a YouTube video. This does not include the "Install Our Logical Verification Repository" step.
-
Install Git for Windows: https://gitforwindows.org/. Accept all default answers during the installation (or, if you would like to minimize the installation, you may deselect all components on the "Select components" question).
-
Start the newly installed
Git Bash
by searching for it in the Windows search bar. -
In Git Bash, run the command
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
. -
Press
[Enter]
to proceed with the installation. -
Run
echo 'PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.profile
. -
Close Git Bash.
-
Download the latest version of python here.
-
Run the downloaded file (
python-3.x.x.exe
) -
Check
Add Python 3.x to PATH
. -
Choose the default installation.
-
Open Git Bash (type
git bash
in the Start Menu) -
Run
which python
- The expected output is something like
/c/Users/<user>/AppData/Local/Programs/Python/Pythonxx-xx/python
. In this case, proceed to the next step. - If it's something like
/c/Users/<user>/AppData/Local/Microsoft/WindowsApps/python
, then- Did you follow the instruction to select
Add Python 3.x to PATH
during the installation?- If not, re-run the python installer to uninstall python and try again.
- Otherwise, you need to disable a Windows setting.
- Type
manage app execution aliases
into the Windows search prompt (start menu) and open the corresponding System Settings page. - There should be two entries
App Installer python.exe
andApp Installer python3.exe
. Ensure that both of these are set toOff
.
- Type
- Close and reopen Git Bash and restart this step.
- Did you follow the instruction to select
- If it is any other directory, you might have an existing version of Python. Ask the TAs for help.
- If you get
command not found
, you should add the Python directory to your path. Google how to do this, or ask the TAs.
- The expected output is something like
-
Run
cp "$(which python)" "$(which python)"3
. This ensures that we can use the commandpython3
to call Python. -
Test whether everything is working by typing
python3 --version
andpip3 --version
. If both commands give a short output and no error, everything is set up correctly.- If
pip3 --version
doesn't give any output, run the commandpython3 -m pip install --upgrade pip
, which should fix it.
- If
- Run
git config --global core.autocrlf input
in Git Bash.
-
in Git Bash, run
pip3 install mathlibtools
-
Install VSCode.
-
Launch VSCode.
-
Go to View > Extensions in the menu (or press ShiftCtrlX) and search for
leanprover
. -
Select the
lean
extension (unique namejroesch.lean
). There is also alean4
extension, but that one does not work for our course. -
Click "install" (in old versions of VSCode, you might need to click "reload" afterwards)
-
Setup the default profile:
- If you're using
git bash
, pressctrl-shift-p
to open the command palette, and typeSelect Default Profile
, then selectgit bash
from the menu.
- If you're using
-
Restart VSCode.
-
Verify Lean is working, for example by saving a file
test.lean
and entering#eval 1+1
. A green line should appear underneath#eval 1+1
, and hovering the mouse over it you should see2
displayed.
-
Close VSCode.
-
Open Git Bash.
-
In Git Bash, use
cd
to go to the directory you want to place the project in (a new folder will be created for it at that location). For instance, you can usecd ~/Documents
to go to your personal Documents folder. -
Run these commands in Git Bash:
leanproject get blanchette/logical_verification_2022 cd logical_verification_2022 lean --make lean
The last command should produce a long list of warnings and errors which you can ignore.
-
Launch VSCode.
-
In the
File
menu, clickOpen Folder
, and choose the folderlogical_verification_2022
(not one of its subfolders). If you used~/Documents
above, it will be located in yourDocuments
folder. -
In the file explorer on the left-hand side, you will find all exercises and homework in the
lean
folder, as we upload them. -
You can retrieve the newest exercises and homework that we upload by clicking the two arrows forming a circle in the bottom left corner.
Debian/Ubuntu and Derivates
These instructions are also in a YouTube video, not including the Logical Verification repository details.
-
Open a terminal, enter the following command and hit enter. (This will take some time.)
wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile
-
You may have to log out and log in again to make sure that the
lean
command is on yourPATH
.
-
Use
cd
to go to the directory you want to place the project in. (A new folder will be created for it at that location.)leanproject get blanchette/logical_verification_2022 cd logical_verification_2022 lean --make lean
The last command should produce a long list of warnings and errors which you can ignore.
-
Launch VSCode, either through your application menu or by typing
code
. -
On the main screen, or in the
File
menu, clickOpen Folder
, and choose the folderlogical_verification_2022
(not one of its subfolders). -
In the file explorer on the left-hand side, you will find all exercises and homework in the
lean
folder, as we upload them. -
You can retrieve the newest exercises and homework that we upload by clicking the two arrows forming a circle in the bottom left corner.
Other Linux Distros
Follow these instructions and proceed by the instructions "Install Our Logical Verification Repository" for Debian/Ubunutu above.
macOS (Intel Macs)
These instructions are also in a YouTube video, not including the Logical Verification repository details.
-
Open a terminal, enter the following command and hit enter. (This will take some time.)
/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile
-
Open a terminal.
-
Use
cd
to go to the directory you want to place the project in (a new folder will be created for it at that location), for example you can use~/Documents
.leanproject get blanchette/logical_verification_2022 cd logical_verification_2022 lean --make lean
The last command should produce a long list of warnings and errors which you can ignore.
-
Open VSCode again.
-
In the
File
menu, clickOpen
, and choose the folderlogical_verification_2022
(not one of its subfolders). If you used~/Documents
above, it will be in theDocuments
folder. -
In the file explorer on the left-hand side, you will find all exercises and homework in the
lean
folder, as we upload them. -
You can retrieve the newest exercises and homework that we upload by clicking the two arrows forming a circle in the bottom left corner.
macOS (M1 Macs / Apple Silicon)
Lean is not yet supported on M1 Macs. Specifically, elan
โ which is otherwise
recommended (and installed) as part of the above instructions โ will not be able
to fetch Lean binaries on these devices.
In the meantime, you can try to set up an Intel installation using Rosetta:
-
Follow the detailed Lean installation instructions, ensuring you use the Intel version of homebrew.
-
Open a Rosetta terminal.
-
Use
cd
to go to the directory you want to place the project in (a new folder will be created for it at that location), for example you can use~/Documents
.leanproject get blanchette/logical_verification_2022 cd logical_verification_2022 lean --make lean
The last command should produce a long list of warnings and errors which you can ignore.
-
Open VSCode again.
-
In the
File
menu, clickOpen
, and choose the folderlogical_verification_2022
(not one of its subfolders). If you used~/Documents
above, it will be in theDocuments
folder. -
In the file explorer on the left-hand side, you will find all exercises and homework in the
lean
folder, as we upload them. -
You can retrieve the newest exercises and homework that we upload by clicking the two arrows forming a circle in the bottom left corner.
There is a Zulip thread with some interim further details and advice. If you have trouble, ask the TAs for help.
Virtual Machine (for Any Operating System)
-
These are the instructions for 2021. They need to be updated for 2022. If you are a student, please talk to one of the instructors before following these instructions.
-
Download and install VirtualBox. (Other virtualization software should also work.)
-
Download the virtual machine,
logical_verification_2021.ova
(3.3G), from Google Drive.SHA256:
c0d002a3bdb4b37ec9e69f6accc2e80846e70253a3e3abe7731436b85b93a854 logical_verification_2021.ova
-
Open VirtualBox.
-
Import the downloaded file via
File > Import Appliance
. This requires around 7GB of disk space. -
Start the virtual machine by selecting
logical_verification_2021
and clicking theStart
button. The virtual machine is configured to use 4 processor cores and up to 5GB of RAM. (You can edit the virtual machine to change these values.) It uses around 4 GB of RAM if you open all the Lean files in VSCode. -
Open VSCode by clicking on the blue ribbon icon on the desktop. VSCode should automatically open the folder
~/logical_verification_2021
. In the file explorer on the left-hand side, you will find all exercises and homework in thelean
folder, as we upload them. -
You can retrieve the newest exercises and homework that we upload by clicking the two arrows forming a circle in the bottom left corner.
-
If you need the password for the virtual machine at some point, it is
love
.