Commit 0d0c865f authored by Raphael Cauderlier's avatar Raphael Cauderlier

Move to the last stable versions of Dedukti and Meta Dedukti and

update installation instructions
parent 1257313e
......@@ -12,53 +12,36 @@ For a description of Dktactics, see the [[./manual.org][manual]].
* Dependencies
To check and compile the files, you need Dedukti v2.5.
To check and compile the files, you need Dedukti v2.5.1.
For interactive development and conversion from certificates to
genuine proofs, Meta Dedukti v2.5 is required.
genuine proofs, Meta Dedukti v2.5.1 is required.
For interactive development, Meta Sukerujo is recommended.
# Optionally, confluence of the [[./fol][fol]] directory can be checked by CSI^HO.
Optionally, confluence of the [[./fol][fol]] directory can be checked by CSI^HO.
* Installation
* Installation of dependencies
To install Dedukti and Meta Dedukti, clone the =meta= branch of
Dedukti git repository
The simplest way to install Dktactics and its dependencies is to use the Opam package manager.
#+BEGIN_SRC bash
git clone -b meta https://scm.gforge.inria.fr/anonscm/git/dedukti/dedukti.git
$ opam repository add deducteam https://gforge.inria.fr/git/opam-deducteam/opam-deducteam.git
$ opam update
$ opam install dktactics
#+END_SRC
then compile and install the programs:
#+BEGIN_SRC bash
cd dedukti/
make
make install
#+END_SRC
If you prefer to install from sources, then follow the instructions on
https://github.com/Deducteam/Dedukti/blob/master/README.md to install
Dedukti and on http://deducteam.gforge.inria.fr/metadedukti/ to
install Meta Dedukti.
To install Meta Sukerujo, clone the =skmeta= branch instead
Then to configure, build, and install Dktactics, run the following
commands:
#+BEGIN_SRC bash
git clone -b skmeta https://scm.gforge.inria.fr/anonscm/git/dedukti/dedukti.git meta_sukerujo
cd meta_sukerujo/
make
make install
$ ./configure
$ make
$ make install
#+END_SRC
CSI^HO can be downloaded from [[http://cl-informatik.uibk.ac.at/software/csi/ho/]]
* Installation of Dktactics
Invoke the =configure= script to produce the file =.config_vars=
containing the path to the dependencies.
# CSI^HO can be downloaded from [[http://cl-informatik.uibk.ac.at/software/csi/ho/]]
#+BEGIN_SRC bash
./configure
#+END_SRC
Then compile all the Dedukti files
#+BEGIN_SRC bash
make
#+END_SRC
......@@ -117,9 +117,9 @@ done
# Ensures that the file ".config_vars" exists and is empty
echo > .config_vars &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5.1" &&
find_and_check_binary "dkdep" ".native" "DKDEP" "" "" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Dedukti v2.5" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti v2.5.1" &&
#find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.6" &&
#find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Sukerujo v2.6" &&
......
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