BIRDS

More information about BIRDS is available at https://dangtv.github.io/BIRDS/

Installation

To install the birds command line tool, download a birds binary file at https://github.com/dangtv/BIRDS/releases or build a birds binary file from the source code.
To build the birds command line tool, the following softwares must be installed:
- GNU Make >= 4.1
- ocaml >= 4.07.0: see OCaml's installation guidance
- Ocaml packages:
  - num (>= 1.0): opam install num
  - postgresql-ocaml (>=4.0.1): opam install postgresql

Compiling:

Clean:
```
make clean
```
Build:
```
make all
```
Release:
```
make release
```
Install:
```
make install
```

See the usage of the birds command by typing:

birds --help

Integrated systems

BIRDS is integrated with other systems to enable some features (verification, counterexample generation, ...) of the birds command. These systems can be installed as follows:

PostgreSQL database >= 9.6: https://www.postgresql.org/download/
- PL/sh extension for PostgreSQL (for only option --dejima): available at https://github.com/petere/plsh
Z3 >= 4.8.7: The binary files can be downloaded at https://github.com/Z3Prover/z3/releases. To install the z3 command, create a symbolic link in /usr/bin to the z3 binary file:
```
ln -s <path-to-the-z3-binary-file> /usr/bin/z3
```
Lean >= 3.4.2: The binary files can be downloaded at https://github.com/leanprover/lean/releases. To install Lean commands, create symbolic links in /usr/bin as follows:
```
ln -s <path-to-the-lean-binary-file> /usr/bin/lean 
ln -s <path-to-the-leanpkg-binary-file> /usr/bin/leanpkg 
ln -s <path-to-the-leanchecker-binary-file> /usr/bin/leanchecker 
```
The Lean package of BIRDS must be configured and compiled as follows:
- Configuration: add a new file /Users/<user_name>/.lean/leanpkg.path on MacOS or /root/.lean/leanpkg.path on Linux with the following content(replace <path_to_BIRDS> with the absolute path to the BIRDS source code folder):
```
  builtin_path
  path <path_to_BIRDS>/verification/_target/deps/mathlib/src
  path <path_to_BIRDS>/verification/src
  path <path_to_BIRDS>/verification/_target/deps/super/src
```
- Installing coreutils:
  - For Ubuntu: apt-get install coreutils.
  - For MacOS: brew install coreutils and then create a symbolic link ln -s /usr/local/bin/gtimeout /usr/local/bin/timeout
- Compilation: To compile the Lean package of BIRDS, type:
```
cd BIRDS/verification
leanpkg configure
leanpkg build
```
Rosette: After installing Racket (Minimal Racket can work well, for macos, brew install minimal-racket), Rosette can be installed by raco pkg install rosette.

To check whether the required external tools and configurations (except PostgreSQL) are installed properly, run birds --environment.

Docker

The docker image that contains all the features and the integrated systems of BIRDS can be built by:

  docker build -t "birds" .

In this docker image, the PostgreSQL database runs on port 5432 and the BIRDS WebUI runs on port 3010

gfngfn/BIRDS

BIRDS

Installation

Integrated systems

Docker