Skip to content

Commit

Permalink
Various updates to CI scripts (#118)
Browse files Browse the repository at this point in the history
- Break out dependency download logic into separate scripts
- Switch to using latest tlapm release in anticipation of rolling releases
- Switch to using M1 macOS github CI runners

Signed-off-by: Andrew Helwer <[email protected]>
  • Loading branch information
ahelwer authored Feb 8, 2024
1 parent 789a653 commit 46bd732
Show file tree
Hide file tree
Showing 8 changed files with 654 additions and 124 deletions.
81 changes: 81 additions & 0 deletions .github/scripts/linux-setup.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,81 @@
# This script downloads all necessary dependencies to run the CI on Linux.
# It can also be run locally, as long as you have the following dependencies:
# - python 3.1x
# - java
# - C & C++ compiler (aliased to cc and cpp commands respectively)
# - wget
# - tar
#
# The script takes the following positional command line parameters:
# 1. Path to this script directory from the current working directory
# 2. Path to the desired dependencies directory
# 3. Boolean true/false; whether to initialize a python virtual env

main() {
# Validate command line parameters
if [ $# -ne 3 ]; then
echo "Usage: $0 <script dir path> <desired dependency dir path> <bool: use python venv>"
exit 1
fi
SCRIPT_DIR="$1"
DEPS_DIR="$2"
USE_VENV=$3
# Print out tool version information
java --version
python --version
pip --version
cc --version
cpp --version
# Install python packages
if $USE_VENV; then
python -m venv .
source bin/activate
pip install -r "$SCRIPT_DIR/requirements.txt"
deactivate
else
pip install -r "$SCRIPT_DIR/requirements.txt"
fi
# Put all dependencies in their own directory to ensure they aren't included implicitly
mkdir -p "$DEPS_DIR"
# Get tree-sitter-tlaplus
wget -nv https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.tar.gz -O /tmp/tree-sitter-tlaplus.tar.gz
tar -xzf /tmp/tree-sitter-tlaplus.tar.gz --directory "$DEPS_DIR"
mv "$DEPS_DIR/tree-sitter-tlaplus-main" "$DEPS_DIR/tree-sitter-tlaplus"
# Get TLA⁺ tools
mkdir -p "$DEPS_DIR/tools"
wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -P "$DEPS_DIR/tools"
# Get TLA⁺ community modules
mkdir -p "$DEPS_DIR/community"
wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
-O "$DEPS_DIR/community/modules.jar"
# Get TLAPS modules
wget -nv https://github.com/tlaplus/tlapm/archive/main.tar.gz -O /tmp/tlapm.tar.gz
tar -xzf /tmp/tlapm.tar.gz --directory "$DEPS_DIR"
mv "$DEPS_DIR/tlapm-main" "$DEPS_DIR/tlapm"
# Install TLAPS
kernel=$(uname -s)
if [ "$kernel" == "Linux" ]; then
TLAPM_BIN_TYPE=x86_64-linux-gnu
elif [ "$kernel" == "Darwin" ]; then
TLAPM_BIN_TYPE=i386-darwin
else
echo "Unknown OS: $kernel"
exit 1
fi
TLAPM_BIN="tlaps-1.5.0-$TLAPM_BIN_TYPE-inst.bin"
wget -nv "https://github.com/tlaplus/tlapm/releases/latest/download/$TLAPM_BIN" -O /tmp/tlapm-installer.bin
chmod +x /tmp/tlapm-installer.bin
# Workaround for https://github.com/tlaplus/tlapm/issues/88
set +e
for ((attempt = 1; attempt <= 5; attempt++)); do
rm -rf "$DEPS_DIR/tlapm-install"
/tmp/tlapm-installer.bin -d "$DEPS_DIR/tlapm-install"
if [ $? -eq 0 ]; then
exit 0
fi
done
exit 1
}

main "$@"

19 changes: 13 additions & 6 deletions .github/scripts/parse_modules.py
Original file line number Diff line number Diff line change
Expand Up @@ -16,35 +16,41 @@
parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True)
parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip parsing', required=False, default=[])
parser.add_argument('--only', nargs='+', help='If provided, only parse models in this space-separated list', required=False, default=[])
parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
args = parser.parse_args()

logging.basicConfig(level=logging.INFO)
logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)

