10. Appendix 1: Set Up

10.1. Installing Lean

10.1.1. Windows

1. Install Visual Studio Code for Windows:

   1. Get it here: https://code.visualstudio.com/download
   2. Select the 64-bit system installer for Windows
   3. Do NOT launch Visual Studio Code when you’re done

2. Install Git for Windows:

   1. Get it here: https://gitforwindows.org/
   2. Accept the default installation settings except for the following two:
   3. Select Visual Studio Code as git editor
   4. Select Use Git and optional tools from the command prompt

3. Configure git

   1. Launch a Git Bash “terminal” window (you just installed this program)
   2. Run the following two commands. Leave out the $ signs and substitute your name and email address for those in the following example:

   $ git config --global user.name "Emma Paris"
   $ git config --global user.email "eparis@atlassian.com"
   

   3. exit from the git bash terminal window

4. Install the Lean Prover

   1. Launch a “Git Bash” terminal window
   2. Cut and paste the following one-line command into the terminal window and hit enter to run it (be sure here and below to select and copy the entire command, which scrolls past the end of the screen):

   curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
   

   3. Select (1) Proceed with installation (default), and hit ENTER
   4. You should see: “Elan is installed now. Great!” and some instructions
   5. Exit from the bash terminal window.

5. Tell Windows where to find the Lean Prover.

   1. Open a new Git Bash terminal window
   2. Cut and paste the following command into the terminal window and hit Enter to run it:

   echo 'PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.profile
   

   3. Exit from the terminal window.

6. Launch and Configure VS Code

   1. Click on the “Extensions” icon in the view bar at the left and search for lean
   2. Select the Lean extension for VS Code, click “install”, then “reload” to restart VS Code
   3. Press ctrl-shift-p (depress the ctrl and shift keys and while holding them down, press the P key. This will open the VS Code command palette. Search for, and then select, “Terminal: Select Default Shell”, then select git bash from the menu

7. Test your installation.

   1. Create a new empty directory on your machine
   2. use File > New in VS Code to create a new file
   3. use File > Save As to save it in the directory you just created, giving it the name “temp.lean” (without quotation marks)
   4. enter “#check 1” as the first and only line of logic in the file.
   5. If Lean is running, you will see that #check is underlined in blue and that if you hover your mouse cursor over it, it will tell you that the type of 1 is nat (blackboard font N).

10.1.2. Mac/OSX

1. Install Git on your machine if it’s not already installed. To find out, open a terminal window and type the command, git –version. If it tells you a version number, you’re done If git isn’t installed, install it from here: https://sourceforge.net/projects/git-osx-installer/files/. Alternatively, you might wish to install (and you will eventually appreciate) XCode, a large collection of programming tools for OSX, including git. To get it, go the Mac App Store, search for XCode, and install it. It takes a while to install.

2. Configure git by running the following two commands in an OSX “terminal” window. Leave out the dollar signs and substitute your name and email address for those in the following example:

   $ git config --global user.name "Emma Paris"
   $ git config --global user.email "eparis@atlassian.com"
   

3. Install Visual Studio Code for OSX (https://code.visualstudio.com/download). Do not launch VS Code.

4. Install homebrew if you haven’t already got it by copying and pasting the following single long line of code into a terminal window and hitting enter to run the code (be sure here and below to select and copy the entire command, which scrolls past the end of the screen):

   /usr/bin/ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"
   

5. Now run this command in the same terminal window to install software needed by Lean:

   brew install gmp coreutils
   

6. Next run this command in the same terminal window to install the Lean Prover:

   curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
   

7. Log out of (exit from) that terminal window.

8. Launch VS Code

   1. Click on the extension icon in the view bar at the left and search for lean
   2. Select the Lean extension for VS Code, click “install”, then “reload” to restart VS Code

9. Test your installation

   1. Create a new empty directory on your machine
   2. use File > New in VS Code to create a new file
   3. use File > Save As to save it into the directory you just created giving it the name “deleteme.lean” (without quotation marks). The “.lean” part of the file name tells VS code to activate the Lean extension.
   4. Then enter “#check 1” as the file contents. If Lean is running, you will see that #check is underlined in green and that if you hover your mouse cursor over it, it will tell you that the type of 1 is nat (blackboard font N).

If you get here and things aren’t working, try again. If that doesn’t work, contact a TA or your instructor.

10.2. Cloning the Class Repository

Now that you have a working terminal window, and the git version control software, you will now clone the student repository for this class. A git repository, also often referred to as a repo. We will make changes to the repository as the class goes along, which you will then incorporate into your “cloned” copy using the “git pull” command. The one important file in the current repository is part of your Homework #1 assignment: to get “Up and Running” for this semester.

So here’s what to do. First, check out the git repo on GitHub by visiting https://github.com/kevinsullivan/uva-cs-dm-f19. Second, “clone” the repo (get a copy of it on your laptop) by issuing this command in your terminal window:

git clone https://github.com/kevinsullivan/uva-cs-dm-f19.git

Now you should find a new uva-cs-dm-f19 directory in your current directory.

Now run VSCode and do File>Open or File>OpenFolder and open that new directory in VS Code. Use File > Open or the Open Folder function, select the uva-cs-dm-f19 directory as the “file” to open, and open it. You must open the directory, not the folder that contains it, and not any folder that it contains (such as “assignments”). If you do this right, you should see assignments and exams, among others, as folders in the project browser panel on the left side of VS Code. If you messed up, no worries, just do File > Close Folder, go back, and open up the right folder/directory. You are now ready to work.

To avoid conflicts, never change files in any directory in the class project directory except in the mywork sub-directory. We have programmed that directory to be ignored by git. (To see how we did this, look in the file you can find in the repo called .gitignore. Files and directories specified in this file are ignored by git. Those files are treated as being not part of the repo, so there will never be conflicts involving them.) So, to work on a file that we’ve given you, e.g., in the “hw” directory, first copy it from its current location to the mywork directory using VS Code right-click copy and paste commands (or do it in the terminal using the Unix “cp” command, which you can read about elsewhere).

10.3. Using Your IDE

The most important principle for using the VS Code editor to work on a Lean project is that you must always open the top-level project folder. Lean looks in the directory that you open for files that tell it what it needs to know to work properly. As an example, if the top-level folder for the class-provided Lean project is called uva-cs-dm-f19, then you must open this folder (directory) in Lean. Then all will be well.

10.4. Creating New Lean Projects

Once you’ve got your IDE installed and configured, you should also be able to create and work on your own Lean projects and code. To work on your own code in Lean, do not simply make a directory (folder) and start editing code in that folder. Rather, you must use the leanpkg tool. You can find instructions for doing that here: https://leanprover.github.io/reference/using_lean.html#using-the-package-manager. We thank the authors of that page for some of the information that we have included in this appendix.