Skip to content

Commit 9eb4838

Browse files
ranjitjhalaranjitjhala
authoredAug 4, 2020
Merge pull request #1722 from ucsd-progsys/adinapoli/polish-docs
Polish documentation
·
v9.2.8liquid-platform-0.9.2.8
2 parents 1bd2a42 + a723bb1 commit 9eb4838

11 files changed

+502
-617
lines changed
 

‎docs/mkDocs/README.md

+15-6
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
## Deploying the Documentation
1+
# Building and deploying the documentation
22

33
To build the documentation, first setup `python3` and related packages
44

@@ -9,16 +9,25 @@ $ python3 get-pip.py
99
$ pip3 install mkdocs pygments Pygmentize mkdocs-bootswatch
1010
```
1111

12-
after that to view the documents locally do
12+
after that to view the documents locally run:
1313

1414
```
15-
$ mkDocs serve
15+
mkDocs serve
1616
```
1717

18-
to push to github you do
18+
## Strict mode
1919

20-
mkDocs gh-deploy
20+
It's recommended to run `mkDocs serve` with the _strict_ option (i.e. `-s`) to ensure no broken links are
21+
present in the generated docs:
2122

2223
```
23-
$ mkdocs gh-deploy
24+
mkDocs serve -s
25+
```
26+
27+
## Publishing
28+
29+
To push to github you can simply run:
30+
31+
```
32+
mkdocs gh-deploy
2433
```

‎docs/mkDocs/docs/community.md

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
# Community
2+
3+
If you have any questions, you can:
4+
5+
* Join the Liquid Haskell [slack channel](https://join.slack.com/t/liquidhaskell/shared_invite/enQtMjY4MTk3NDkwODE3LTFmZGFkNGEzYWRkNDJmZDQ0ZGU1MzBiZWZiZDhhNmY3YTJiMjUzYTRlNjMyZDk1NDU3ZGIxYzhlOTIzN2UxNWE)
6+
* Mail the [users mailing list](https://groups.google.com/forum/#!forum/liquidhaskell)
7+
8+
9+
Alternatively, feel free to drop [Ranjit Jhala](https://github.com/ranjitjhala) or
10+
[Niki Vazou](https://github.com/nikivazou) an email.

‎docs/mkDocs/docs/contributing.md

+26-9
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,39 @@
1-
# Contributions
1+
# Get involved
22

3-
We are excited for you to try LH!
3+
We are excited for you to try LH!
44

5-
## Community
5+
In this section you can find instructions on how to submit your first PR as well as practical instructions
6+
on how develop LiquidHaskell.
67

7-
If you have any questions
8+
## Hacking on LiquidHaskell
89

9-
* Join the Liquid Haskell [slack channel](https://join.slack.com/t/liquidhaskell/shared_invite/enQtMjY4MTk3NDkwODE3LTFmZGFkNGEzYWRkNDJmZDQ0ZGU1MzBiZWZiZDhhNmY3YTJiMjUzYTRlNjMyZDk1NDU3ZGIxYzhlOTIzN2UxNWE)
10-
* Mail the [users mailing list](https://groups.google.com/forum/#!forum/liquidhaskell)
11-
* Create a [github issue](https://github.com/ucsd-progsys/liquidhaskell/issues)
10+
If you want to extend LH to fix a bug or provide a new feature, you might be interested in reading
11+
our [Developer's guide](develop.md).
1212

13-
## Pull requests
13+
## Reporting a bug
1414

15-
We are thrilled to get PRs!
15+
If something doesn't work as it should, please consider opening a [github issue](https://github.com/ucsd-progsys/liquidhaskell/issues)
16+
to let us know. If possible, try to:
17+
18+
* Try to use a descriptive title;
19+
* State as clearly as possible what is the problem you are facing;
20+
* Provide a small Haskell file producing the issue;
21+
* Write down the expected behaviour vs the actual behaviour;
22+
* If possible, let us know if you have used the [plugin](plugin.md) or the [executable](legacy.md) and
23+
which _GHC version_ you are using.
24+
25+
## Your first Pull Request
26+
27+
We are thrilled to get PRs! Please follow these guidelines, as doing so will increase the chances of
28+
having your PR accepted:
1629

1730
* The main LH repo [lives here](https://github.com/ucsd-progsys/liquidhaskell)
1831
* Please create pull requests against the `develop` branch.
1932
* Please be sure to include test cases that illustrate the effect of the PR
2033
- e.g. show new features that that are supported or how it fixes some previous issue
2134
* If the PR adds a `LIQUID` pragma or option, please also add documentation
2235
- e.g. in [options.md](options.md) or [specifications.md](specifications.md)
36+
37+
## Ask for help
38+
39+
If you have further questions or you just need help, you can always reach out to the [community](community.md).

‎docs/mkDocs/docs/develop.md

+36-152
Original file line numberDiff line numberDiff line change
@@ -116,163 +116,51 @@ You can directly extend and run the tests by modifying
116116
117117
## Working With Submodules
118118
119-
- To update the `liquid-fixpoint` submodule, run
119+
To update the `liquid-fixpoint` submodule, run:
120120
121-
```
122-
cd ./liquid-fixpoint
123-
git fetch --all
124-
git checkout <remote>/<branch>
125-
cd ..
126-
```
127-
128-
This will update `liquid-fixpoint` to the latest version on `<branch>`
129-
(usually `master`) from `<remote>` (usually `origin`).
130-
131-
- After updating `liquid-fixpoint`, make sure to include this change in a
132-
commit! Running
133-
134-
```
135-
git add ./liquid-fixpoint
136-
```
137-
138-
will save the current commit hash of `liquid-fixpoint` in your next commit
139-
to the `liquidhaskell` repository.
140-
141-
- For the best experience, **don't** make changes directly to the
142-
`./liquid-fixpoint` submodule, or else git may get confused. Do any
143-
`liquid-fixpoint` development inside a separate clone/copy elsewhere.
144-
145-
- If something goes wrong, run
146-
147-
```
148-
rm -r ./liquid-fixpoint
149-
git submodule update --init
150-
```
151-
152-
to blow away your copy of the `liquid-fixpoint` submodule and revert to the
153-
last saved commit hash.
154-
155-
- Want to work fully offline? git lets you add a local directory as a remote.
156-
Run
157-
158-
```
159-
cd ./liquid-fixpoint
160-
git remote add local /path/to/your/fixpoint/clone
161-
cd ..
162-
```
163-
164-
Then to update the submodule from your local clone, you can run
165-
166-
```
167-
cd ./liquid-fixpoint
168-
git fetch local
169-
git checkout local/<branch>
170-
cd ..
171-
```
172-
173-
174-
## Generating Performance Reports
175-
176-
**DEPRECATED**
177-
178-
We have set up infrastructure to generate performance reports using [Gipeda](https://github.com/nomeata/gipeda).
179-
180-
Gipeda will generate a static webpage that tracks the performance improvements
181-
and regressions between commits. To generate the site, first ensure you have the
182-
following dependencies available:
183-
184-
* Git
185-
* Cabal >= 1.18
186-
* GHC
187-
* Make
188-
* Bash (installed at `/bin/bash`)
189-
190-
After ensuring all dependencies are available, from the Liquid Haskell
191-
directory, execute:
192-
193-
cd scripts/performance
194-
./deploy-gipeda.bash
195-
196-
This will download and install all the relevant repositories and files. Next, to
197-
generate the performance report, use the `generate-site.bash` script. This script
198-
has a few options:
199-
200-
* `-s [hash]`: Do not attempt to generate performance reports for any commit
201-
older than the commit specified by the entered git hash
202-
* `-e [hash]`: Do not attempt to generate performance reports for any commit
203-
newer than the commit specified by the entered git hash
204-
* `-f`: The default behavior of `generate-site.bash` is to first check if logs
205-
have been created for a given hash. If logs already exist, `generate-site.bash`
206-
will not recreate them. Specify this option to skip this check and regenerate
207-
all logs.
208-
209-
You should expect this process to take a very long time. `generate-site.bash`
210-
will compile each commit, then run the entire test suite and benchmark suite
211-
for each commit. It is suggested to provide a manageable range to `generate-site.bash`:
212-
213-
./generate-site.bash -s [starting hash] -e [ending hash]
214-
215-
...will generate reports for all commits between (inclusive) [starting hash]
216-
and [ending hash].
217-
218-
./generate-site.bash -s [starting hash]
219-
220-
... will generate reports for all commits newer than [starting hash]. This command
221-
can be the basis for some automated report generation process (i.e. a cron job).
222-
223-
Finally, to remove the Gipeda infrastructure from your computer, you may execute:
224-
225-
./cleanup-gipeda.bash
226-
227-
...which will remove any files created by `deploy-gipeda.bash` and `generate-site.bash`
228-
from your computer.
229-
230-
231-
## Configuration Management
232-
233-
It is very important that the version of Liquid Haskell be maintained properly.
234-
235-
Suppose that the current version of Liquid Haskell is `A.B.C.D`:
236-
237-
+ After a release to hackage is made, if any of the components `B`, `C`, or `D` are missing, they shall be added and set to `0`. Then the `D` component of Liquid Haskell shall be incremented by `1`. The version of Liquid Haskell is now `A.B.C.(D + 1)`
238-
239-
+ The first time a new function or type is exported from Liquid Haskell, if any of the components `B`, or `C` are missing, they shall be added and set to `0`. Then the `C` component shall be incremented by `1`, and the `D` component shall stripped. The version of Liquid Haskell is now `A.B.(C + 1)`
240-
241-
+ The first time the signature of an exported function or type is changed, or an exported function or type is removed (this includes functions or types that Liquid Haskell re-exports from its own dependencies), if the `B` component is missing, it shall be added and set to `0`. Then the `B` component shall be incremented by `1`, and the `C` and `D` components shall be stripped. The version of Liquid Haskell is now `A.(B + 1)`
242-
243-
+ The `A` component shall be updated at the sole discretion of the project owners.
244-
245-
## Updating GHC Versions
121+
```
122+
cd ./liquid-fixpoint
123+
git fetch --all
124+
git checkout <remote>/<branch>
125+
cd ..
126+
```
246127
247-
Here's a script to generate the diff for the `desugar` modules.
128+
This will update `liquid-fixpoint` to the latest version on `<branch>` (usually `master`)
129+
from `<remote>` (usually `origin`). After updating `liquid-fixpoint`, make sure to include this change in a
130+
commit! Running:
248131
249132
```
250-
export GHCSRC=$HOME/Documents/ghc
251-
252-
# Checkout GHC-8.2.2
253-
(cd $GHCSRC && git checkout ghc-8.2.2 && git pull)
133+
git add ./liquid-fixpoint
134+
```
254135
255-
# make a patch
256-
diff -ur $GHCSRC/compiler/deSugar src/Language/Haskell/Liquid/Desugar > liquid.patch
136+
will save the current commit hash of `liquid-fixpoint` in your next commit to the `liquidhaskell` repository.
137+
For the best experience, **don't** make changes directly to the `./liquid-fixpoint` submodule, or else git
138+
may get confused. Do any `liquid-fixpoint` development inside a separate clone/copy elsewhere. If something
139+
goes wrong, run:
257140
258-
# Checkout GHC-8.4.3
259-
(cd $GHCSRC && git checkout ghc-8.2.2 && git pull)
141+
```
142+
rm -r ./liquid-fixpoint
143+
git submodule update --init
144+
```
260145
261-
# Copy GHC desugarer to temporary directory
262-
cp -r $GHCSRC/compiler/deSugar .
146+
to blow away your copy of the `liquid-fixpoint` submodule and revert to the last saved commit hash.
263147
264-
# Patch
265-
(cd deSugar && patch -p5 --merge --ignore-whitespace < ../liquid.patch)
148+
Want to work fully offline? `git` lets you add a local directory as a remote. Run:
266149
267-
# Copy stuff over
268-
for i in src/Language/Haskell/Liquid/Desugar/*.*; do j=$(basename $i); echo $j; cp deSugar/$j src/Language/Haskell/Liquid/Desugar; done
150+
```
151+
cd ./liquid-fixpoint
152+
git remote add local /path/to/your/fixpoint/clone
153+
cd ..
269154
```
270155
271-
Here's the magic diff that we did at some point that we keep bumping up to new GHC versions:
272-
273-
https://github.com/ucsd-progsys/liquidhaskell/commit/d380018850297b8f1878c33d0e4c586a1fddc2b8#diff-3644b76a8e6b3405f5492d8194da3874R224
156+
Then to update the submodule from your local clone, you can run:
274157
275-
[compiler plugin]: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/extending_ghc.html#compiler-plugins
158+
```
159+
cd ./liquid-fixpoint
160+
git fetch local
161+
git checkout local/<branch>
162+
cd ..
163+
```
276164
277165
## Releasing on Hackage
278166
@@ -281,11 +169,7 @@ in the release process. Most contributors can skip this section.*
281169
282170
We provide a conveniency script to upload all the `liquid-*` packages (**including** `liquid-fixpoint`) on
283171
Hackage, in a lockstep fashion. To do so, it's possible to simply run the `scripts/release_to_hackage.sh`
284-
Bash script. The script tries to determine the packages to upload by scanning the $PWD for packages named
285-
appropriately. It will ask the user for confirmation before proceeding, and `cabal upload` will be used
286-
under the hood. Any options passed to the script will be routed to `cabal`. For example, to upload a package
287-
using a particular combination of user and password:
172+
Bash script. The script doesn't accept any argument and it tries to determine the packages
173+
to upload by scanning the `$PWD` for packages named appropriately. It will ask the user for confirmation
174+
before proceeding, and `stack upload` will be used under the hood.
288175
289-
```
290-
./scripts/release_to_hackage.sh -u foo -p bar
291-
```

‎docs/mkDocs/docs/index.md

+17-13
Original file line numberDiff line numberDiff line change
@@ -2,33 +2,37 @@
22

33
# LiquidHaskell
44

5-
LiquidHaskell (LH) refines Haskell's types with logical
5+
LiquidHaskell (_LH_) refines Haskell's types with logical
66
predicates that let you enforce important properties at
77
compile time. See [the blog](https://ucsd-progsys.github.io/liquidhaskell-blog/)
88
for examples.
99

1010
## Quick Start
1111

12-
The following links are a quick way to play with and learn about LH
12+
Read the below for more details on how to:
13+
14+
* **Install** [external software](install.md) dependencies required by LH
15+
* **Install** and use LH as a [GHC Plugin](plugin.md)
16+
* Use the command line [options](options.md) supported by LH
17+
* Write refinement type [specifications](specifications.md)
18+
19+
## Learn
20+
21+
The following links are a quick way to play with and learn about LH:
1322

1423
* [Try online in your browser](http://goto.ucsd.edu:8090/index.html)
1524
* [Splash page with examples and link to blog](https://ucsd-progsys.github.io/liquidhaskell-blog/)
1625
* [Andres Loeh's Tutorial](https://liquid.kosmikus.org)
1726

18-
## Longer Tutorials
19-
20-
If the above whets your appetite, you may enjoy working through the following
27+
If the above whets your appetite, you may enjoy working through the following longer tutorials:
2128

2229
* [120 minute workshop with more examples](http://ucsd-progsys.github.io/lh-workshop/01-index.html)
2330
* [Long ish Tutorial](http://ucsd-progsys.github.io/liquidhaskell-tutorial/)
2431

25-
## Documentation
32+
## Get involved
2633

27-
Read the below for more details on how to
34+
If you are interested to contribute to LH and its ecosystem, you may want to:
2835

29-
* Use LH as a [GHC Plugin](plugin.md)
30-
* Use the (legacy) LH standalone [executable](legacy.md)
31-
* Use the command line [options](options.md) supported by LH
32-
* Write refinement type [specifications](specifications.md)
33-
* Develop and [contribute](develop.md) to LH
34-
* Join the LH [community](contributing.md) to discuss issues related to LH
36+
* Read the contribution [guidelines](contributing.md)
37+
* Read our [developers' guide](develop.md) to LH
38+
* Join the LH [community](community.md) to discuss issues related to LH

‎docs/mkDocs/docs/install.md

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
# How to install
2+
3+
This sections documents how to install LH and its dependencies.
4+
5+
## External software requirements
6+
7+
In order to use `liquidhaskell`, you will need a [SMT solver](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)
8+
installed on your system. Download and install at least one of:
9+
10+
* [Z3](https://github.com/Z3Prover/z3) or [Microsoft official binary](https://www.microsoft.com/en-us/download/details.aspx?id=52270)
11+
* [CVC4](https://cvc4.github.io/)
12+
* [MathSat](https://mathsat.fbk.eu/)
13+
14+
Note: The SMT solver binary should be on your `PATH`; LiquidHaskell will execute it as a child process.
15+
16+
## Next
17+
18+
Once installed, you can now install and use LH as [a plugin](plugin.md) or legacy [executable](legacy.md).

‎docs/mkDocs/docs/legacy.md

+19-74
Original file line numberDiff line numberDiff line change
@@ -1,34 +1,18 @@
1-
# Installing and Running the Legacy LiquidHaskell Executable
1+
# Installing the Legacy LiquidHaskell Executable
22

33
**We strongly recommend** that you use the [GHC Plugin](plugin.md)
4-
available in version 0.8.10 onwards. The legacy executable has been
5-
kept around for backwards compatibility but will eventually be deprecated.
4+
available in version 0.8.10 onwards, as the legacy executable is deprecated and has been
5+
kept around for backwards compatibility. It will eventually be removed from future LH releases.
66

7+
## External software requirements
78

8-
## Install
9+
Make sure all the required [external software](install.md) software is installed before proceeding.
910

10-
To run the legacy LiquidHaskell executable you need to install:
11-
12-
1. An SMT solver
13-
2. LH itself as a standalone binary
14-
15-
You can install the `liquid` binary via package manager *or* source.
16-
17-
### 1. Install SMT Solver
18-
19-
Download and install *at least one* of
20-
21-
+ [Z3](https://github.com/Z3Prover/z3/releases) or [Microsoft official binary](https://www.microsoft.com/en-us/download/details.aspx?id=52270)
22-
+ [CVC4](http://cvc4.cs.stanford.edu/web/)
23-
+ [MathSat](http://mathsat.fbk.eu/download.html)
24-
25-
**Note:** The SMT solver binary should be on your `PATH`; LiquidHaskell will execute it as a child process.
26-
27-
### 2. Install Legacy Binary
11+
## Installation options
2812

2913
You can install the `liquid` binary via package manager *or* source.
3014

31-
#### Via Package Manager
15+
### Via Package Manager
3216

3317
Simply do:
3418

@@ -38,72 +22,34 @@ We are working to put `liquid` on `stackage`.
3822

3923
You can designate a specific version of LiquidHaskell to
4024
ensure that the correct GHC version is in the environment.
41-
As an example,
25+
For example:
4226

43-
cabal install liquidhaskell-0.9.0.0
27+
cabal install liquidhaskell-0.8.10.1
4428

45-
#### Build from Source
29+
### Build from Source
4630

4731
If you want the most recent version, you can build from source as follows,
4832
either using `stack` (recommended) or `cabal`. In either case:
4933

50-
1. *recursively* `clone` the repo
51-
52-
git clone --recursive https://github.com/ucsd-progsys/liquidhaskell.git
53-
cd liquidhaskell
54-
55-
2. `build` the package with [stack][stack]
56-
57-
stack install liquidhaskell
58-
59-
3. or with [cabal][cabal]
60-
61-
cabal v2-build liquidhaskell
34+
1. *recursively* `clone` the repo:
6235

63-
#### A note on the GHC_PACKAGE_PATH
36+
```git clone --recursive https://github.com/ucsd-progsys/liquidhaskell.git```
6437