tools_jar_path = normpath(args.tools_jar_path)
tlaps_modules = normpath(args.tlapm_lib_path)
community_modules = normpath(args.community_modules_jar_path)
manifest_path = normpath(args.manifest_path)
examples_root = dirname(manifest_path)
skip_modules = [normpath(path) for path in args.skip]
only_modules = [normpath(path) for path in args.only]

def parse_module(path):
"""
Parse the given module using SANY.
"""
logging.info(path)
# Jar paths must go first
search_paths = pathsep.join([tools_jar_path, community_modules, dirname(path), tlaps_modules])
search_paths = pathsep.join([tools_jar_path, dirname(path), community_modules, tlaps_modules])
sany = subprocess.run([
'java',
'-cp', search_paths,
'tla2sany.SANY',
'-error-codes',
path
], capture_output=True)
if sany.returncode != 0:
logging.error(sany.stdout.decode('utf-8'))
output = ' '.join(sany.args) + '\n' + sany.stdout.decode('utf-8')
if 0 == sany.returncode:
logging.debug(output)
return True
else:
logging.error(output)
return False
return True

manifest = tla_utils.load_json(manifest_path)

Expand All @@ -54,13 +60,14 @@ def parse_module(path):
for spec in manifest['specifications']
for module in spec['modules']
if normpath(module['path']) not in skip_modules
and (only_modules == [] or normpath(module['path']) in only_modules)
]

for path in skip_modules:
logging.info(f'Skipping {path}')

# Parse specs in parallel
thread_count = cpu_count()
thread_count = cpu_count() if not args.verbose else 1
logging.info(f'Parsing using {thread_count} threads')
with ThreadPoolExecutor(thread_count) as executor:
results = executor.map(parse_module, modules)
Expand Down
56 changes: 56 additions & 0 deletions .github/scripts/windows-setup.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
# This script downloads all necessary dependencies to run the CI on Windows.
# It can also be run locally, as long as you have the following dependencies:
# - python 3.1x
# - java
# - curl
# - 7-zip
#
# The script takes the following positional command line parameters:
# 1. Path to this script directory from the current working directory
# 2. Path to the desired dependencies directory
# 3. Boolean true/false; whether to initialize a python virtual env

