Skip to content

Unify pr/main workflows and use tlaplus/examples as integration tests #265

Unify pr/main workflows and use tlaplus/examples as integration tests

Unify pr/main workflows and use tlaplus/examples as integration tests #265

Workflow file for this run

name: Build on PR
on: [pull_request]
jobs:
test:
name: Build and Test
runs-on: ${{ matrix.operating-system }}
strategy:
fail-fast: false
matrix:
operating-system: [
macos-latest,
ubuntu-latest]
ocaml-compiler: [
'0',
'1',
'2',
]
steps:
- name: Install deps
if: matrix.operating-system == 'ubuntu-latest'
run: |
sudo apt-get update
sudo apt-get install --yes time
- name: Set up Python
uses: actions/setup-python@v4
with:
python-version: '3.11'
- name: Clone repo
uses: actions/checkout@v3
- name: Get OCaml version
run: |
INDEX=${{ matrix.ocaml-compiler }}
OCAML_VERSION=\
`python .github/workflows/ocaml_versions.py $INDEX`
echo "OCAML_VERSION=$OCAML_VERSION" \
>> $GITHUB_ENV
echo "OCAML_VERSION = $OCAML_VERSION"
- uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: ${{ env.OCAML_VERSION }}
# - uses: actions/cache@v3
# id: cache
# with:
# path: _build_cache
# key: ${{ runner.os }}_build_cache
- name: Build TLAPS installer
run: |
eval $(opam env)
opam install ./ --deps-only --yes
make
make release
- name: Get TLA+ examples
uses: actions/checkout@v3
with:
repository: tlaplus/examples
path: tlaplus-examples
- name: Check proofs in TLA+ examples
run: |
EXAMPLES_DIR=tlaplus-examples
mkdir $EXAMPLES_DIR/deps
cp ./_build/tlaps*.tar.gz $EXAMPLES_DIR/deps/tlaps.tar.gz
tar -xzf $EXAMPLES_DIR/deps/tlaps.tar.gz -C $EXAMPLES_DIR/deps
rm $EXAMPLES_DIR/deps/tlaps.tar.gz
mv $EXAMPLES_DIR/deps/tlaps* $EXAMPLES_DIR/deps/tlapm-install
python $EXAMPLES_DIR/.github/scripts/check_proofs.py \
--tlapm_path $EXAMPLES_DIR/deps/tlapm-install \
--manifest_path $EXAMPLES_DIR/manifest.json
- name: Run tests
run: |
eval $(opam env)
set +e
make test
result=$?
cat _build/default/test/tests.log
exit $result