Commit ac14e305 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Update README

parent 97661837
......@@ -51,7 +51,7 @@ SKDEP=skdep
DKDEP=dkdep
DKMETA=../dedukti/dkmeta.native
CONFLUENCECHECKER=$(shell locate csiho.sh)
CCOPT=-cc $(CONFLUENCECHECKER)
CCOPT= # -cc $(CONFLUENCECHECKER)
DKCHECKOPTIONS=-v -d $(CCOPT)
DKDEPOPTIONS=-v
......
......@@ -38,12 +38,26 @@ knowledge of the CeCILL-B license and that you accept its terms.
* Installation
** Dependencies
Sigmaid has the same dependencies than Dedukti :
Sigmaid depends on the following tools :
- OCaml
- Menhir
- GNU Make
Sigmaid produces files for Dedukti and Coq.
*** If you are interested in the Coq output, then you also need Coq
*** If you are interested in the Dedukti output, then you also need the following tools :
- Dedukti (version 2.5)
Sigmaid uses an experimental feature of Dedukti called
MetaDedukti. At time of writing (January 2017), the only way to
install this is by source.
Follow the compilation instructions on [[http://dedukti.gforge.inria.fr/manual_v2_5.html][Dedukti manual]] using the
branch "meta" instead of "v2.5".
- [[http://deducteam.gforge.inria.fr/sukerujo/][Sukerujo]] (version 2.5)
The Dedukti files produced by Sigmaid are to be parsed with Sukerujo.
** Source code
......@@ -52,16 +66,22 @@ knowledge of the CeCILL-B license and that you accept its terms.
#+BEGIN_SRC sh
git clone git://scm.gforge.inria.fr/sigmaid/sigmaid.git
#+END_SRC
- [[http://sigmaid.gforge.inria.fr/sigmaid.tgz][as a tarball]]
- [[http://sigmaid.gforge.inria.fr/sigmaid.tgz][as a tarball]] (outdated)
** Compilation
To compile, simply invoke
To compile, invoke
#+BEGIN_SRC sh
make
make sigmaid
#+END_SRC
in Sigmaid's directory.
By default, Sigmaid is compiled natively. If you want to use OCaml
bytecode compilation instead, invoke
#+BEGIN_SRC sh
make COMPILE_MODE=byte sigmaid
#+END_SRC
** Installation
If you want Sigmaid to be installed system-wide, and if you have
......@@ -70,17 +90,22 @@ knowledge of the CeCILL-B license and that you accept its terms.
make install
#+END_SRC
This will install Sigmaid in the directory =/usr/local/bin=. If you
prefer to install Sigmaid in some other directory =<MYDIRECTORY>=,
then instead invoke
#+BEGIN_SRC sh
make INSTALL_DIR=<MYDIRECTORY> install
#+END_SRC
** Check
Sigmaid comes with a small example file =test.sigma=. If you have
Dedukti (v 2.2) installed, you can check this example with Dedukti
using the command
Sigmaid comes with a small example file =test.sigma=. You can
check this example with Dedukti using the command
#+BEGIN_SRC sh
make test.dko
#+END_SRC
If you have Coq installed, you can check this example with Coq
using the command
You can check this example with Coq using the command
#+BEGIN_SRC sh
make test.vo
#+END_SRC
......@@ -91,9 +116,9 @@ knowledge of the CeCILL-B license and that you accept its terms.
#+END_SRC
* Further reading
Sigmaid is described in [[https://hal.inria.fr/hal-01097444][this article]].
Sigmaid is described in [[https://hal.inria.fr/hal-01097444][this article]] and in the second part of [[https://hal.inria.fr/tel-01415945][this PhD thesis]].
The Dedukti files presented there are:
The Dedukti files presented in the article are:
- [[file:dk_domain.dk][=dk_domain.dk=]] corresponding to Section 4.1.1 (Domains),
- [[file:dk_type.dk][=dk_type.dk=]] corresponding to the other definitions and proofs of Section 4.1 (Encoding of types),
- [[file:dk_obj.dk][=dk_obj.dk=]] corresponding to Sections 4.2 (Encoding of terms) and 5.1 (Modified rewrite system)
......
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