From e2479494c0e54745e1cca53f495197ae7f024748 Mon Sep 17 00:00:00 2001
From: Gabriel <gabriel@motacilla.home>
Date: Sun, 10 Oct 2021 17:36:37 +0200
Subject: [PATCH] added documentation

---
 docs/.gitignore |   1 +
 docs/Makefile   |  10 +++++
 docs/main.adoc  | 105 ++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 116 insertions(+)
 create mode 100644 docs/.gitignore
 create mode 100644 docs/Makefile
 create mode 100644 docs/main.adoc

diff --git a/docs/.gitignore b/docs/.gitignore
new file mode 100644
index 0000000..2d19fc7
--- /dev/null
+++ b/docs/.gitignore
@@ -0,0 +1 @@
+*.html
diff --git a/docs/Makefile b/docs/Makefile
new file mode 100644
index 0000000..31c7025
--- /dev/null
+++ b/docs/Makefile
@@ -0,0 +1,10 @@
+all: main.html
+
+.SUFFIXES: .adoc .html
+
+.adoc.html:
+	asciidoc $<
+
+.PHONY: clobber
+clobber:
+	rm -f *.html
diff --git a/docs/main.adoc b/docs/main.adoc
new file mode 100644
index 0000000..87e433d
--- /dev/null
+++ b/docs/main.adoc
@@ -0,0 +1,105 @@
+// 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+.
+
-- 
GitLab