LiquidHaskell Tutorial
TODO: UPDATE the website with the new code
NOTE The PDF/HTML are sometimes not up-to-date with the latest LiquidHaskell release. Please clone the github repository and run locally for best results.
How to Do The Tutorial
LH is available as a GHC plugin from version 0.8.10.
Thus, the best way to do this tutorial is to
Step 1 Clone this repository,
$ git clone --recursive https://github.com/ucsd-progsys/liquidhaskell-tutorial.git
Step 2: Iteratively edit-compile until it builds without any liquid type errors
$ cabal v2-build
or
$ stack build --fast --file-watch
The above workflow will let you use whatever Haskell tooling you use for your favorite editor, to automatically display LH errors as well.
Contents
Part I: Refinement Types
Part II: Measures
Part III : Case Studies
- Case Study: Okasaki's Lazy Queues
- Case Study: Associative Maps
- Case Study: Pointers & Bytes
- Case Study: AVL Trees
Update
$ git pull origin master
$ git submodule update --recursive
Building
Deploy on Github
Step 1
Do we really need to install pandoc-citeproc
?
$ mv package.yaml.pandoc package.yaml
$ stack install pandoc template
$ make html
$ make pdf
$ make upload
Prerequisites
$ cd ../ && git clone https://github.com/ucsd-progsys/liquid-client.git
Dependencies
$ stack install pandoc pandoc-citeproc template
Prerequisites
- Install LaTeX dependencies:
- Texlive
- texlive-latex-extra
- texlive-fonts-extra
Producing .pdf Book
$ make pdf
$ evince dist/pbook.pdf
Solutions to Exercises
Solutions are in separate private repo
TODO
A work list of TODO items can be found in the bug tracker
Feedback and Gotchas
Editing feedback and various gotchas can be found in feedback.md