main() {
# Validate command line parameters
if [ $# -ne 3 ]; then
echo "Usage: $0 <script dir path> <desired dependency dir path> <bool: use python venv>"
exit 1
fi
SCRIPT_DIR="$1"
DEPS_DIR="$2"
USE_VENV=$3
# Print out tool version information
java --version
python --version
pip --version
# Install python packages
if $USE_VENV; then
python -m venv .
pwsh Scripts/Activate.ps1
pip install -r "$SCRIPT_DIR/requirements.txt"
deactivate
else
pip install -r "$SCRIPT_DIR/requirements.txt"
fi
# Put all dependencies in their own directory to ensure they aren't included implicitly
mkdir -p "$DEPS_DIR"
# Get tree-sitter-tlaplus
curl -L https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.zip --output tree-sitter-tlaplus.zip
7z x tree-sitter-tlaplus.zip
mv tree-sitter-tlaplus-main "$DEPS_DIR/tree-sitter-tlaplus"
rm tree-sitter-tlaplus.zip
# Get TLA⁺ tools
mkdir -p "$DEPS_DIR/tools"
curl http://nightly.tlapl.us/dist/tla2tools.jar --output "$DEPS_DIR/tools/tla2tools.jar"
# Get TLA⁺ community modules
mkdir -p "$DEPS_DIR/community"
curl -L https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar --output "$DEPS_DIR/community/modules.jar"
# Get TLAPS modules
curl -L https://github.com/tlaplus/tlapm/archive/main.zip --output tlapm.zip
7z x tlapm.zip
mv tlapm-main "$DEPS_DIR/tlapm"
rm tlapm.zip
}

main "$@"

127 changes: 26 additions & 101 deletions .github/workflows/CI.yml
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,11 @@ jobs:
include:
- { os: windows-latest }
- { os: ubuntu-latest }
- { os: macos-latest }
- { os: macos-14 }
fail-fast: false
env:
SCRIPT_DIR: .github/scripts
TLAPS_VERSION: 202210041448
DEPS_DIR: deps
defaults:
run:
shell: bash
Expand All @@ -32,93 +32,18 @@ jobs:
- name: Install python
uses: actions/setup-python@v5
with:
python-version: '3.11'
python-version: '3.12'
- name: Install Java
uses: actions/setup-java@v4
with:
distribution: adopt
java-version: 17
- name: Download TLA⁺ dependencies
- name: Download TLA⁺ dependencies (Windows)
if: matrix.os == 'windows-latest'
run: |
# Print out tool version information
java --version
python --version
pip --version
# Install python packages
pip install -r $SCRIPT_DIR/requirements.txt
# Put all dependencies in their own directory to ensure they aren't included implicitly
mkdir deps
# Get tree-sitter-tlaplus
curl -LO https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.zip
7z x main.zip
rm main.zip
mv tree-sitter-tlaplus-main deps/tree-sitter-tlaplus
# Get TLA⁺ tools
mkdir deps/tools
curl -LO http://nightly.tlapl.us/dist/tla2tools.jar
mv tla2tools.jar deps/tools/tla2tools.jar
# Get TLA⁺ community modules
mkdir deps/community
curl -LO https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
mv CommunityModules-deps.jar deps/community/modules.jar
# Get TLAPS modules
curl -LO https://github.com/tlaplus/tlapm/archive/refs/tags/$TLAPS_VERSION.zip
7z x $TLAPS_VERSION.zip
rm $TLAPS_VERSION.zip
mv tlapm-$TLAPS_VERSION deps/tlapm
- name: Download TLA⁺ dependencies
run: $SCRIPT_DIR/windows-setup.sh $SCRIPT_DIR $DEPS_DIR false
- name: Download TLA⁺ dependencies (Linux & macOS)
if: matrix.os != 'windows-latest'
run: |
# Print out tool version information
java --version
python --version
pip --version
cc --version
cpp --version
# Install python packages
pip install -r $SCRIPT_DIR/requirements.txt
# Put all dependencies in their own directory to ensure they aren't included implicitly
mkdir deps
# Get tree-sitter-tlaplus
wget -nv https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.tar.gz
tar -xf main.tar.gz
rm main.tar.gz
mv tree-sitter-tlaplus-main deps/tree-sitter-tlaplus
# Get TLA⁺ tools
mkdir deps/tools
wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -O deps/tools/tla2tools.jar
# Get TLA⁺ community modules
mkdir deps/community
wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
-O deps/community/modules.jar
# Get TLAPS modules
wget -nv https://github.com/tlaplus/tlapm/archive/refs/tags/$TLAPS_VERSION.tar.gz
tar -xf $TLAPS_VERSION.tar.gz
rm $TLAPS_VERSION.tar.gz
mv tlapm-$TLAPS_VERSION deps/tlapm
# Install TLAPS
if [[ "${{ runner.os }}" == "Linux" ]]; then
TLAPM_BIN_TYPE=x86_64-linux-gnu
elif [[ "${{ runner.os }}" == "macOS" ]]; then
TLAPM_BIN_TYPE=i386-darwin
else
echo "Unknown OS"
exit 1
fi
TLAPM_BIN="tlaps-1.5.0-$TLAPM_BIN_TYPE-inst.bin"
wget -nv https://github.com/tlaplus/tlapm/releases/download/$TLAPS_VERSION/$TLAPM_BIN
chmod +x $TLAPM_BIN
# Workaround for https://github.com/tlaplus/tlapm/issues/88
set +e
for ((attempt = 1; attempt <= 5; attempt++)); do
rm -rf deps/tlapm-install
./$TLAPM_BIN -d deps/tlapm-install
if [ $? -eq 0 ]; then
exit 0
fi
done
exit 1
run: $SCRIPT_DIR/linux-setup.sh $SCRIPT_DIR $DEPS_DIR false
- name: Check manifest.json format
run: |
python $SCRIPT_DIR/check_manifest_schema.py \
Expand All @@ -133,25 +58,25 @@ jobs:
run: |
python $SCRIPT_DIR/check_manifest_features.py \
--manifest_path manifest.json \
--ts_path deps/tree-sitter-tlaplus
--ts_path $DEPS_DIR/tree-sitter-tlaplus
- name: Check README spec table
run: |
python $SCRIPT_DIR/check_markdown_table.py \
--manifest_path manifest.json \
--readme_path README.md
- name: Parse all modules
run: |
python $SCRIPT_DIR/parse_modules.py \
--tools_jar_path deps/tools/tla2tools.jar \
--tlapm_lib_path deps/tlapm/library \
--community_modules_jar_path deps/community/modules.jar \
python $SCRIPT_DIR/parse_modules.py \
--tools_jar_path $DEPS_DIR/tools/tla2tools.jar \
--tlapm_lib_path $DEPS_DIR/tlapm/library \
--community_modules_jar_path $DEPS_DIR/community/modules.jar \
--manifest_path manifest.json
- name: Check small models
run: |
python $SCRIPT_DIR/check_small_models.py \
--tools_jar_path deps/tools/tla2tools.jar \
--tlapm_lib_path deps/tlapm/library \
--community_modules_jar_path deps/community/modules.jar \
python $SCRIPT_DIR/check_small_models.py \
--tools_jar_path $DEPS_DIR/tools/tla2tools.jar \
--tlapm_lib_path $DEPS_DIR/tlapm/library \
--community_modules_jar_path $DEPS_DIR/community/modules.jar \
--manifest_path manifest.json
- name: Smoke-test large models
run: |
Expand All @@ -163,11 +88,11 @@ jobs:
if [[ "${{ runner.os }}" == "Windows" ]]; then
SKIP+=("specifications/ewd426/SimTokenRing.cfg")
fi
python $SCRIPT_DIR/smoke_test_large_models.py \
--tools_jar_path deps/tools/tla2tools.jar \
--tlapm_lib_path deps/tlapm/library \
--community_modules_jar_path deps/community/modules.jar \
--manifest_path manifest.json \
python $SCRIPT_DIR/smoke_test_large_models.py \
--tools_jar_path $DEPS_DIR/tools/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 proofs
if: matrix.os != 'windows-latest'
Expand All @@ -188,16 +113,16 @@ jobs:
specifications/MisraReachability/ReachabilityProofs.tla
specifications/byzpaxos/BPConProof.tla # Takes about 30 minutes
)
python $SCRIPT_DIR/check_proofs.py \
--tlapm_path deps/tlapm-install \
--manifest_path manifest.json \
python $SCRIPT_DIR/check_proofs.py \
--tlapm_path $DEPS_DIR/tlapm-install \
--manifest_path manifest.json \
--skip "${SKIP[@]}"
- name: Smoke-test manifest generation script
run: |
rm -r deps/tree-sitter-tlaplus/build
rm -r $DEPS_DIR/tree-sitter-tlaplus/build
python $SCRIPT_DIR/generate_manifest.py \
--manifest_path manifest.json \
--ci_ignore_path .ciignore \
--ts_path deps/tree-sitter-tlaplus
--ts_path $DEPS_DIR/tree-sitter-tlaplus
git diff -a
1 change: 0 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ All specs in this repository are subject to CI validation to ensure quality.

## Examples Included Here
Here is a list of specs included in this repository, with links to the relevant directory and flags for various features:
<<<<<<< HEAD
| Name | Author(s) | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |
| --------------------------------------------------------------------------------------------------- | --------------------------------------------------- | :------: | :---------: | :-----: | :-------: | :------: |
| [Teaching Concurrency](specifications/TeachingConcurrency) | Leslie Lamport ||||| |
Expand Down
Loading

0 comments on commit 46bd732

Please sign in to comment.