Change some instructions in the README.md (#573)

* Change git commands in the README.md for beginners

* Only clone PLFA shallowly.
* Correct the version of stdandard library for PLFA.

* Install `fix-whitespace` via Stackage

The program `fix-whitespace` is available on Stackage already.
This commit is contained in:
Liang-Ting Chen 2021-08-23 02:52:20 +08:00 committed by GitHub
parent 8fec0eb208
commit 09d04baefd
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -94,20 +94,21 @@ Finished hello.
### Install PLFA and the Agda standard library ### Install PLFA and the Agda standard library
You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]: You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]:
```bash ```bash
git clone --recurse-submodules https://github.com/plfa/plfa.github.io plfa git clone --depth 1 --recurse-submodules --shallow-submodules https://github.com/plfa/plfa.github.io plfa
# Remove `--depth 1` and `--shallow-submodules` if you want the complete git history of PLFA and the standard library.
``` ```
PLFA ships with the required version of the Agda standard library, so if you cloned with the `--recurse-submodules` flag, youve already got, in the `standard-library` directory! PLFA ships with the required version of the Agda standard library, so if you cloned with the `--recurse-submodules` flag, youve already got, in the `standard-library` directory!
If you forgot to add the `--recurse-submodules` flag, no worries, we can fix that! If you forgot to add the `--recurse-submodules` flag, no worries, we can fix that!
```bash ```bash
cd plfa/ cd plfa/
git submodule update --recursive git submodule update --init --recursive --depth 1
# Remove `--depth 1` if you want the complete git history of the standard library.
``` ```
If you obtained PLFA by downloading the zip archive, you can get the required version of the Agda standard library from GitHub. You can either clone the repository and switch to the correct branch, or you can download the [the zip archive][agda-stdlib]: If you obtained PLFA by downloading the zip archive, you can get the required version of the Agda standard library from GitHub. You can either clone the repository and switch to the correct branch, or you can download the [the zip archive][agda-stdlib]:
```bash ```bash
git clone https://github.com/agda/agda-stdlib.git agda-stdlib git clone https://github.com/agda/agda-stdlib.git --branch v1.6 --depth 1 agda-stdlib
cd agda-stdlib # Remove `--depth 1` if you want the complete git history of the standard library.
git checkout v1.3
``` ```
Finally, we need to let Agda know where to find the Agda standard library. Finally, we need to let Agda know where to find the Agda standard library.
You'll need the path where you installed the standard library. Check to see that the file “standard-library.agda-lib” exists, and make a note of the path to this file. You'll need the path where you installed the standard library. Check to see that the file “standard-library.agda-lib” exists, and make a note of the path to this file.
@ -318,9 +319,7 @@ The repository comes with several Git hooks:
You can install these Git hooks by calling `make init`. You can install these Git hooks by calling `make init`.
You can install [fix-whitespace][fix-whitespace] by running: You can install [fix-whitespace][fix-whitespace] by running:
```bash ```bash
git clone https://github.com/agda/fix-whitespace stack install fix-whitespace
cd fix-whitespace/
stack install --stack-yaml stack-8.8.3.yaml
``` ```
If you want Stack to use your system installation of GHC, follow the instructions for [Using an existing installation of GHC](#using-an-existing-installation-of-ghc). If you want Stack to use your system installation of GHC, follow the instructions for [Using an existing installation of GHC](#using-an-existing-installation-of-ghc).