文件列表:

hitchhikers_guide.pdf (2007904, 2020-12-04)
hitchhikers_guide_tablet.pdf (2054486, 2020-12-04)
lean/ (0, 2020-12-04)
lean/love01_definitions_and_statements_demo.lean (10797, 2020-12-04)
lean/love01_definitions_and_statements_exercise_sheet.lean (4107, 2020-12-04)
lean/love01_definitions_and_statements_exercise_solution.lean (6131, 2020-12-04)
lean/love01_definitions_and_statements_homework_sheet.lean (3706, 2020-12-04)
lean/love02_backward_proofs_demo.lean (7939, 2020-12-04)
lean/love02_backward_proofs_exercise_sheet.lean (3388, 2020-12-04)
lean/love02_backward_proofs_exercise_solution.lean (4665, 2020-12-04)
lean/love02_backward_proofs_homework_sheet.lean (2313, 2020-12-04)
lean/love03_forward_proofs_demo.lean (10703, 2020-12-04)
lean/love03_forward_proofs_exercise_sheet.lean (2792, 2020-12-04)
lean/love03_forward_proofs_exercise_solution.lean (4924, 2020-12-04)
lean/love03_forward_proofs_homework_sheet.lean (2326, 2020-12-04)
lean/love04_functional_programming_demo.lean (12638, 2020-12-04)
lean/love04_functional_programming_exercise_sheet.lean (5498, 2020-12-04)
lean/love04_functional_programming_exercise_solution.lean (7232, 2020-12-04)
lean/love04_functional_programming_homework_sheet.lean (2478, 2020-12-04)
lean/love05_inductive_predicates_demo.lean (13827, 2020-12-04)
lean/love05_inductive_predicates_exercise_sheet.lean (2302, 2020-12-04)
lean/love05_inductive_predicates_exercise_solution.lean (3336, 2020-12-04)
lean/love05_inductive_predicates_homework_sheet.lean (2999, 2020-12-04)
lean/love06_monads_demo.lean (11478, 2020-12-04)
lean/love06_monads_exercise_sheet.lean (6234, 2020-12-04)
lean/love06_monads_exercise_solution.lean (7015, 2020-12-04)
lean/love06_monads_homework_sheet.lean (5071, 2020-12-04)
lean/love07_metaprogramming_demo.lean (14384, 2020-12-04)
lean/love07_metaprogramming_exercise_sheet.lean (7185, 2020-12-04)
lean/love07_metaprogramming_exercise_solution.lean (9504, 2020-12-04)
lean/love07_metaprogramming_homework_sheet.lean (4093, 2020-12-04)
lean/love08_operational_semantics_demo.lean (21026, 2020-12-04)
lean/love08_operational_semantics_exercise_sheet.lean (5546, 2020-12-04)
lean/love08_operational_semantics_exercise_solution.lean (9418, 2020-12-04)
lean/love08_operational_semantics_homework_sheet.lean (4496, 2020-12-04)
lean/love08_operational_semantics_homework_solution.lean (7356, 2020-12-04)
lean/love09_hoare_logic_demo.lean (14734, 2020-12-04)
lean/love09_hoare_logic_exercise_sheet.lean (3982, 2020-12-04)
... ...

# Logical Verification 2020: Installation Instructions We have installation instructions for Windows, Linux, and macOS. As a backup plan, we provide a virtual machine on which Lean is already installed. These directions are adapted from the [leanprover-community](https://leanprover-community.github.io/get_started.html#regular-install) web page.

Windows

## Windows These instructions are also covered in a [YouTube video](https://www.youtube.com/watch?v=y3GsHIe4wZ4). This does not include the "Install our Logical Verification Repository" step. ### Get Lean * Install Git for Windows: https://gitforwindows.org/. Accept all default answers during the installation (or, if you would like to minimize the installation, you may deselect all components on the "Select components" question). * Start the newly installed `Git Bash` by searching for it in the Windows search bar. * In Git Bash, run the command `curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh`. * Press `[Enter]` to proceed with the installation. * Run `echo 'PATH="$HOME/.elan/bin:$PATH"' >> $HOME/.profile`. * Close Git Bash. ### Get Python * Download the latest version of python [here](https://www.python.org/downloads/). * Run the downloaded file (`python-3.x.x.exe`) * Check `Add Python 3.x to PATH`. * Choose the default installation. * Open Git Bash (type `git bash` in the Start Menu) * Run `which python` * The expected output is something like `/c/Users//AppData/Local/Programs/Python/Pythonxx-xx/python`. In this case, proceed to the next step. * If it's something like `/c/Users//AppData/Local/Microsoft/WindowsApps/python`, then * Did you follow the instruction to select `Add Python 3.x to PATH` during the installation? * If not, re-run the python installer to uninstall python and try again. * Otherwise, you need to disable a Windows setting. * Type `manage app execution aliases` into the Windows search prompt (start menu) and open the corresponding System Settings page. * There should be two entries `App Installer python.exe` and `App Installer python3.exe`. Ensure that both of these are set to `Off`. * Close and reopen Git Bash and restart this step. * If it is any other directory, you might have an existing version of Python. Ask the TAs for help. * If you get `command not found`, you should add the Python directory to your path. Google how to do this, or ask the TAs. * Run `cp "$(which python)" "$(which python)"3`. This ensures that we can use the command `python3` to call Python. * Test whether everything is working by typing `python3 --version` and `pip3 --version`. If both commands give a short output and no error, everything is set up correctly. * If `pip3 --version` doesn't give any output, run the command `python3 -m pip install --upgrade pip`, which should fix it. ### Configure Git * Run `git config --global core.autocrlf input` in Git Bash. ### Install Lean Tools * in Git Bash, run ```bash pip3 install mathlibtools ``` ### Install and Configure the Editor * Install [VS Code](https://code.visualstudio.com/). * Launch VS Code. * Click on the extension icon  (or  in older versions) in the side bar on the left edge of the screen (or press ShiftCtrlX) and search for `leanprover`. * Click "install" (In old versions of VS Code, you might need to click "reload" afterwards) * Setup the default shell: * If you're using `git bash`, press `ctrl-shift-p` to open the command palette, and type `Select Default Shell`, then select `git bash` from the menu. * Restart VS Code. * Verify Lean is working, for example by saving a file `test.lean` and entering `#eval 1+1`. A green line should appear underneath `#eval 1+1`, and hovering the mouse over it you should see `2` displayed. ### Install Our Logical Verification Repository * Close VSCode. * Open Git Bash. * In Git Bash, use `cd` to go to the directory you want to place the project in (a new folder will be created for it at that location). For instance, you can use `cd ~/Documents` to go to your personal Documents folder. * Run these commands in Git Bash: ```bash leanproject get blanchette/logical_verification_2020 cd logical_verification_2020 lean --make lean ``` The last command should produce a long list of warnings and errors which you can ignore. * Launch VSCode. * In the `File` menu, click `Open Folder`, and choose the folder `logical_verification_2020` (not one of its subfolders). If you used `~/Documents` above, it will be located in your `Documents` folder. * In the file explorer on the left-hand side, you will find all exercises and homework in the `lean` folder, as we upload them. * You can retrieve the newest exercises and homework that we upload by clicking the two arrows forming a circle in the bottom left corner.

