MirrorCore is a library for extensible reflective automation. It includes two main components.

• Lambda -- a simply typed lambda calculus to use as the reflective core language
• RTac -- a reflective tactic language modeled on Ltac.

The system is described at a mathematical level in two works:

• Extensible Proof Engineering in Intensional Type Theory by Gregory Malecha (PhD Dissertation)
• Extensible and Efficient Automation through Reflective Tactics by Gregory Malecha & Jesper Bengtson (ESOP'16)

If you find a bug, please report it on github: https://github.com/gmalecha/mirror-core/issues

Add the Coq repository:

opam repo add coq-released https://coq.inria.fr/opam/released

and run:

opam install coq-mirror-core

To get the beta versions of Coq, activate the repository:

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev

This version of MirrorCore builds on Coq 8.5.

(In the following commands 'mirror-core' refers to the root directory of mirror-core)

(If you need to set up dependencies, please see the next section first)

To build the library, run:

mirror-core/ $ make -jN

in the main directory.

You can build the examples by running

mirror-core/examples/ $ make -jN

in the examples directory.

MirrorCore depends on two external libraries.

• coq-ext-lib
• coq-plugin-utils (to build the plugins)

Both of these can be installed using opam, provided you have added the repository described above.

opam install coq-ext-lib coq-plugin-utils

coq-plugin-utils needs to be installed, you should follow the directions in the README.md in that repository.

coq-ext-lib does not need to be installed.

If you do install it, simply touch coq-ext-lib in the mirror-core folder to prevent pulling a fresh copy.

mirror-core/ $ touch coq-ext-lib

If you already have a copy of coq-ext-lib on your system but it is not installed, you can create a symbolic link to it in the mirror-core directory.

ln -s <path/to/coq-ext-lib> coq-ext-lib

If you do not have a local copy already you can run

mirror-core/ $ make init

which will pull a fresh copy of coq-ext-lib and build it.

In order to build the reification plugin, you must use OCaml 4.01 or later.