Skip to content

Commit

Permalink
Updated README.md. with set up instructions.
Browse files Browse the repository at this point in the history
  • Loading branch information
@duncanatt
duncanatt committed Oct 8, 2024
1 parent 09b910f commit 6845a91
Showing 1 changed file with 112 additions and 26 deletions.
138 changes: 112 additions & 26 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,35 +18,38 @@ The current type-checking pipeline consists of these stages:
paterl:compile("src/examples/erlang/codebeam/id_server_demo.erl", [{includes, ["include"]}, {out, "out"}]).
```

## Using from command line
## Using from the terminal

```shell
./src/paterl src/examples/erlang/codebeam/id_server_demo.erl -v all -I include
```

---

# Installing the `paterl` toolchain

The following instructions detail how `paterl` can be installed on MacOS, Ubuntu, and Windows.

Some of the installation steps below are common to different installations and this guide identifies them accordingly by the corresponding operating system icon on which steps should be executed.
<!-- Some of the installation steps below are common to different installations and this guide identifies them accordingly by the corresponding operating system icon on which steps should be executed. -->

<img src="https://raw.githubusercontent.com/FortAwesome/Font-Awesome/6.x/svgs/brands/apple.svg" width="20" height="20"> <img src="https://raw.githubusercontent.com/FortAwesome/Font-Awesome/6.x/svgs/brands/ubuntu.svg" width="20" height="20"> <img src="https://raw.githubusercontent.com/FortAwesome/Font-Awesome/6.x/svgs/brands/windows.svg" width="20" height="20">
<!-- <img src="https://raw.githubusercontent.com/FortAwesome/Font-Awesome/6.x/svgs/brands/apple.svg" width="20" height="20"> <img src="https://raw.githubusercontent.com/FortAwesome/Font-Awesome/6.x/svgs/brands/ubuntu.svg" width="20" height="20"> <img src="https://raw.githubusercontent.com/FortAwesome/Font-Awesome/6.x/svgs/brands/windows.svg" width="20" height="20"> -->

## Install the Windows Subsystem for Linux

The simplest and ideal way to install `paterl` on Windows is to use the Windows Subsystem for Linux (WSL).
WSL provides virtualised Linux environment on Hyper-V.
While WSL can access your Windows file system, software installed on the virtualised Linux environment is isolated from and cannot be accessed by Windows, and vice versa
While WSL can access your Windows file system, software installed on the virtualised Linux environment is isolated from and cannot be accessed by Windows, and vice versa.
This means that packages (e.g. Erlang) installed on Windows must also be installed in the virtualised Linux environment to be available to Linux.

1. By default, WSL installs the latest Ubuntu distribution.
This is done by typing the following on your terminal or PowerShell:

```bash
wsl --install
C:\> wsl --install
C:\> wsl
```

2. After the installation completes, update your Ubuntu environment to the latest packages.
2. After the installation completes, update your Ubuntu virtual environment to the latest packages.

```bash
$ sudo apt update && sudo apt upgrade
Expand Down Expand Up @@ -77,7 +80,7 @@ $ cd /mnt/c/Users/your-username/Desktop

We start by installing `opam`, the OCaml package manager.

1. The easiest way to install on WSL and Ubuntu is via `apt`:
1. The easiest way to install `opam` on WSL and Ubuntu is via `apt`:

```bash
$ sudo apt install opam
Expand All @@ -103,7 +106,7 @@ We start by installing `opam`, the OCaml package manager.
$ eval $(opam env --switch=default)
```

**This step is required whenever you wish to interact with `opam` to install packages.**
**This step is required whenever you wish to interact with `opam` in a fresh terminal to install or build packages.**

4. Now that `opam` is successfully installed, we can install the common OCaml platform tools.
These are required to run or develop OCaml applications.
Expand Down Expand Up @@ -131,8 +134,8 @@ We start by installing `opam`, the OCaml package manager.

1. To install Z3 on WSL and Ubuntu, type:

```
sudo apt install z3
```bash
$ sudo apt install z3
```

On macOS, Z3 is installed using Homebrew as follows:
Expand All @@ -150,28 +153,39 @@ We start by installing `opam`, the OCaml package manager.
For usage information: z3 -h
```

## Setting up your development directory

Before downloading the necessary components to set up the `paterl` toolchain on your system, create a new directory where all the development source code will be cloned from GitHub.

```bash
$ mkdir Development
$ cd Development
```

Feel free to change the `Development` directory to one that fits your system configuration set-up.

## Setting up Pat

Pat is the OCaml backend component to `paterl`.
It processes programs written in the Pat language and uncovers communication errors.
The `paterl` Erlang frontend synthesises Pat programs from Erlang source code and launches the Pat type checker as a shell process and retrieves potential errors generated by Pat.
These Pat-generated errors are processed by `paterl` and presented to the user in the form of Erlang errors.
It processes programs written in the Pat language, and reports communication errors.
The `paterl` Erlang frontend synthesises Pat programs from Erlang source code and launches the Pat type checker as a shell process, retrieving any errors reported by Pat.
These errors are post-processed by `paterl` and presented to the user in the form of Erlang errors.

