Do not copy pvs-translation-tools to PVS sources

README.md

@@ -36,6 +36,4 @@ the path (absolute or relative to `$HOME`) to the `exporter` directory.
 
 ### Usage
 
-Assuming PVS sources have been downloaded to `$PVSPATH`, copy
-`pvs-translation-tools` as `${PVSPATH}/translations`. Further instructions can
-be found in `pvs-translation-tools/README.md`.
+See `pvs-translation-tools/README.md`.

pvs-translation-tools/prelude/Makefile

@@ -2,7 +2,7 @@ PVS2DK = ../pvs2dk.sh
 LPC    = lambdapi check
 
 THEORIES != grep -v -E '^-|\#' theories
-PVSPATH  != realpath ../..
+PVSPATH   =
 
 all: dummy ${THEORIES:C/$/.lpo/}
 
@@ -16,7 +16,7 @@ translate: dummy ${THEORIES:C/$/.lp/}
 .for th in ${THEORIES}
 ${th}.lp:
 	PVSPATH=${PVSPATH} ${PVS2DK} -f ${PVSPATH}/lib/prelude.pvs -t ${.TARGET:R} \
--o ${PVSPATH}/translations/prelude/${.TARGET} > /dev/null
+-o ${PWD}/${.TARGET} > /dev/null
 	-[ -r "${.TARGET}.patch" ] && patch < "${.TARGET}.patch"
 	-[ -r "${.TARGET}.sh" ] && sh "${.TARGET}.sh"
 .endfor

pvs-translation-tools/prelude/README.md

@@ -4,9 +4,9 @@ Prelude translation
 **Warning:** the makefile uses BSD-syntax, Linux users may use `bmake` rather than
 `make`.
 
-To translate all Prelude:
+To translate all Prelude, assuming PVS sources have been downloaded to `<PVSPATH>`
 ``` sh
-make
+make PVSPATH=<PVSPATH>
 ```
 
 Theories can be translated to lambdapi files, to translate theory "functions" of