From 8ace4aa604351def479a8b75d0bf45d3d679b001 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 28 Mar 2024 02:31:26 -0700 Subject: [PATCH] Reduce noise of TLAi linter. (#6103) --- .github/workflows/tlaplus.yml | 4 ++-- scripts/TLAi-linter.genai.js | 4 ++++ tla/StatsFile.tla | 2 +- tla/actions.py | 2 +- tla/consensus/MCccfraftAtomicReconfig.cfg | 2 +- tla/consensus/MCccfraftWithReconfig.cfg | 2 +- 6 files changed, 10 insertions(+), 6 deletions(-) diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml index 41d201c4e..a507cbc56 100644 --- a/.github/workflows/tlaplus.yml +++ b/.github/workflows/tlaplus.yml @@ -144,7 +144,7 @@ jobs: ## Identify git diff: $(git diff --name-only HEAD^ | grep '.tla') ## Install genaiscript runtime: https://microsoft.github.io/genaiscript/reference/cli/ ## Output LLM response in SARIF format: https://microsoft.github.io/genaiscript/reference/scripts/annotations/ (redirect other output to /dev/null for GH not to also show the annotations) - run: npx --yes genaiscript run scripts/TLAi-linter.genai.js $(git diff --name-only HEAD^ | grep '\.tla') --max-tokens 2000 --out-annotations results.sarif > /dev/null + run: npx --yes genaiscript run scripts/TLAi-linter.genai.js $(git diff --name-only HEAD^ | grep '\.tla') --max-tokens 2000 --out-annotations results.sarif > /dev/null && jq '.runs |= map(.results |= map(select(.level != "note")))' results.sarif > filtered.sarif - name: Upload SARIF file if: (success() || failure()) && steps.git_commit.outputs.contains_tla == 'true' @@ -152,4 +152,4 @@ jobs: ## https://docs.github.com/en/code-security/code-scanning/integrating-with-code-scanning/uploading-a-sarif-file-to-github uses: github/codeql-action/upload-sarif@v3 with: - sarif_file: results.sarif + sarif_file: filtered.sarif diff --git a/scripts/TLAi-linter.genai.js b/scripts/TLAi-linter.genai.js index 466371f78..ea5c6d374 100644 --- a/scripts/TLAi-linter.genai.js +++ b/scripts/TLAi-linter.genai.js @@ -14,6 +14,7 @@ def( // use $ to output formatted text to the prompt $`You are an expert at TLA+/TLAPLUS. Your task is to check if the prose comments and their TLA+ declarations and definitions are syntactically and semantically consistent!!! +However, you may assume that that a parser has already checked the syntax of the TLA+ code. Explain any consistencies and inconsistencies you may find. Report inconsistent and consistent pairs in a single ANNOTATION section. ## TLA+ Syntax Hints @@ -30,4 +31,7 @@ Explain any consistencies and inconsistencies you may find. Report inconsistent ## Formal and informal math Hints - Take into account that humans may write informal math that is syntactically different from the formal math, yet semantically equivalent. For example, humans may write \`N > 3T\` instead of \`N > 3 * T\`. + +## Natural language Hints +- Unless a built-in TLA+ declaration or definition like an operator in the TLA+ standard library dictates otherwise, the prose comments should follow British English spelling conventions. `; diff --git a/tla/StatsFile.tla b/tla/StatsFile.tla index d7c709998..d227deac9 100644 --- a/tla/StatsFile.tla +++ b/tla/StatsFile.tla @@ -16,7 +16,7 @@ WriteStatsFile == /\ Serialize(<>, StatsFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>]) \* Append TLC coverage in ndJson format to file identified by CoverageFilename. Create CoverageFilename if it does not exist. -SerialiseCoverage == +SerializeCoverage == Serialize(<>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>]) ==== diff --git a/tla/actions.py b/tla/actions.py index 71b20b6da..16000d4ee 100644 --- a/tla/actions.py +++ b/tla/actions.py @@ -16,7 +16,7 @@ ls -tr _coverage.json | xargs cat | python3 actions.py The spec needs to have constraint like: -SerialiseCoverage == +SerializeCoverage == Serialize(<>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>]) """ diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg index 3e8107e32..0cd0ee3d3 100644 --- a/tla/consensus/MCccfraftAtomicReconfig.cfg +++ b/tla/consensus/MCccfraftAtomicReconfig.cfg @@ -93,4 +93,4 @@ INVARIANTS RetirementCompletedAreRetirementCompletedInv _PERIODIC - SerialiseCoverage \ No newline at end of file + SerializeCoverage \ No newline at end of file diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg index daf7a131d..a1071ffd4 100644 --- a/tla/consensus/MCccfraftWithReconfig.cfg +++ b/tla/consensus/MCccfraftWithReconfig.cfg @@ -92,4 +92,4 @@ INVARIANTS RetirementCompletedAreRetirementCompletedInv _PERIODIC - SerialiseCoverage \ No newline at end of file + SerializeCoverage \ No newline at end of file