dangtv/birds repository overview

⁠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
    

    Copy
  • Build:

    make all
    

    Copy
  • Release:

    make release
    

    Copy
  • Install:

    make install
    

    Copy

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
  

  Copy

• 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 
  

  Copy

  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
    

    Copy
  • 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
    

    Copy

• 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