Logically revert: "Replace Functions and FunctionTheorems with Fork variants

.github/scripts/check_proofs.py

@@ -12,13 +12,15 @@
 
 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=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
 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

.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: |

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  *)

specifications/bcastByz/bcastByz.tla

@@ -34,8 +34,8 @@
 
 EXTENDS Naturals, 
         FiniteSets,
-        FunctionsFork,
-        FunctionForkTheorems, 
+        Functions,
+        FunctionTheorems, 
         FiniteSetTheorems,
         NaturalsInduction,
         SequenceTheorems,