Skip to content
master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
 
 
src
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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/

  • 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