1. Install the Pat OCaml dependencies.
These dependencies include the Z3 OCaml bridge, which is used by Pat to solve pattern inclusion constraints to uncover communication errors in Pat programs.
These dependencies include the Z3 OCaml bridge, which is used by Pat to solve pattern inclusion constraints to ensure that there are no communication errors in Pat programs.
The dependencies can be installed via `opam` as shown.

```bash
$ opam install ppx_import visitors z3 bag cmdliner
```

2. Clone the Pat type checker Git repository:
2. Clone the Pat type checker GitHub repository:

```bash
git clone https://github.com/SimonJF/mbcheck.git
$ git clone https://github.com/SimonJF/mbcheck.git
```

3. The `paterl`-Pat integration is currently implemented as an experimental branch, and is required by `paterl`.
3. The `paterl`-Pat integration is currently implemented as an experimental branch and is required by `paterl`.
Switch the Pat development branch to `paterl-experiments`

```
Expand All @@ -185,12 +199,14 @@ These Pat-generated errors are processed by `paterl` and presented to the user i
$ make
```

4. Finally, test your Pat type checker installation by running one of the many Pat examples:
4. Lastly, test your Pat type checker installation by running one of the many Pat examples:

```bash
$ ./mbcheck test/examples/de_liguoro_padovani/future.pat
```

No errors should be reported.

## Installing Erlang/OTP

Our `paterl` frontend requires Erlang/OTP > 26.
Expand All @@ -205,7 +221,7 @@ The RabbitMQ PPA is valid for Ubuntu 22.04 and 20.04.
$ sudo apt install erlang
```

If you have already installed Erlang from the Ubuntu repository, it will be upgraded to the version given in the PPA.
If you have already installed Erlang from the Ubuntu repository, it will be upgraded to the version given in the RabbitMQ PPA.

2. Test your installation by launching the Erlang shell:

Expand All @@ -220,7 +236,7 @@ The RabbitMQ PPA is valid for Ubuntu 22.04 and 20.04.
3. Quit the shell by typing:
```erlang
q().
1> q().
```
### Removing Erlang
Expand All @@ -238,20 +254,90 @@ If you wish to completely remove Erlang, type:
$ sudo apt remove erlang
```
## Setting up `paterl`
## Set up `paterl`
The last step is to set up `paterl`, the Erlang front-end tool used to process Erlang files.
## Step 1: Clone paterl
1. Clone the `paterl` Git repository:
```
git clone
```
```bash
$ git clone https://github.com/duncanatt/paterl.git
```
2. Set the path for the Pat type checker, `mbcheck`.
The `paterl` Erlang frontend must point to the `mbcheck` tool to type check the Pat source code files it synthesises.
Open the `paterl.erl` file located in `src/` and edit the `EXEC` macro at the top, pointing it to the directory containing the **compiled** `mbcheck` binary.
For instance,
```erlang
-define(EXEC, "/home/duncan/Development/mbcheck/mbcheck").
```
Save the file.
3. Build the `paterl` Erlang front-end using the included `Makefile`:
```bash
$ make
```
4. Finally, test your `paterl` installation by running one of the many included examples:
```bash
$ ./src/paterl src/examples/erlang/codebeam/id_server_demo.erl -v all -I include
```
You should see the following output on your terminal:
```bash
[WRITE] Writing temporary Pat file ebin/id_server_demo.
[PAT] Pat'ting ebin/id_server_demo.
[PAT] Successfully type-checked ebin/id_server_demo.erl.
```
## Troubleshooting
- If `mbcheck` fails to build and complains with errors similar to the one below, it means that the `opam` environment is not initialised in your active shell.
```bash
$ make
/bin/sh: 1: dune: not found
```
Reinisialize your `opam` environment using
```bash
$ eval $(opam env --switch=default)
```
and rebuild `mbcheck`.
- If errors like the one below occur when testing `paterl`, it means that your `EXEC` macro in the `src/paterl.erl` Erlang module is misconfigured and points to an incorrect `mbcheck` binary.
In the excerpt below, the binary is mistyped as `mbcheckk`.
```bash
[WRITE] Writing temporary Pat file ebin/id_server_demo.
[PAT] Pat'ting ebin/id_server_demo.
Error: sh: /home/duncan/Development/mbcheck/mbcheckk: No such file or directory
sh: line 0: exec: /home/duncan/Development/mbcheck/mbcheckk: cannot execute: No such file or directory
```
Make the necessary modification to the `EXEC` macro and rebuild `paterl`.
## (Optional) Install and configure VS Code
You may wish to set up VS Code as your default source code editor.
We recommend the following extensions that provide syntax highlighting, debugging, and building support for OCaml and Erlang projects.
- [OCaml Platform](https://marketplace.visualstudio.com/items?itemName=ocamllabs.ocaml-platform)
- [Erlang/OTP](https://marketplace.visualstudio.com/items?itemName=yuce.erlang-otp)
These extensions work for VS Code on MacOS, Ubuntu, and Windows.
We also recommend the [WSL](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-wsl) extension which directly integrates into your Windows WSL set-up.
This extension enables you to load and execute code directly into your virtualised WSL environment and accesses the WSL shell from within VS Code.
Note that code extensions, such as the OCaml Platform and Erlang/OTP extensions, need to be **installed** separately for WSL from VS Code.
## Insall and configure VS Code

0 comments on commit 6845a91

Please sign in to comment.