From 8300208b41aae536f890dd1a8ff8ae99410900db Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 15 Jan 2026 07:54:36 -0800 Subject: [PATCH 1/2] Logically revert: "Replace Functions and FunctionTheorems with Fork variants" Fork libraries have been removed in TLAPS in https://github.com/tlaplus/tlapm/commit/c706ff1c7a1a20122ee88e085e64a645978d5d2a, which reverts https://github.com/tlaplus/tlapm/pull/239. This commit logically reverts git commit 9ece37b2e6d5cab0de16582ea81733ce5f586a84 [Dependencies] Signed-off-by: Markus Alexander Kuppe --- specifications/LoopInvariance/SumSequence.tla | 2 +- specifications/bcastByz/bcastByz.tla | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/specifications/LoopInvariance/SumSequence.tla b/specifications/LoopInvariance/SumSequence.tla index 13ff984e..c4aed791 100644 --- a/specifications/LoopInvariance/SumSequence.tla +++ b/specifications/LoopInvariance/SumSequence.tla @@ -9,7 +9,7 @@ (* *) (* http://lamport.azurewebsites.net/tla/proving-safety.pdf *) (***************************************************************************) -EXTENDS Integers, SequenceTheorems, SequencesExtForkTheorems, NaturalsInduction, TLAPS +EXTENDS Integers, SequenceTheorems, SequencesExtTheorems, NaturalsInduction, TLAPS (***************************************************************************) (* To facilitate model checking, we assume that the sequence to be summed *) diff --git a/specifications/bcastByz/bcastByz.tla b/specifications/bcastByz/bcastByz.tla index b8cec64e..43ce7814 100644 --- a/specifications/bcastByz/bcastByz.tla +++ b/specifications/bcastByz/bcastByz.tla @@ -34,8 +34,8 @@ EXTENDS Naturals, FiniteSets, - FunctionsFork, - FunctionForkTheorems, + Functions, + FunctionTheorems, FiniteSetTheorems, NaturalsInduction, SequenceTheorems, From 7d3264f3ce40a568abe17b49705a0032f9bc5f34 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 15 Jan 2026 09:10:27 -0800 Subject: [PATCH 2/2] Add community modules path argument to proof checking script Updated the check_proofs.py script to include a new optional argument for specifying the path to extracted community modules. This allows for better integration of community modules during proof validation. Additionally, modified the CI workflow to create and unzip the community modules directory before running the proof checks. Co-authored-by: Claude Sonnet 4.5 Signed-off-by: Markus Alexander Kuppe --- .github/scripts/check_proofs.py | 15 ++++++++++----- .github/workflows/CI.yml | 8 ++++++-- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/.github/scripts/check_proofs.py b/.github/scripts/check_proofs.py index 5132ee8c..0e9e9601 100644 --- a/.github/scripts/check_proofs.py +++ b/.github/scripts/check_proofs.py @@ -12,6 +12,7 @@ parser = ArgumentParser(description='Validate all proofs in all modules with TLAPM.') parser.add_argument('--tlapm_path', help='Path to TLAPM install dir; should have bin and lib subdirs', required=False, default = 'deps/tlapm') +parser.add_argument('--community_modules_path', help='Path to extracted community modules directory', required=False, default='') parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=False, default='.') parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip checking', required=False, default=[]) parser.add_argument('--only', nargs='+', help='If provided, only check proofs in this space-separated list', required=False, default=[]) @@ -19,6 +20,7 @@ args = parser.parse_args() tlapm_path = normpath(args.tlapm_path) +community_modules_path = normpath(args.community_modules_path) if args.community_modules_path else '' examples_root = args.examples_root manifest = tla_utils.load_all_manifests(examples_root) skip_modules = args.skip @@ -50,12 +52,15 @@ full_module_path = tla_utils.from_cwd(examples_root, module_path) module_dir = dirname(full_module_path) try: + tlapm_args = [ + tlapm_path, full_module_path, + '-I', module_dir, + '--stretch', '5' + ] + if community_modules_path: + tlapm_args.extend(['-I', community_modules_path]) tlapm_result = subprocess.run( - [ - tlapm_path, full_module_path, - '-I', module_dir, - '--stretch', '5' - ], + tlapm_args, stdout = subprocess.PIPE, stderr = subprocess.STDOUT, text = True diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 0efddefb..6999b008 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -135,8 +135,12 @@ jobs: - name: Check proofs if: matrix.os != 'windows-latest' && !matrix.unicode run: | - python $SCRIPT_DIR/check_proofs.py \ - --tlapm_path $DEPS_DIR/tlapm \ + # Extract community modules for TLAPM + mkdir -p $DEPS_DIR/community/modules + unzip -q -o $DEPS_DIR/community/modules.jar -d $DEPS_DIR/community/modules + python $SCRIPT_DIR/check_proofs.py \ + --tlapm_path $DEPS_DIR/tlapm \ + --community_modules_path $DEPS_DIR/community/modules \ --examples_root . - name: Smoke-test manifest generation script run: |