65-
To work correctly `liquid` requires access to auxiliary packages
66-
installed as part of the executable. Therefore, you might need to
67-
extend your `$GHC_PACKAGE_PATH` to have it point to the right location(s).
68-
69-
Typically the easiest way is to call `stack path`, which will print
70-
a lot of diagnostic output. From that it should be suffient to copy
71-
the paths printed as part of `ghc-package-path: <some-paths>` and
72-
extend the `GHC_PACKAGE_PATH` this way (typically editing your `.bashrc`
73-
to make the changes permanent):
74-
75-
```
76-
export GHC_PACKAGE_PATH=$GHC_PACKAGE_PATH:<some-paths>
77-
```
78-
79-
After that, running `liquid` anywhere from the filesystem should work.
80-
81-
### Troubleshooting
82-
83-
1. If you're on Windows, please make sure the SMT solver is installed
84-
in the **same** directory as LiquidHaskell itself (i.e. wherever
85-
`cabal` or `stack` puts your binaries). That is, do:
38+
2. Go inside the `liquidhaskell` directory:
8639

8740
```
88-
which liquid
41+
cd liquidhaskell
8942
```
9043
91-
and make sure that `z3` or `cvc4` or `mathsat` are in the `PATH`
92-
returned by the above.
44+
3. Build the package:
9345
94-
2. If you installed via `stack` and are experiencing path related woes, try:
46+
a. with [stack][stack]:
9547
96-
```
97-
stack exec -- liquid path/to/file.hs
98-
```
48+
stack install liquidhaskell
9949
100-
## Running the Legacy Binary
50+
b. or with [cabal][cabal]:
10151
102-
To verify a file called `foo.hs` at type
103-
104-
```bash
105-
$ liquid foo.hs
106-
```
52+
cabal v2-build liquidhaskell
10753
10854
## Running in GHCi
10955
@@ -115,6 +61,5 @@ ghci> :m +Language.Haskell.Liquid.Liquid
11561
ghci> liquid ["tests/pos/Abs.hs"]
11662
```
11763

118-
11964
[stack]: https://github.com/commercialhaskell/stack/blob/master/doc/install_and_upgrade.md
12065
[cabal]: https://www.haskell.org/cabal/

‎docs/mkDocs/docs/options.md

+92-91
Original file line numberDiff line numberDiff line change
@@ -5,18 +5,19 @@ checking.
55

66
To see all options, run `liquid --help`.
77

8-
Each option can be passed in at the command line, or directly
9-
added to the source file via a **pragma**
8+
You can pass options in different ways:
109

11-
```haskell
12-
{-@ LIQUID "option-within-quotes" @-}
13-
```
10+
1. From the **command line**, if you use the **legacy executable**:
1411

15-
for example, to disable termination checking (see below)
12+
liquid --opt1 --opt2 ...
1613

17-
```haskell
18-
{-@ LIQUID "--no-termination" @-}
19-
```
14+
2. As a **plugin option**:
15+
16+
ghc-options: -fplugin-opt=LiquidHaskell:--opt1 -fplugin-opt=LiquidHaskell:--opt2
17+
18+
3. As a **pragma**, directly added to the source file:
19+
20+
{-@ LIQUID "opt1" @-}
2021

2122
You may also put command line options in the environment variable
2223
`LIQUIDHASKELL_OPTS`. For example, if you add the line:
@@ -33,6 +34,10 @@ Below, we list the various options and what they are used for.
3334

3435
## Theorem Proving
3536

37+
**Options:** `reflection`, `ple`, `ple-local`, `extensionality`
38+
39+
**Directives:** `automatic-instances`
40+
3641
To enable theorem proving, e.g. as [described here](https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html)
3742
use the option
3843

@@ -65,15 +70,17 @@ liquid annotation
6570
{-@ automatic-instances theorem @-}
6671
```
6772

