CI: check library proofs

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

Author: ahelwer

.github/workflows/ci.yml

@@ -61,6 +61,19 @@ jobs:
                   fi
                 done
                 exit 1
+            - name: Check library proofs
+              run: |
+                find library -type f -iname "*_proofs.tla" -print0    \
+                  \(                                                  \
+                         -not -name "BagsTheorems_proofs.tla"         \
+                    -and -not -name "FiniteSetTheorems_proofs.tla"    \
+                    -and -not -name "FunctionTheorems_proofs.tla"     \
+                    -and -not -name "NaturalsInduction_proofs.tla"    \
+                    -and -not -name "SequenceTheorems_proofs.tla"     \
+                    -and -not -name "SequencesExtTheorems_proofs.tla" \
+                    -and -not -name "WellFoundedInduction_proofs.tla" \
+                  \)                                                  \
+                  | xargs -0 -n1 -r ./_build/tlapm/bin/tlapm --cleanfp
             - name: Run tests
               run: |
                 eval $(opam env)