View on GitHub

Andromeda 2

A proof checker for user-definable dependent type theories

Andromeda is implemented in OCaml and relies on the OPAM package manager for installation. Please make sure you have a recent working OCaml & OPAM.

Execute the following command to get and install Andromeda:

opam pin add andromeda git+https://github.com/Andromedans/andromeda

How to compile Andromeda

If you would like to compile Andromeda yourself, follow these instructions.

Prerequisites

You need OCaml 4.12 or later, and quite possibly it works with earlier versions, and several OCaml packages, which you can install by running

opam install dune dune-build-info dune-site menhir sedlex

If you also install the ledit or rlwrap utility, the Andromeda toplevel will use them to give you line editing capabilities.

Compilation

Checkout the Andromeda repository

git clone git@github.com:Andromedans/andromeda.git

or consider forking it if you indent do experiment with it, or contribute to the project.

To build Andromeda, run the command

dune build

in the andromeda folder. This will create the executable ./andromeda.exe. You can also run tests with

dune runtest

If you see no input, the tests passed.

Usage

You may run the compiled executable andromeda.exe. For basic usage and command-line options, run

./andromeda.exe --help