Added Python venv instructions

Signed-off-by: Andrew Helwer <[email protected]>

Author: ahelwer

.github/workflows/CI.yml

@@ -41,7 +41,10 @@ jobs:
         if: matrix.os == 'windows-latest'
       - name: Install python packages
         shell: bash
-        run: pip install -r $SCRIPT_DIR/requirements.txt
+        run: |
+          python -m venv .
+          source ./bin/activate
+          pip install -r $SCRIPT_DIR/requirements.txt
       - name: Download TLA⁺ dependencies
         run: |
           # Fix tar symbolic link issues on Windows; see:
@@ -67,25 +70,38 @@ jobs:
           mv tlapm-$TLAPS_VERSION tlapm
       - name: Check manifest.json format
         shell: bash
-        run: python $SCRIPT_DIR/check_manifest_schema.py
+        run: |
+          source ./bin/activate
+          python $SCRIPT_DIR/check_manifest_schema.py
       - name: Check manifest files
         shell: bash
-        run: python $SCRIPT_DIR/check_manifest_files.py
+        run: |
+          source ./bin/activate
+          python $SCRIPT_DIR/check_manifest_files.py
       - name: Check manifest feature flags
         shell: bash
-        run: python $SCRIPT_DIR/check_manifest_features.py
+        run: |
+          source ./bin/activate
+          python $SCRIPT_DIR/check_manifest_features.py
       - name: Parse all modules
         shell: bash
-        run: python $SCRIPT_DIR/parse_modules.py
+        run: |
+          source ./bin/activate
+          python $SCRIPT_DIR/parse_modules.py
       - name: Check small models
         shell: bash
-        run: python $SCRIPT_DIR/check_small_models.py
+        run: |
+          source ./bin/activate
+          python $SCRIPT_DIR/check_small_models.py
       - name: Smoke-test large models
         shell: bash
-        run: python $SCRIPT_DIR/smoke_test_large_models.py
+        run: |
+          source ./bin/activate
+          python $SCRIPT_DIR/smoke_test_large_models.py
       - name: Smoke-test manifest generation script
         shell: bash
         run: |
+          source ./bin/activate
           rm -r build
           python $SCRIPT_DIR/generate_manifest.py
           git diff -a

README.md

@@ -117,7 +117,7 @@ A central manifest of specs with descriptions and accounts of their various mode
 | 100 | Simplified Fast Paxos | <a href="https://github.com/tlaplus/Examples/tree/master/specifications/SimplifiedFastPaxos">Simplified version of Fast Paxos (Lamport, 2006)</a> | Lim Ngian Xin Terry, Gaurav Gandhi | |&#10004;| TLC, Naturals, FiniteSets, Integers | | |
 | 101 | Learn TLA⁺ Proofs | <a href="specifications/LearnProofs">Basic PlusCal algorithms and formal proofs of their correctness</a> | Andrew Helwer | &#10004; | &#10004; | Sequences, Naturals, Integers, TLAPS | &#10004; | |
 | 102 | Lexicographically-Least Circular Substring | <a href="specifications/LeastCircularSubstring">Booth's 1980 algorithm to find the lexicographically-least circular substring</a> | Andrew Helwer | | &#10004; | FiniteSets, Integers, Naturals, Sequences | &#10004; | |
-| 103 | Distributed Checkpoint Coordination | <a href="specifications/LeastCircularSubstring">Algorithm for coordinating checkpoint/snapshot leases in a Paxos ring</a> | Andrew Helwer | | &#10004; | FiniteSets, Naturals, Sequences, TLC | | |
+| 103 | Distributed Checkpoint Coordination | <a href="specifications/CheckpointCoordination">Algorithm for coordinating checkpoint/snapshot leases in a Paxos ring</a> | Andrew Helwer | | &#10004; | FiniteSets, Naturals, Sequences, TLC | | |
 
 ## License
 
@@ -146,10 +146,11 @@ To do this, you'll have to update the [`manifest.json`](manifest.json) file with
 If this process doesn't work for you, you can alternatively modify the [`.ciignore`](.ciignore) file to exclude your spec from validation.
 Otherwise, follow these directions:
 
-1. Ensure you have Python 3.X installed
+1. Ensure you have Python 3.11+ installed
 1. Download & extract tree-sitter-tlaplus ([zip](https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/refs/heads/main.zip), [tar.gz](https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/refs/heads/main.tar.gz)) to the root of the repository; ensure the extracted folder is named `tree-sitter-tlaplus`
 1. Open a shell and navigate to the repo root; ensure a C++ compiler is installed and on your path
     - On Windows, this might entail running the below script from the visual studio developer command prompt
+1. It is considered best practice to create & initialize a Python virtual environment to preserve your system package store; run `python -m venv .` then `source ./bin/activate` on Linux & macOS or `.\Scripts\activate.bat` on Windows (run `deactivate` to exit)
 1. Run `pip install -r .github/scripts/requirements.txt`
 1. Run `python .github/scripts/generate_manifest.py`
 1. Locate your spec's entry in the [`manifest.json`](manifest.json) file and ensure the following fields are filled out:

manifest.json

@@ -1335,8 +1335,8 @@
       "description": "Spec of simplified Fast Paxos from Lamport's 2006 paper Fast Paxos",
       "source": "",
       "authors": [
-        "Lim Ngian Xin Terry",
-        "Gaurav Gandhi"
+        "Gaurav Gandhi",
+        "Lim Ngian Xin Terry"
       ],
       "tags": [],
       "modules": [
@@ -3654,4 +3654,4 @@
       ]
     }
   ]
-}
+}