chore: CI: flag Lean modules not using prelude (#3463)

Co-authored-by: Henrik Böving <hargonix@gmail.com>

.github/workflows/check-prelude.yml

@@ -0,0 +1,26 @@
+name: Check for modules that should use `prelude`
+
+on: [pull_request]
+
+jobs:
+  check-prelude:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          # the default is to use a virtual merge commit between the PR and master: just use the PR
+          ref: ${{ github.event.pull_request.head.sha }}
+          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 -name '*.lean' -print0)
+          if [ -n "$failed_files" ]; then
+            echo -e "The following files use 'prelude':\n$failed_files"
+            exit 1
+          fi

src/Lean/Elab/Tactic/NormCast.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
 -/
+prelude
 import Lean.Meta.Tactic.NormCast
 import Lean.Elab.Tactic.Conv.Simp
 import Lean.Elab.ElabRules

src/Lean/Elab/Tactic/Omega.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+prelude
 import Lean.Elab.Tactic.Omega.Frontend
 
 /-!

src/Lean/Elab/Tactic/Omega/Core.lean

@@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+prelude
+import Init.Omega.Constraint
 import Lean.Elab.Tactic.Omega.OmegaM
 import Lean.Elab.Tactic.Omega.MinNatAbs
 

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+prelude
 import Lean.Elab.Tactic.Omega.Core
 import Lean.Elab.Tactic.FalseOrByContra
 import Lean.Meta.Tactic.Cases

src/Lean/Elab/Tactic/Omega/MinNatAbs.lean

@@ -3,6 +3,10 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+prelude
+import Init.BinderPredicates
+import Init.Data.List
+import Init.Data.Option
 
 /-!
 # `List.nonzeroMinimum`, `List.minNatAbs`, `List.maxNatAbs`

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -3,6 +3,10 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+prelude
+import Init.Omega.LinearCombo
+import Init.Omega.Int
+import Init.Omega.Logic
 import Lean.Meta.AppBuilder
 
 /-!

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+prelude
 import Lean.Elab.ElabRules
 import Lean.Elab.Tactic.Simp
 import Lean.Meta.Tactic.TryThis

src/Lean/Elab/Tactic/Simpa.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Gabriel Ebner, Mario Carneiro
 -/
+prelude
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Tactic.Simp

src/Lean/Meta/CompletionName.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-
+prelude
 import Lean.Meta.Basic
 import Lean.Meta.Match.MatcherInfo
 

src/Lean/Meta/Tactic/NormCast.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
 -/
+prelude
 import Lean.Meta.CongrTheorems
 import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.CoeAttr

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.ToExpr
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.ToExpr
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char