Skip to content

Add unicode support to SANY #167

Add unicode support to SANY

Add unicode support to SANY #167

Workflow file for this run

name: PullRequest builder TLA+
on: [pull_request]
jobs:
build:
runs-on: ubuntu-latest
env:
SCRIPT_DIR: examples/.github/scripts
DEPS_DIR: examples/deps
TLAPS_VERSION: 202210041448
MVN_COMMAND: xvfb-run mvn -Dtest.skip=true -Dmaven.test.failure.ignore=true
steps:
- uses: actions/checkout@v2
with:
# Number of commits to fetch. 0 indicates all history.
# jgit task nested in customBuild.xml fails without history.
fetch-depth: '0'
- name: Set up JDK 11
uses: actions/setup-java@v1
with:
java-version: 11.0.3
##
## Run TLC tests.
##
- name: Run TLC tests
run: ant -f tlatools/org.lamport.tlatools/customBuild.xml -Dtest.halt=true compile compile-test test dist
##
## Build TLC and Toolbox (logger reduces verbosity).
##
- name: Build with Maven (Linux)
run: $MVN_COMMAND -Dtycho.disableP2Mirrors=true -Dorg.slf4j.simpleLogger.log.org.apache.maven.cli.transfer.Slf4jMavenTransferListener=warn -fae -B verify --file pom.xml
##
## Trigger build of CommunityModule as integration tests.
##
- uses: actions/checkout@v2
with:
repository: tlaplus/CommunityModules
path: communitymodules/
# Number of commits to fetch. 0 indicates all history.
# jgit task nested in customBuild.xml fails without history.
fetch-depth: '0'
- name: Build CommunityModules
run: |
mkdir -p communitymodules/tlc
cp tlatools/org.lamport.tlatools/dist/tla2tools.jar communitymodules/tlc/
ant -f communitymodules/build.xml -Dskip.download=true
##
## Trigger run of examples as integration tests.
##
- uses: actions/checkout@v2
with:
repository: tlaplus/examples
path: examples/
# Number of commits to fetch. 0 indicates all history.
# jgit task nested in customBuild.xml fails without history.
fetch-depth: '0'
- name: Download tlaplus/examples test dependencies
run: $SCRIPT_DIR/linux-setup.sh $SCRIPT_DIR $DEPS_DIR false
- name: Parse tlaplus/examples modules
run: |
python examples/.github/scripts/parse_modules.py \
--tools_jar_path tlatools/org.lamport.tlatools/dist/tla2tools.jar \
--tlapm_lib_path tlapm/library \
--community_modules_jar_path CommunityModules-deps.jar \
--manifest_path examples/manifest.json
- name: Model-check small tlaplus/examples models
run: |
python examples/.github/scripts/check_small_models.py \
--tools_jar_path tlatools/org.lamport.tlatools/dist/tla2tools.jar \
--tlapm_lib_path tlapm/library \
--community_modules_jar_path CommunityModules-deps.jar \
--manifest_path examples/manifest.json
- name: Smoke-test large tlaplus/examples models
run: |
# SimKnuthYao requires certain number of states to have been generated
# before termination or else it fails. This makes it not amenable to
# smoke testing.
python examples/.github/scripts/smoke_test_large_models.py \
--tools_jar_path tlatools/org.lamport.tlatools/dist/tla2tools.jar \
--tlapm_lib_path tlapm/library \
--community_modules_jar_path CommunityModules-deps.jar \
--manifest_path examples/manifest.json \
--skip specifications/KnuthYao/SimKnuthYao.cfg
- name: Convert specs to unicode
run: |
python $SCRIPT_DIR/unicode_conversion.py \
--tlauc_path deps/tlauc/tlauc \
--manifest_path manifest.json
- name: Unicode shims
run: |
python $SCRIPT_DIR/unicode_number_set_shim.py \
--ts_path deps/tree-sitter-tlaplus \
--manifest_path manifest.json
- name: Parse all modules (Unicode)
run: |
# These redefine Nat, Int, or Real so cannot be shimmed
SKIP=(
"specifications/SpecifyingSystems/Standard/Naturals.tla"
"specifications/SpecifyingSystems/Standard/Peano.tla"
"specifications/SpecifyingSystems/Standard/Integers.tla"
"specifications/SpecifyingSystems/Standard/Reals.tla"
"specifications/SpecifyingSystems/Standard/ProtoReals.tla"
"specifications/SpecifyingSystems/RealTime/MCRealTime.tla"
"specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.tla"
)
python $SCRIPT_DIR/parse_modules.py \
--tools_jar_path tlatools/org.lamport.tlatools/dist/tla2tools.jar \
--tlapm_lib_path $DEPS_DIR/tlapm/library \
--community_modules_jar_path $DEPS_DIR/community/modules.jar \
--manifest_path manifest.json \
--skip "${SKIP[@]}"
- name: Check small models (Unicode)
run: |
# These redefine Real so cannot be shimmed
SKIP+=(
"specifications/SpecifyingSystems/RealTime/MCRealTime.tla"
"specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.tla"
)
python $SCRIPT_DIR/check_small_models.py \
--tools_jar_path tlatools/org.lamport.tlatools/dist/tla2tools.jar \
--tlapm_lib_path $DEPS_DIR/tlapm/library \
--community_modules_jar_path $DEPS_DIR/community/modules.jar \
--manifest_path manifest.json \
--skip "${SKIP[@]}"
- name: Smoke-test large models (Unicode)
run: |
python $SCRIPT_DIR/smoke_test_large_models.py \
--tools_jar_path tlatools/org.lamport.tlatools/dist/tla2tools.jar \
--tlapm_lib_path $DEPS_DIR/tlapm/library \
--community_modules_jar_path $DEPS_DIR/community/modules.jar \
--manifest_path manifest.json \
--skip specifications/KnuthYao/SimKnuthYao.cfg