chore: import plausible everywhere!

leanprover-community · Oct 28, 2024 · a2d68c4 · a2d68c4
1 parent 646e270
commit a2d68c4
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 4 deletions.
diff --git a/.github/build.in.yml b/.github/build.in.yml
@@ -248,7 +248,7 @@ jobs:
       - name: build everything
         # make sure everything is available for test/import_all.lean
         run: |
-          lake build Batteries Qq Aesop ProofWidgets
+          lake build Batteries Qq Aesop ProofWidgets Plausible
 
       - name: test mathlib
         id: test

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -258,7 +258,7 @@ jobs:
       - name: build everything
         # make sure everything is available for test/import_all.lean
         run: |
-          lake build Batteries Qq Aesop ProofWidgets
+          lake build Batteries Qq Aesop ProofWidgets Plausible
 
       - name: test mathlib
         id: test

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -265,7 +265,7 @@ jobs:
       - name: build everything
         # make sure everything is available for test/import_all.lean
         run: |
-          lake build Batteries Qq Aesop ProofWidgets
+          lake build Batteries Qq Aesop ProofWidgets Plausible
 
       - name: test mathlib
         id: test

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -262,7 +262,7 @@ jobs:
       - name: build everything
         # make sure everything is available for test/import_all.lean
         run: |
-          lake build Batteries Qq Aesop ProofWidgets
+          lake build Batteries Qq Aesop ProofWidgets Plausible
 
       - name: test mathlib
         id: test

diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean
@@ -9,6 +9,7 @@ import Mathlib.Tactic.Linter.OldObtain
 import Mathlib.Tactic.Linter.RefineLinter
 import Mathlib.Tactic.Linter.UnusedTactic
 import Mathlib.Tactic.Linter.Style
+import Plausible.Tactic -- allows everyone access to plausible
 
 /-!
 This is the root file in Mathlib: it is imported by virtually *all* Mathlib files.

diff --git a/test/import_all.lean b/test/import_all.lean
@@ -5,6 +5,7 @@ import Batteries
 import Aesop
 import ProofWidgets
 import Mathlib
+import Plausible
 
 /-!
 Verify that Mathlib and all its upstream dependencies can be simultaneously imported.