Repository files navigation

For the course at Bonn SuSe 24.

• We will use a private channel on theLean Zulip to coordinate.
• Blueprint
• Blueprint as pdf

Note: To get this repository, you will need to download Lean's mathematical library, which takes about 5 GB of storage space.

• You have to install Lean, and two supporting programs: Git and VSCode. Follow theseinstructions to do this. You do not have to follow the last step (creating Lean projects). Instead, use either VSCode or a terminal to get this repository.

• Open Visual Studio Code

• PressClone Git Repository (if you don't see the welcome screen, you can pressctrl+shift+P (orcmd+shift+P on Mac), typeGit: Clone and pressenter)

• Typehttps://github.com/fpvandoorn/BonnAnalysis.git and press enter

• Choose a folder where you want to clone this repository (everything will be placed in a subfolderBonnAnalysis).

• Pressopen when asked if you want to open the cloned repository

• Open the fileBonnAnalysis/Test.lean using the explorer button in the top-right. Donot pressRestart Lean orRebuild Imports when these pop-ups show up. (If you do, you will rebuild mathlib yourself, which is not recommended)

• In the top-middle (or top-right) of the screen there is a Lean menu marked by∀.In it, chooseProject Actions... > Project: Fetch Mathlib Build Cache.This downloads mathlib, and will take a bit of time.

• Once this is finished, press theRebuild Imports button. The file should be ready a few seconds later. If you see a blue squiggle under#eval, Lean is running correctly.

• Open a terminal (I recommendgit bash on Windows, which was installed as part of git in the first step).

• Usecd to navigate to a directory where you would like to create theBonnAnalysis folder.

• Rungit clone https://github.com/fpvandoorn/BonnAnalysis.git.

• Runcd BonnAnalysis

• Runlake exe cache get!

  • This downloads mathlib, and will take a bit of time
  • On Windows, if you get an error that starts withcurl: (35) schannel: next InitializeSecurityContext failed it is probably your antivirus program that doesn't like that we're downloading many files. The easiest solution is to temporarily disable your antivirus program.

• Launch VS Code, either through your application menu or by typingcode . (note the dot!). (MacOS users need to take a one-offextra stepto be able to launch VS Code from the command line.)

• If you launched VS Code from a menu, on the main screen, or in the File menu,click "Open folder" (just "Open" on a Mac), and choose the folderBonnAnalysis (not one of its subfolders).

• Test that everything is working by openingBonnAnalysis/Test.lean.It is normal if it takes 10-60 seconds for Lean to start up.

To test the Blueprint locally, you can compileprint.tex using XeLaTeX (i.e.xelatex print.tex in the folderblueprint/src). If you have the Python packageinvoke you can also runinv bp which puts the output inblueprint/print/print.pdf.If you feel adventurous and want to build the web version of the blueprint locally, you need to install some packages by following the instructionshere. But if the pdf builds locally, you can just make a pull request and use the online blueprint.

• Update this repository to the latest version (rungit pull orgit fetch +git merge or their equivalents using VSCode source control).

• Switch to a branch. You can create a new branch usinggit switch -c mynewbranch or use... > Checkout to > Create new branch in VSCode. (This can also be done after the next step if you forget.)

• Write some Lean code

  • Try to follow the style guide:https://leanprover-community.github.io/contribute/style.html
  • Make sure it compiles

• Push your branch to your fork of this repository

  • Using the terminal you first have to create a fork on Github and usegit remote add to add this fork
  • Using VSCode this fork automatically created for you
  • When you have added a new file, please import it inBonnAnalysis.lean.

• Open a pull request

  • Just after you pushthis page will have a message on the top prompting you to open a pull request.

• If it builds, I'll merge it.

  • Feel free to make a pull request with partial work and a lot of sorry's, as long as it builds.

Reminder: Some additional details can be found in the instructions of the LeanCourse repository:https://github.com/fpvandoorn/LeanCourse23/blob/master/LeanCourse/Project/README.md