Commit 1ca025d0 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Compilation instructions

parent cad483e2
......@@ -41,6 +41,9 @@ language that eases the definition of mathematical structures and the
automation of proofs and for which a translator to Dedukti exists.
* Installation
** Dependencies
The following tools are required to compile the MathTransfer library:
For the core of the library:
......@@ -55,7 +58,7 @@ For the core of the library:
Sukerujo is an alternative Dedukti parser used by FoCaLiZe
- Zenon Modulo version 0.4.2
- Zenon Modulo version 0.4.3
For the interoperability library, the following extra tools are
required to import logical developments from other proof systems:
......@@ -85,6 +88,32 @@ required to import logical developments from other proof systems:
limits the dependencies on non-constructive axioms by taking
implication and universal quantification as primitives.
** Installing dependencies
All dependencies but the OpenTheory tool are written in OCaml and
packaged using Opam.
To install OpenTheory, please refer to http://www.gilith.com/software/opentheory/download.html
If you have Opam installed, you can download and install all
other dependencies by typing
#+BEGIN_SRC bash
$ opam repository add deducteam https://gforge.inria.fr/git/opam-deducteam/opam-deducteam.git
$ opam update
$ opam install focalize=0.9.2 dedukti=2.5 sukerujo=2.5 zenon_modulo_focalide=0.4.3 coq=8.4.6 coqine=0.4 holide=0.2.1~holala
#+END_SRC
** Building the library
To build the library, type the following commands:
#+BEGIN_SRC bash
$ ./configure
$ make
#+END_SRC
* Detailed Content of the MathTransfer library
** Core
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment