posix shell, no ksh needed

.github/workflows/check_encoding.yml

@@ -44,7 +44,7 @@ jobs:
     # Runs a set of commands using the runners shell
     - name: install lambdapi and deps
       run: |
-        sudo apt install --yes bmake ksh perl
+        sudo apt install --yes bmake perl
         (cd "${GITHUB_WORKSPACE}/lambdapi/" || exit 1
          opam install .)
         eval $(opam env)

specs/tools/pvs2dk.sh

-#!/bin/ksh
+#!/bin/sh
 
 # usage: pvs2dk.sh [options]
 #   -f p, --file p              translate theory from file p
 #   -t h, --theory h            translate theory t
 #   -o p, --output p            write translation to file p
-#   -v n, --verbose n           set verbosity level
 
-set -eufo pipefail
+set -euf
 
 theory=""
 file=""
 output=""
-verbose=3
 
-USAGE="[-author?Gabriel Hondet <gabriel.hondet@inria.fr>]"
-USAGE+="[+NAME?pvs2dk.sh --- Translate a PVS specification to Dedukti]"
-USAGE+="[+DESCRIPTION?Parse and proofcheck a theory in PVS to translate it
+HELP () {
+	printf 'NAME: %s --- Translate a PVS specification to Dedukti
+
+SYNOPSIS:
+
+%s -f FILE -t THEORY -o OUTPUT
+
+ Options:
+   -f File containing the theory
+   -t Name of the theory to translate
+   -o Target file of the translation
+
+DESCRIPTION:
+
+Parse and proofcheck a theory in PVS to translate it
 to Dedukti, an implementation of λΠ/R.
 
 PVS filepaths are ALWAYS relative to the root of PVS. This restriction
@@ -25,22 +35,21 @@ Theories are translated one at a time using the -f and -t options,
 such as in pvs2dk --file=lib/prelude.pvs --theory=booleans.
 
 Translated files can be type checked by Lambdapi (taken from the PATH). Files to
-be typechecked may be edited.]"
-USAGE+="[f:file?File containing the theory.]:[path]"
-USAGE+="[t:theory?Name of the theory to translate.]:[theory]"
-USAGE+="[o:output?Target file of the translation.]:[path]"
-USAGE+="[v:verbose]#[verbose:=3?Verbosity level.]"
-USAGE+=$'\n\n\n\n'
-while getopts "${USAGE}" o; do
+be typechecked may be edited.\n' "$0" "$0"
+	exit 1
+}
+
+while getopts 'f:t:o:h' o; do
     case "$o" in
         f) file="$(realpath "${OPTARG}")" ;;
         t) theory="${OPTARG}" ;;
         o) output="${OPTARG}" ;;
-        v) verbose="${OPTARG}"
+				h) HELP ;;
+				?) HELP ;;
     esac
 done
-output="$(realpath $(dirname ${output}))/$(basename ${output})"
+output="$(realpath "$(dirname "${output}")")/$(basename "${output}")"
 
 pvscmd="(prettyprint-dedukti \"${file}#${theory}\" \"${output}\")"
-(cd ${PVSPATH:?'PVSPATH not set'} || exit 1
+(cd "${PVSPATH:?'PVSPATH not set'}" || exit 1
  ./pvs -raw -E "${pvscmd}" --quit)