chore: CI: flag Lean modules importing Init

.github/workflows/ci.yml

@@ -470,6 +470,28 @@ jobs:
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 
+  # checks that each `Lean` module contains a `prelude` line
+  check-prelude:
+    needs: build
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          sparse-checkout: src/Lean
+      - name: Check Prelude
+        run: |
+          failed_files=""
+          while IFS= read -r -d '' file; do
+            if ! grep -q "^prelude$" "$file"; then
+              failed_files="$failed_files$file\n"
+            fi
+          done < <(find src/Lean -type f -print0)
+          if [ -n "$failed_files" ]; then
+            echo -e "The following files should not import `Init`:\n$failed_files"
+            exit 1
+          fi
+
   # This job creates nightly releases during the cron job.
   # It is responsible for creating the tag, and automatically generating a changelog.
   release-nightly: