Setup

Installing Lean

All the software we will use in this course, including Lean and its main library, is free and open source. With this comes a familiar speed bump: community-developed software is not always the easiest to install. Luckily, the Lean community has put in some effort to streamline the process.

Please follow the instructions in the Lean Manual quick-start guide if you have not previously installed Lean on your computer.¹ Stop when you reach the text "You are set up!" — do not continue onto the "Create a Lean Project" section. Once you have installed Lean, clone the course GitHub repository (see below) and execute lake exe cache get in the fpv2024 directory.

If you have previously installed Lean, open a terminal and run elan self update. You should also have Git and Visual Studio Code installed. Then clone the course GitHub repository (see below) and execute lake exe cache get in the fpv2024 directory.

The course staff will be available at the beginning of the course to help with installation hiccups.

Note: When you open VSCode, be sure to open a full Lean project. That means, use File -> Open Folder... to open a folder that contains a lakefile.lean file (e.g., the fpv2024 directory). Alternatively, open VS Code from the command line with code fpv2024. If you open a single file instead of a directory, the Lean VS Code plugin will not know what version of Lean to use, and your imports will most likely not work.

Course Files

The lecture notes, practice exercises, and homework assignments will be uploaded to the course GitHub repository: https://github.com/BrownCS1951x/fpv2024. We recommend cloning this repository now and periodically pulling as we update and add files over the course of the semester.

¹If these instructions don't work, try the fallback setup instructions for your operating system: Windows, Debian/Ubuntu, other Linux distros, macOS.