Logipedia is a project that aims to translate and share formal proofs between several systems. The website displaying all available proofs can be reached at http://logipedia.inria.fr/
- Dedukti commit
5990bc6
git clone https://github.com/deducteam/dedukti.git git checkout 5990bc6 make install
ppx_deriving_yojson
dune
make install
The source of the project documentation can be found in docs
. The
documentation can be browsed at https://deducteam.github.io/Logipedia or it
can be built locally and then browsed using mkdocs
with
mkdocs build
mkdocs serve
then head to http://127.0.0.1:8000.
Note: version(mkdocs) >= 1.0.0. Use pip3 install -U mkdocs
to upgrade mkdocs
.
The code is also documented with dune
and mkdocs
, use make doc
to build it. It will
be available in _build/default/_doc/
, so you can run for instance firefox _build/default/_doc/_html/logipedia/index.html
.
To contribute to the API, simply fork the repository and make a pull request. To work on new translations, send an email to dedukti-dev@inria.fr.