Lean Up

This tool is intended to help students install & update Lean for CSE 505.

This is the first version of the class we are offering written in Lean, and the goal of this tool is to make upgrade as seamless as possible for you over the course of the quarter.

Note: This is the first iteration of the course with Lean, and this auto-updating software is a work in progress, if you find issues please report them to us so we can try to improve the user experince.

Setup

Getting set up with Lean takes just a few simple steps.

In order to run leanup.py you need a few components:

Git
Python 3 (with pip), it should be installed on most Linux distributions, can easily be installed on macOS with homebrew, and Windows instructions are here.
VSCode

First clone this tool on to your computer:

git clone https://github.com/uwplse/leanup

Then setup the tool (you should only do this once):

pip install pipenv
cd leanup
pipenv install
pipenv shell

You should now be able to run:

./leanup.py install

Now copy the path provided to you by the tool since we will need it for VSCode. First open the User Settings window of VSCode (cmd-, or ctrl-, depending on platform), and modify the lean.executablePath to point to the executable provided by leanup.

When you are all done you should be able to open the file in test/example.lean and see some diagnostics.

Overall this process should take no more then a few minutes. I've done my best to test it on the major platforms, if you have trouble please drop by the Slack channel #505-au17 for questions/help.

Use

leanup.py has a few features ...

Shamrock-Frost/leanup

Lean Up

Setup

Use