check that Compfiles.lean is up-to-date in CI

.github/workflows/pull-request.yaml

@@ -31,6 +31,15 @@ jobs:
           result_run1=$?
           echo "Complete at $(date +'%T'); return value $result_run1"
 
+      - name: check that Compfiles.lean is up to date
+        id: check-Compfiles-lean
+        run: |
+          echo "Running mk_toplevel_file.bash..."
+          bash ./scripts/mk_toplevel_file.bash
+          echo "Checking that Compfiles.lean is unchanged..."
+          echo "(If this fails, you should run ./scripts/mk_toplevel_file.bash locally.)"
+          bash ./scripts/assert_working_directory_clean.bash
+
       - name: run extractProblems
         id: run-extractProblems
         run: |

.github/workflows/push-main.yaml

@@ -47,6 +47,15 @@ jobs:
           result_run1=$?
           echo "Complete at $(date +'%T'); return value $result_run1"
 
+      - name: check that Compfiles.lean is up to date
+        id: check-Compfiles-lean
+        run: |
+          echo "Running mk_toplevel_file.bash..."
+          bash ./scripts/mk_toplevel_file.bash
+          echo "Checking that Compfiles.lean is unchanged..."
+          echo "(If this fails, you should run ./scripts/mk_toplevel_file.bash locally.)"
+          bash ./scripts/assert_working_directory_clean.bash
+
       - name: run extractProblems
         id: run-extractProblems
         run: |

Compfiles.lean

@@ -1,12 +1,12 @@
 import Compfiles.Bulgaria1998P1
-import Compfiles.Bulgaria1998P11
 import Compfiles.Bulgaria1998P2
 import Compfiles.Bulgaria1998P3
 import Compfiles.Bulgaria1998P6
 import Compfiles.Bulgaria1998P8
+import Compfiles.Bulgaria1998P11
+import Compfiles.CIIM2022P6
 import Compfiles.Canada1998P3
 import Compfiles.Canada1998P5
-import Compfiles.CIIM2022P6
 import Compfiles.Hungary1998P6
 import Compfiles.Imo1959P1
 import Compfiles.Imo1959P2

scripts/assert_working_directory_clean.bash

@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+OUTPUT=$(git status --porcelain)
+
+if [ -z $OUTPUT ]; then
+    echo "Working directory is clean."
+else
+    echo "Working directory is not clean."
+    echo $OUTPUT
+    git diff
+    exit 1
+fi

scripts/mk_toplevel_file.bash

@@ -11,4 +11,4 @@
 # prepend `import `
 find Compfiles/ -name \*.lean \
   | sed 's,^\./,,;s,/,.,g;s,\.lean$,,;s,^,import ,' \
-  | sort > Compfiles.lean
+  | sort -V > Compfiles.lean