/IISc-experiments

Some material for Lean 4 lectures at IISc

Primary LanguageLean

IISc-experiments

Some material for Lean 4 lectures at IISc.

Written in Bengaluru, April 2023.

Learning resources (how do I learn?)

See the RESOURCES file.

How to run this repo yourself?

Local installation

This is the best way; you can edit files and experiment, and you won't lose them. It's also the hardest way: it involves typing stuff in on the command line.

In brief: first install Lean 4 following the instructions here.

Then download and install this project by going to its home page on GitHub, clicking "Code" and "local", and then downloading the project onto your computer.

Pic: local installation

Next open a command line in the project folder, type lake exe cache get, and wait until all files are downloaded and installed and your cursor has reappeared.

Finally, open the root directory of the project folder in VS Code. You can open the files in the IIScExperiments directory (not the IIScExperiments.lean Lean file!) and these correspond to the material I was going through in lectures.

Remote running via GitPod

You don't need to install anything onto your computer using this method.

Just click here: Open in Gitpod

Note to self: I got gitpod working by adding the files .gitpod.yml and .docker/gitpod/Dockerfile

Remote running via Codespaces

You don't need to install anything onto your computer using this method.

Go to the project's home page on GitHub, click "Code" and then "Codespaces" so it looks like this:

Pic: codespaces installation

Then click "create codespace on main", and then wait for a few minutes. When it looks like everything has downloaded, open up the IIScExperiments directory (not the file!) and the code I've been using in the lectures should just work.

Note to self: I got codespaces working by adding the files .devcontainer/devcontainer.json and .devcontainer/Dockerfile.