Debian/Ubuntu and Derivates

## Debian/Ubuntu and Derivates These instructions are also in a [YouTube video](https://www.youtube.com/watch?v=02ff4WrW0FU), not including the Logical Verification repository details. ### Install Lean * Open a terminal, enter the following command and hit enter. (This will take some time.) ```bash wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile ``` * You may have to log out and log in again to make sure that the `lean` command is on your `PATH`. ### Install our Logical Verification Repository * Use `cd` to go to the directory you want to place the project in. (A new folder will be created for it at that location.) ```bash leanproject get blanchette/logical_verification_2020 cd logical_verification_2020 lean --make lean ``` The last command should produce a long list of warnings and errors which you can ignore. * Launch VScode, either through your application menu or by typing `code`. * On the main screen, or in the `File` menu, click `Open Folder`, and choose the folder `logical_verification_2020` (not one of its subfolders). * In the file explorer on the left-hand side, you will find all exercises and homework in the `lean` folder, as we upload them. * You can retrieve the newest exercises and homework that we upload by clicking the two arrows forming a circle in the bottom left corner.

Other Linux Distros

## Other Linux Distros Follow [these instructions](https://leanprover-community.github.io/install/linux.html) and proceed by the instructions "Install our logical verification repository" for Debian/Ubunutu above.

macOS

## macOS These instructions are also in a [YouTube video](https://www.youtube.com/watch?v=NOGWsCNm_FY&ab_channel=leanprovercommunity), not including the Logical Verification repository details. ### Install Lean * Open a terminal, enter the following command and hit enter. (This will take some time.) ```bash /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile ``` ### Install our Logical Verification Repository * Open a terminal. * Use `cd` to go to the directory you want to place the project in (a new folder will be created for it at that location), for example you can use `~/Documents`. ```bash leanproject get blanchette/logical_verification_2020 cd logical_verification_2020 lean --make lean ``` The last command should produce a long list of warnings and errors which you can ignore. * Open VScode again. * In the `File` menu, click `Open`, and choose the folder `logical_verification_2020` (not one of its subfolders). If you used `~/Documents` above, it will be in the `Documents` folder. * In the file explorer on the left-hand side, you will find all exercises and homework in the `lean` folder, as we upload them. * You can retrieve the newest exercises and homework that we upload by clicking the two arrows forming a circle in the bottom left corner.

Virtual Machine (for Any Operating System)

## Virtual Machine * Download and install [VirtualBox](https://www.virtualbox.org/). (Other virtualization software should also work.) * Download the virtual machine, `logical_verification_2020.ova` (2.8G), from [Google Drive](https://drive.google.com/file/d/1oqV8ckyUN_jwLTOOB-DfYn4p2E-xwFs1/view?usp=sharing). SHA256: ``` 055d8a81ba1b48c9ae30b05c0a736f7aacc0b1a37133c8c681be47e040a50be6 logical_verification_2020.ova ``` * Open VirtualBox. * Import the downloaded file via `File > Import Appliance`. This requires around 6GB of disk space. The virtual machine is configured to use 4 processor cores and up to 5GB of RAM. It uses around 4GB of RAM if you open all the Lean files in VSCode. * Start the virtual machine by selecting `logical_verification_2020` and clicking the `Start` button. * Open VSCode by clicking on the blue ribbon icon on the desktop. VSCode should automatically open the folder `~/logical_verification_2020`. In the file explorer on the left-hand side, you will find all exercises and homework in the `lean` folder, as we upload them. * You can retrieve the newest exercises and homework that we upload by clicking the two arrows forming a circle in the bottom left corner. * If you need the password for the virtual machine at some point, it is `love`.

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：