From 3668ca46f41747613c1b565feb3507d2869d4fff Mon Sep 17 00:00:00 2001
From: Gabriel <gabriel@motacilla.home>
Date: Sat, 9 Oct 2021 14:58:50 +0200
Subject: [PATCH] Do not copy pvs-translation-tools to PVS sources
---
README.md | 4 +---
pvs-translation-tools/prelude/Makefile | 4 ++--
pvs-translation-tools/prelude/README.md | 4 ++--
3 files changed, 5 insertions(+), 7 deletions(-)
diff --git a/README.md b/README.md
index a2c5506..ef8be0f 100644
--- a/README.md
+++ b/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`.
diff --git a/pvs-translation-tools/prelude/Makefile b/pvs-translation-tools/prelude/Makefile
index 5f44f00..bedd021 100644
--- a/pvs-translation-tools/prelude/Makefile
+++ b/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
diff --git a/pvs-translation-tools/prelude/README.md b/pvs-translation-tools/prelude/README.md
index 7ca5fbb..34da6d7 100644
--- a/pvs-translation-tools/prelude/README.md
+++ b/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
--
GitLab