Converts a TLA+ source to a LaTeX snippet containing only the resulting tlatex environment

tlatex.sh

#!/bin/bash

# Copyright 2024 Konstantin Läufer <laufer AT cs.luc.edu>
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
#     http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

# look for GNU getopt and head

if [[ $(uname -s) =~ "Darwin" ]]; then
    GETOPT=$HOMEBREW_PREFIX/opt/gnu-getopt/bin/getopt
    HEAD=ghead
    if [[ ! -x $GETOPT ]]; then
	echo Error: no GNU-compatible getopt found
	echo Consider running
	echo '    brew install gnu-getopt'
    fi
else
    GETOPT=$(which getopt)
    HEAD=head
fi

echo Using $GETOPT
echo Using $HEAD

synopsis() {
    echo "Converts a TLA+ source to a LaTeX snippet containing only"
    echo "  the resulting tlatex environment"
    echo
    echo "Usage: tlatex [ -d|--dry-run ] [ -f|--from n1 [ [-t|--to n2 ] ] file.tla"
    exit 1
}

VALID_ARGS=$($GETOPT -o hdf:t: --long help,dry-run,from:,to: -- "$@")
if [[ $? -ne 0 ]]; then
    synopsis
fi

eval set -- "$VALID_ARGS"
while [ : ]; do
    case "$1" in
	-h | --help)
	    synopsis
	    ;;
	-d | --dry-run)
            dryrun=1
            shift
            ;;
	-f | --from)
            from=$2
            shift 2
            ;;
	-t | --to)
            to=$2
            shift 2
            ;;
	--) shift
	    break 
            ;;
    esac
done

echo $*

if [ $# != 1 ]; then
    synopsis
fi

JAVA_HOME=${JAVA_HOME:=$HOME/.sdkman/candidates/java/current}
TLA_HOME=${TLA_HOME:=$HOME/.vscode/extensions/alygin.vscode-tlaplus-nightly-*}

>&2 echo Using Java SDK in $JAVA_HOME
>&2 echo Using TLA+ tools in $TLA_HOME

input=$1
input=${input%.tla}.tla
fname=$(basename "$input")
fname=${fname%.tla}.tex

>&2 echo Writing $fname

echo "\\begin{document}" > "$fname"
echo "\\begin{tla}" >> "$fname"

if [[ -z $to ]]; then
    if [[ -z $from ]]; then
	cat "$input" >> "$fname"
    else
	tail -n +$from "$input" >> "$fname"
    fi
else
    sed -n "${from},${to}p;$((to + 1))q" < "$input" >> "$fname"
fi

echo "\\end{tla}" >> "$fname"
echo "\\end{document}" >> "$fname"

if [[ $dryrun ]]; then
    >&2 echo Dry run for determining from and to line numbers! Rerun without -d or --dry-run
    tail -n +3 "$fname" | cat -n | $HEAD -n -2
    exit
fi

>&2 echo Converting to tlatex

>&2 $JAVA_HOME/bin/java -cp $TLA_HOME/tools/tla2tools.jar tla2tex.TeX "$fname"

>&2 echo Extracting tlatex only to stdout

awk '/\\begin\{tlatex\}/,/\end\{tlatex\}/' "$fname"