fix: remove check for oleans in assert_not_imported (#15839)

See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/assert_not_imported) for a discussion of the issues arising from looking for `olean`s, rather than `lean`s.

As a test, this PR also incorporates some uses of `assert_not_imported` to verify that CI and `!bench` work!

Author: adomani

Mathlib/Algebra/BigOperators/Group/List.lean

@@ -21,9 +21,7 @@ of elements of a list and `List.alternatingProd`, `List.alternatingSum`, their a
 counterparts.
 -/
 
--- Make sure we haven't imported `Data.Nat.Order.Basic`
-assert_not_exists OrderedSub
-assert_not_exists Ring
+assert_not_imported Mathlib.Algebra.Order.Group.Nat
 
 variable {ι α β M N P G : Type*}
 

Mathlib/Algebra/Field/Defs.lean

@@ -43,12 +43,11 @@ a `GroupWithZero` lemma instead.
 field, division ring, skew field, skew-field, skewfield
 -/
 
+assert_not_imported Mathlib.Tactic.Common
+
 -- `NeZero` should not be needed in the basic algebraic hierarchy.
 assert_not_exists NeZero
 
--- Check that we have not imported `Mathlib.Tactic.Common` yet.
-assert_not_exists Mathlib.Tactic.scopedNS
-
 assert_not_exists MonoidHom
 
 open Function Set

Mathlib/Data/List/Chain.lean

@@ -18,8 +18,7 @@ A graph-specialized version is in development and will hopefully be added under
 sometime soon.
 -/
 
--- Make sure we haven't imported `Data.Nat.Order.Basic`
-assert_not_exists OrderedSub
+assert_not_imported Mathlib.Algebra.Order.Group.Nat
 
 universe u v
 

Mathlib/Data/List/GetD.lean

@@ -13,11 +13,9 @@ import Mathlib.Util.AssertExists
 This file provides theorems for working with the `getD` and `getI` functions. These are used to
 access an element of a list by numerical index, with a default value as a fallback when the index
 is out of range.
-
 -/
 
--- Make sure we haven't imported `Data.Nat.Order.Basic`
-assert_not_exists OrderedSub
+assert_not_imported Mathlib.Algebra.Order.Group.Nat
 
 namespace List
 

Mathlib/Util/AssertExists.lean

@@ -72,12 +72,10 @@ elab "assert_not_exists " n:ident : command => do
 /-- `assert_not_imported m₁ m₂ ... mₙ` checks that each one of the modules `m₁ m₂ ... mₙ` is not
 among the transitive imports of the current file.
 
-It also checks that each one of `m₁ m₂ ... mₙ` is actually the name of an existing module, just
-one that is not currently imported!
+The command does not currently check whether the modules `m₁ m₂ ... mₙ` actually exist.
 -/
+-- TODO: make sure that each one of `m₁ m₂ ... mₙ` is the name of an actually existing module!
 elab "assert_not_imported " ids:ident+ : command => do
   let mods := (← getEnv).allImportedModuleNames
   for id in ids do
     if mods.contains id.getId then logWarningAt id m!"the module '{id}' is (transitively) imported"
-    if let none ← (← searchPathRef.get).findModuleWithExt "olean" id.getId then
-      logErrorAt id m!"the module '{id}' does not exist"

test/AssertExists.lean

@@ -1,10 +1,6 @@
 import Mathlib.Util.AssertExists
 
-/--
-warning: the module 'Lean.Elab.Command' is (transitively) imported
----
-error: the module 'I_do_not_exist' does not exist
--/
+/-- warning: the module 'Lean.Elab.Command' is (transitively) imported -/
 #guard_msgs in
 assert_not_imported
   Mathlib.Tactic.Common