config

b-mehta · Sep 26, 2024 · 834fe99 · 834fe99
1 parent 6549727
commit 834fe99
Show file tree

Hide file tree

Showing 7 changed files with 6 additions and 6 deletions.
diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml
@@ -21,10 +21,10 @@ jobs:
         if: always() # Ensure the step runs regardless of the success or failure of previous steps
         run: |
           # Find Lean files with lines longer than 100 characters, excluding URLs
-          ! (find Project -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
+          ! (find equational_theories -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
 
       - name: Don't 'import Mathlib', use precise imports
         if: always() # Ensure the step runs regardless of the success or failure of previous steps
         run: |
           # Find and disallow any file that imports the entire Mathlib, encouraging precise imports instead
-          ! (find Project -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
+          ! (find equational_theories -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
diff --git a/Project.lean b/Project.lean
diff --git a/equational_theories.lean b/equational_theories.lean
@@ -0,0 +1 @@
+import equational_theories.Example
diff --git a/Project/Example.lean → equational_theories/Example.lean b/Project/Example.lean → equational_theories/Example.lean
diff --git a/Project/ForMathlib/README.md → equational_theories/ForMathlib/README.md b/Project/ForMathlib/README.md → equational_theories/ForMathlib/README.md
diff --git a/Project/Mathlib/README.md → equational_theories/Mathlib/README.md b/Project/Mathlib/README.md → equational_theories/Mathlib/README.md
diff --git a/lakefile.toml b/lakefile.toml
@@ -1,5 +1,5 @@
-name = "Project"
-defaultTargets = ["Project"]
+name = "equational_theories"
+defaultTargets = ["equational_theories"]
 
 [leanOptions]
 pp.unicode.fun = true
@@ -11,4 +11,4 @@ name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
 
 [[lean_lib]]
-name = "Project"
+name = "equational_theories"