68-
To allow reasoning about function extensionality use the `extensionality flag`. [See](https://github.com/ucsd-progsys/liquidhaskell/blob/880c78f94520d76fa13880eac050f21dacb592fd/tests/pos/T1577.hs)
73+
To allow reasoning about function extensionality use the `--extensionality` flag.
74+
[See test T1577](https://github.com/ucsd-progsys/liquidhaskell/blob/880c78f94520d76fa13880eac050f21dacb592fd/tests/pos/T1577.hs).
6975

7076
```
7177
{-@ LIQUID "--extensionality" @-}
7278
```
7379

74-
7580
## Fast Checking
7681

82+
**Options:** `fast`, `nopolyinfer`
83+
7784
The option `--fast` or `--nopolyinfer` greatly recudes verification time, can also reduces precision of type checking.
7885
It, per module, deactivates inference of refinements during
7986
instantiation of polymorphic type variables.
@@ -82,18 +89,13 @@ functions are trivially refined.
8289

8390
## Incremental Checking
8491

85-
LiquidHaskell supports *incremental* checking where each run only checks
86-
the part of the program that has been modified since the previous run.
87-
88-
```
89-
$ liquid --diff foo.hs
90-
```
91-
92-
Each run of `liquid` saves the file to a `.bak` file and the *subsequent* run
92+
**Options:** `diff`
9393

94-
+ does a `diff` to see what has changed w.r.t. the `.bak` file
95-
+ only generates constraints for the `[CoreBind]` corresponding to the
96-
changed top-level binders and their transitive dependencies.
94+
The LiquidHaskell executable supports *incremental* checking where each run only checks
95+
the part of the program that has been modified since the previous run. Each run of `liquid` saves the file
96+
to a `.bak` file and the *subsequent* run does a `diff` to see what has changed w.r.t. the `.bak` file only
97+
generates constraints for the `[CoreBind]` corresponding to the changed top-level binders and their
98+
transitive dependencies.
9799

98100
The time savings are quite significant. For example:
99101

@@ -108,7 +110,7 @@ The time savings are quite significant. For example:
108110
Now if you go and tweak the definition of `spanEnd` on line 1192 and re-run:
109111

110112
```
111-
$ time liquid -d --notermination -i . Data/ByteString.hs > log 2>&1
113+
$ time liquid --diff --notermination -i . Data/ByteString.hs > log 2>&1
112114

113115
real 0m11.584s
114116
user 0m6.008s
@@ -130,24 +132,20 @@ the pragma:
130132

131133
{-@ LIQUID "--diff" @-}
132134

133-
134135
## Full Checking (DEFAULT)
135136

136-
To force LiquidHaskell to check the **whole** file (DEFAULT), use:
137-
138-
$ liquid --full foo.hs
139-
140-
to the file. This will override any other `--diff` incantation
141-
elsewhere (e.g. inside the file.)
142-
137+
**Options:** `full`
143138

144-
If you always want to run a given file with full-checking, add
145-
the pragma:
139+
You can force LiquidHaskell to check the **whole** file (which is the _DEFAULT_) using the `--full` option.
140+
This will override any other `--diff` incantation elsewhere (e.g. inside the file). If you always want
141+
to run a given file with full-checking, add the pragma:
146142

147143
{-@ LIQUID "--full" @-}
148144

149145
## Specifying Different SMT Solvers
150146

147+
**Options:** `smtsolver`
148+
151149
By default, LiquidHaskell uses the SMTLIB2 interface for Z3.
152150

153151
To run a different solver (supporting SMTLIB2) do:
@@ -167,26 +165,27 @@ dependencies). If you do so, you can use that interface with:
167165

168166
$ liquid --smtsolver=z3mem foo.hs
169167

170-
171168
## Short Error Messages
172169

170+
**Options:** `short-errors`
171+
173172
By default, subtyping error messages will contain the inferred type, the
174173
expected type -- which is **not** a super-type, hence the error -- and a
175174
context containing relevant variables and their type to help you understand
176175
the error. If you don't want the above and instead, want only the
177-
**source position** of the error use:
178-
179-
--short-errors
176+
**source position** of the error use `--short-errors`.
180177

181178
## Short (Unqualified) Module Names
182179

183-
By default, the inferred types will have fully qualified module names.
184-
To use unqualified names, much easier to read, use:
180+
**Options:** `short-names`
185181

186-
--short-names
182+
By default, the inferred types will have fully qualified module names.
183+
To use unqualified names, much easier to read, use `--short-names`.
187184

188185
## Disabling Checks on Functions
189186

187+
**Directives:** `ignore`
188+
190189
You can _disable_ checking of a particular function (e.g. because it is unsafe,
191190
or somehow not currently outside the scope of LH) by using the `ignore` directive.
192191

@@ -203,44 +202,44 @@ See `tests/pos/Ignores.hs` for an example.
203202

204203
## Totality Check
205204

205+
**Options:** `no-totality`
206+
206207
LiquidHaskell proves the absence of pattern match failures.
207208

208209
For example, the definition
209210

210-
fromJust :: Maybe a -> a
211-
fromJust (Just a) = a
211+
```haskell
212+
fromJust :: Maybe a -> a
213+
fromJust (Just a) = a
214+
```
212215

213216
is not total and it will create an error message.
214217
If we exclude `Nothing` from its domain, for example using the following specification
215218

216-
{-@ fromJust :: {v:Maybe a | (isJust v)} -> a @-}
219+
```haskell
220+
{-@ fromJust :: {v:Maybe a | (isJust v)} -> a @-}
221+
```
217222

218223
`fromJust` will be safe.
219224

220225
Use the `no-totality` flag to disable totality checking.
221226

222-
liquid --no-totality test.hs
223-
224227
## Termination Check
225228

226-
By **default** a termination check is performed on all recursive functions.
227-
228-
Use the `--no-termination` option to disable the check
229+
**Options:** `no-termination`
229230

230-
{-@ LIQUID "--no-termination" @-}
231-
232-
See the [specifications documentation][specifications] for how to write termination
233-
specifications.
231+
By **default** a termination check is performed on all recursive functions, but you can disable the check
232+
with the `--no-termination` option.
234233

234+
See the [specifications section](specifications.md) for how to write termination specifications.
235235

236236
## Total Haskell
237237

238+
**Options:** `total-Haskell`
239+
238240
LiquidHaskell provides a total Haskell flag that checks both totallity and termination of the program,
239241
overriding a potential no-termination flag.
240242

241-
liquid --total-Haskell test.hs
242-
243-
244243
## Lazy Variables
245244

246245
A variable can be specified as `LAZYVAR`
@@ -250,110 +249,112 @@ A variable can be specified as `LAZYVAR`
250249
With this annotation the definition of `z` will be checked at the points where
251250
it is used. For example, with the above annotation the following code is SAFE:
252251

253-
foo = if x > 0 then z else x
254-
where
255-
z = 42 `safeDiv` x
256-
x = choose 0
252+
```haskell
253+
foo = if x > 0 then z else x
254+
where
255+
z = 42 `safeDiv` x
256+
x = choose 0
257+
```
257258

258259
By default, all the variables starting with `fail` are marked as LAZY, to defer
259260
failing checks at the point where these variables are used.
260261

261262
## No measure fields
262263

264+
**Options:** `no-measure-fields`
265+
263266
When a data type is refined, Liquid Haskell automatically turns the data constructor fields into measures.
264267
For example,
265268

266-
{-@ data L a = N | C {hd :: a, tl :: L a} @-}
267-
268-
will automatically create two measures `hd` and `td`.
269-
To deactivate this automatic measure definition, and speed up verification, you can use the `no-measure-fields` flag.
270-
271-
liquid --no-measure-fields test.hs
272-
269+
```haskell
270+
{-@ data L a = N | C {hd :: a, tl :: L a} @-}
271+
```
273272

273+
will automatically create two measures `hd` and `td`. To deactivate this automatic measure definition,
274+
and speed up verification, you can use the `--no-measure-fields` flag.
274275

275276
## Prune Unsorted Predicates
276277

278+
**Options:** `prune-unsorted`
279+
277280
The `--prune-unsorted` flag is needed when using *measures over specialized instances* of ADTs.
278281

279282
For example, consider a measure over lists of integers
280283

281284
```haskell
282-
sum :: [Int] -> Int
283-
sum [] = 0
284-
sum (x:xs) = 1 + sum xs
285+
sum :: [Int] -> Int
286+
sum [] = 0
287+
sum (x:xs) = 1 + sum xs
285288
```
286289

287290
This measure will translate into strengthening the types of list constructors
288291

289292
```
290-
[] :: {v:[Int] | sum v = 0 }
291-
(:) :: x:Int -> xs:[Int] -> {v:[Int] | sum v = x + sum xs}
293+
[] :: {v:[Int] | sum v = 0 }
294+
(:) :: x:Int -> xs:[Int] -> {v:[Int] | sum v = x + sum xs}
292295
```
293296

294297
But what if our list is polymorphic `[a]` and later instantiate to list of ints?
295298
The workaround we have right now is to strengthen the polymorphic list with the
296299
`sum` information
297300

298301
```
299-
[] :: {v:[a] | sum v = 0 }
300-
(:) :: x:a -> xs:[a] -> {v:[a] | sum v = x + sum xs}
302+
[] :: {v:[a] | sum v = 0 }
303+
(:) :: x:a -> xs:[a] -> {v:[a] | sum v = x + sum xs}
301304
```
302305

303306
But for non numeric `a`s, refinements like `x + sum xs` are ill-sorted!
304307

305308
We use the flag `--prune-unsorted` to prune away unsorted expressions
306309
(like `x + sum xs`) inside refinements.
307310

308-
309-
```
310-
liquid --prune-unsorted test.hs
311-
```
312-
313-
314311
## Case Expansion
315312

313+
**Options:** `no-case-expand`
314+
316315
By default LiquidHaskell expands all data constructors to the case statements.
317316
For example, given the definition
318317

319318
```haskell
320-
data F = A1 | A2 | .. | A10
319+
data F = A1 | A2 | .. | A10
321320
```
322321

323322
LiquidHaskell will expand the code
324323

325324
```haskell
326-
case f of {A1 -> True; _ -> False}
325+
case f of {A1 -> True; _ -> False}
327326
```
328327

329328
to
330329

331330
```haskell
332-
case f of {A1 -> True; A2 -> False; ...; A10 -> False}
331+
case f of {A1 -> True; A2 -> False; ...; A10 -> False}
333332
```
334333

335334
This expansion can lead to more precise code analysis
336335
but it can get really expensive due to code explosion.
337-
The `no-case-expand` flag prevents this expansion and keeps the user
336+
The `--no-case-expand` flag prevents this expansion and keeps the user
338337
provided cases for the case expression.
339338

340-
liquid --no-case-expand test.hs
341-
342-
343339
## Higher order logic
344340

345-
The flag `--higherorder` allows reasoning about higher order functions.
341+
**Options:** `higherorder`
346342

343+
The flag `--higherorder` allows reasoning about higher order functions.
347344

348345
## Restriction to Linear Arithmetic
349346

347+
**Options:** `linear`
348+
350349
When using `z3` as the solver, LiquidHaskell allows for non-linear arithmetic:
351350
division and multiplication on integers are interpreted by `z3`. To treat division
352-
and multiplication as uninterpreted functions use the `linear` flag
351+
and multiplication as uninterpreted functions use the `--linear` flag.
352+
353+
## Counter examples
353354

354-
liquid --linear test.hs
355+
**Options:** `counter-examples`
355356

356-
## Counter examples (Experimental!)
357+
**Status:** `experimental`
357358

358359
When given the `--counter-examples` flag, LiquidHaskell will attempt to produce
359360
counter-examples for the type errors it discovers. For example, see
@@ -407,4 +408,4 @@ verification attempts.
407408
your system. If not, `hscolour` is used to render the HTML.
408409

409410
It is also possible to generate *slide shows* from the above.
410-
See the [slides directory](docs/slides) for an example.
411+
See the [slides directory](https://github.com/ucsd-progsys/liquidhaskell/tree/develop/docs/slides) for an example.

‎docs/mkDocs/docs/plugin.md

+12-15
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,8 @@
33
As of LH version 0.8.10, mirroring GHC-8.10, LiquidHaskell
44
is available as a [GHC compiler plugin](https://downloads.haskell.org/~ghc/8.10.1/docs/html/users_guide/extending_ghc.html).
55

6-
(We still offer a [legacy executable](legacy.md) which uses
7-
the plugin internally, to give users enough time to complete
8-
migrations to the new system.)
6+
(We still offer the old [legacy executable](legacy.md), to give users enough time to complete migrations
7+
to the new system.)
98

109
## Benefits
1110

@@ -19,19 +18,19 @@ of your project in the cabal file, after which `stack` or `cabal` automatically:
1918

2019
**We recommend switching to the new compiler plugin as soon as possible.**
2120

22-
## Installation and Use
21+
## External software requirements
2322

24-
1. Install an SMT Solver Download and install at least one of
23+
Make sure all the required [external software](install.md) software is installed before proceeding.
2524

26-
Z3 or Microsoft official binary
27-
CVC4
28-
MathSat
25+
## Getting started
2926

30-
Note: The SMT solver binary should be on your PATH; LiquidHaskell will execute it as a child process.
27+
We offer a detailed "getting started" walkthrough in the form of a Haskell module with a lot of comments,
28+
written in prose. You can read it [here](https://github.com/ucsd-progsys/liquidhaskell/tree/develop/src/Language/Haskell/Liquid/GHC/Plugin/Tutorial.hs).
3129

32-
The following concrete examples show how the source plugin works
30+
## Examples
31+
32+
The following concrete examples show the source plugin in action:
3333

34-
- [Tutorial documentation](src/Language/Haskell/Liquid/GHC/Plugin/Tutorial.hs)
3534
- [Sample package](https://github.com/ucsd-progsys/lh-plugin-demo)
3635
- [Sample client package](https://github.com/ucsd-progsys/lh-plugin-demo-client)
3736

@@ -41,7 +40,5 @@ codebase.
4140

4241
## Editor Support
4342

44-
**In plugin-mode** you get to automatically reuse **all** `ghc`
45-
based support for your editor as is. Again, the sample packages
46-
include examples for `vscode`, `vim` and `emacs`.
47-
43+
One of the added benefit of the plugin is that you get to automatically reuse **all** ghc-based support
44+
for your editor as is. Again, the sample packages include examples for `vscode`, `vim` and `emacs`.

‎docs/mkDocs/docs/specifications.md

+242-248
Large diffs are not rendered by default.

‎docs/mkDocs/mkdocs.yml

+15-9
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,19 @@
1-
site_name: LiquidHaskell
1+
site_name: LiquidHaskell
22

33
nav:
4-
- Online: "https://liquid-demo.programming.systems/index.html"
5-
- Blog: "https://ucsd-progsys.github.io/liquidhaskell-blog/"
6-
- Plugin: plugin.md
7-
- Legacy: legacy.md
8-
- Options: options.md
9-
- Specifications: specifications.md
10-
- Community: contributing.md
11-
- Development: develop.md
4+
- Home: index.md
5+
- Install: plugin.md
6+
- Play: "https://liquid-demo.programming.systems/index.html"
7+
- Learn:
8+
- Blog: "https://ucsd-progsys.github.io/liquidhaskell-blog/"
9+
- Options: options.md
10+
- Specifications: specifications.md
11+
- "Get Involved": contributing.md
12+
- "<i class='fa fa-github'></i>&nbsp;Github": "https://github.com/ucsd-progsys/liquidhaskell"
13+
1214

1315
theme: litera
16+
17+
markdown_extensions:
18+
- toc:
19+
permalink: true

0 commit comments

Comments
 (0)
Please sign in to comment.