Welcome! This workshop is planned as a beginner-friendly hacking session where we want you to get your hands dirty coding liquid haskell. Please bring your laptop to the workshop!
To not waste time on installation problems during the workshop, we kindly ask you to perform the installation instructions before the workshop. Thank you 🤗 !
If you are not familiar with haskell, the easiest and recommended way to get started is using docker. We have prepared a liquid haskell docker image that comes with batteries included so you don't have to worry about anything! Please proceed to use docker image.
If you are familiar with haskell, you can also proceed to install liquid haskell locally.
If you are not using docker yet, install docker following the instructions here: https://www.docker.com/get-started.
If you are familiar with git you can just clone the repository:
git clone https://github.com/janschultecom/20181025-strongly-typed-martini.git
cd 20181025-strongly-typed-martiniIf you are not familiar with git you can also download the repository as a zip file:
1. click on 'Clone or download'
2. click on 'Download ZIP'
3. unzip the file
4. open command prompt and change to the directory
You can find more detailed instructions on how to clone or download a repository here: https://help.github.com/articles/cloning-a-repository/.
Now that you got docker installed and the repository cloned, you can run the liquid haskell container:
Mac Os / Linux
docker run -ti -v $(PWD):/data janschultecom/docker-liquidhaskell:latestWindows
docker run -ti -v %cd%:/data janschultecom/docker-liquidhaskell:latestThis will start to download the liquid haskell docker container and enter the command prompt of the container:
root@7d8d5dc51645:/data# Note: This may take a few minutes and might look slightly different on your computer.
In the container check the exercise liquid haskell file by running the liquid command:
root@7d8d5dc51645:/data# liquid --full src/haskell/Exercise1.hsYou should get the following output:
**** DONE: A-Normalization ****************************************************
**** DONE: Extracted Core using GHC *******************************************
**** DONE: Transformed Core ***************************************************
Working 150% [==================================================================================================]
**** DONE: annotate ***********************************************************
**** RESULT: SAFE **************************************************************
If you see this, you are good to go 🙌 ! You don't have to do anything else! See you at the workshop!
Requirements:
- SMTLIB2 compatible solver installed and its executable found on PATH (in our case Z3)
- Linux:
sudo apt-get install z3 - Mac OS:
brew install z3
$ wget -qO- https://get.haskellstack.org/ | sh
In order to have stack installed executable availables we need to modify the $PATH. To do that, please add the following line to your ~/.bashrc or ~/.zshrc
export PATH=$HOME/.local/bin:$PATH
And now we proceed to install Liquid Haskell
$ git clone --recursive https://github.com/ucsd-progsys/liquidhaskell.git ~/liquidhaskell
$ cd ~/liquidhaskell
$ stack install
(Please be sure you went through the upper section)
To get started with this repository you can easily do:
$ stack install
So you can get the proper GHC version and dependencies installed.
Check the exercise liquid haskell file by running the 'liquid' command:
liquid --full src/haskell/Exercise1.hsIf you have trouble using the installation methods, you can alternatively use the web editor. Please bear in mind that the server is a little flaky and might not work reliably during the workshop.
Note: If you see an odd/even example, please refresh your browser.