added documentation

docs/.gitignore

+*.html

docs/Makefile

+all: main.html
+
+.SUFFIXES: .adoc .html
+
+.adoc.html:
+	asciidoc $<
+
+.PHONY: clobber
+clobber:
+	rm -f *.html

docs/main.adoc

+// vim: set syntax=asciidoc textwidth=70:
+= Translating PVS to Dedukti with Personoj =
+Gabriel Hondet <gabriel.hondet@inria.fr>
+v1.0, October 2021
+
+_Personoj_ is a suite of tools to translate specifications from
+the higher order, highly automated proof assistant
+link:http://pvs.csl.sri.com[PVS] to the universal type checker
+link:https://deducteam.github.io[Dedukti].
+
+Translating PVS to Dedukti serves mainly two purposes. The first is to
+port PVS developments to other proof assistants, so that users of say,
+link:https://coq.inria.fr[Coq], could use in their work theorems or
+specifications done in PVS. The second is to cross-check PVS
+specifications and proofs with an independent checker in order to
+increase our trust in these proofs and specifications.
+
+This work is part of a larger project led by the
+link:https://deducteam.gitlabpages.inria.fr[Deducteam] made of
+link:http://www.lsv.fr/~dowek/Publi/logipedia.pdf[Logipedia] and
+link:https://github.com/Deducteam/nubo[Nubo].
+
+== Translating theoretically ==
+
+Translating PVS into Dedukti requires to be able to express a
+sufficiently large subset of the theory of PVS into the 
+link:http://www.lsv.fr/~dowek/Publi/expressing.pdf[λΠ-calculus modulo
+theory]. Such a task is usually not easy. In the case of PVS,
+defining the logic of PVS is already tricky, but its core has been
+formally studied in
+link:https://tel.archives-ouvertes.fr/hal-01673518[F. Gilbert PhD
+thesis]. In particular, two languages has been defined. The first
+named _PVS-Core_ is the language in which PVS specifications are
+written in. It is based on Simple Type Theory with implicit predicate
+subtyping, ad-hoc polymorphism and some sort of prenex polymorphism
+and dependent types.  In particular, this language does not contain
+proof terms and type checking a term is not decidable. The second
+language named _PVS-Cert_ is a language for PVS-Core certificates. It
+replaces implicit predicate subtyping of PVS-Core with explicit
+predicate subtyping. This allows terms to contain proof terms and type
+checking terms becomes decidable.
+
+PVS-Cert has been encoded in
+link:https://github.com/Deducteam/lambdpi[lambdapi], an extension of
+Dedukti with meta-variables. This encoding is described
+link:https://arxiv.org/abs/2010.16115[there].
+The encoding of PVS-Core is work in progress. In particular, encoding
+implicit predicate subtyping requires some procedure to make it
+explicit. Personoj provides the encodings that can be used by lambdapi
+(in its development version) to explicit PVS-Core specifications and
+type check them.
+
+== How to translate and X-check PVS files? ==
+
+This section can be seen as a tutorial. It explains step by step how
+to translate theories from PVS to lambdapi files.
+
+IMPORTANT: this document is focused on the translation of the standard
+library of PVS called _Prelude_. Its management is a bit particular
+because it is somewhat linked to the lisp code of PVS. Some steps
+shouldn't be necessary when translating other libraries such as NASA's
+link:https://github.com/nasa/pvslib[pvslib].
+
+=== Requirements ===
+
+* link:https://github.com/CSL-SRI/PVS[PVS sources] version 7.1
+* link:https://github.com/gabrielhdt/lambdapi[lambdapi], branch
+  +refiner+
+* BSD flavoured +make+
+* ksh
+* patch
+
+=== Compiling PVS with a patched prelude ===
+
+NOTE: Compiling PVS is required because the prelude must be patched to
+remove some sort of _ad-hoc polymorphism_. Because PVS is linked
+against the prelude during compilation, we need to patch the prelude
+and then compile PVS with the modified prelude.
+
+CAUTION: this tutorial is made for Linux operating systems. PVS
+handles poorly BSD systems and I do not use MacOS nor Windows.
+
+NOTE: It's difficult to use some system-installed SBCL to compile PVS.
+
+[source,sh]
+git clone https://github.com/CSL-SRI/PVS
+cd PVS
+git checkout pvs7.1
+export PVSPATH=$(pwd)
+
+The last command sets the environment variable +PVSPATH+ to the root
+of the sources of PVS.
+
+The patches to be applied to the prelude are in
++tools/prelude_patches/+ and must be applied in the
+order defined by their filename. Assuming the shell is in the root
+directory of personoj,
+[source,sh]
+for p in $(find 'tools/prelude_patches/' -name '*.diff' | sort); do
+	patch "${PVSPATH}/lib/prelude.pvs" "$p"
+done
+
+PVS can then be compiled, the instructions to compile PVS can be found
+in +$PVSPATH/INSTALL+.
+