chore: copyright headers and Lean imports size in CI (#88)

leanprover · Oct 21, 2024 · eff3536 · eff3536
1 parent 87b9112
commit eff3536
Show file tree

Hide file tree

Showing 39 changed files with 252 additions and 0 deletions.
diff --git a/.github/workflows/copyright-header.yml b/.github/workflows/copyright-header.yml
@@ -0,0 +1,20 @@
+name: Check for copyright headers
+
+on: [pull_request]
+
+jobs:
+  check-lean-files:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Verify .lean files start with a copyright header.
+      run: |
+        FILES=$(find . -type f -name "*.lean" -not -path "./.lake/*" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
+        if [ -n "$FILES" ]; then
+          echo "Found .lean files which do not have a copyright header:"
+          echo "$FILES"
+          exit 1
+        else
+          echo "All copyright headers present."
+        fi
diff --git a/.github/workflows/too-big-imports.yml b/.github/workflows/too-big-imports.yml
@@ -0,0 +1,14 @@
+name: Check for too-big Lean imports
+
+on: [pull_request]
+
+jobs:
+  check-lean-files:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Don't 'import Lean', use precise imports
+      run: |
+        ! (find . -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')
+
diff --git a/Main.lean b/Main.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import Manual
 import Manual.Meta
 import VersoManual

diff --git a/Manual.lean b/Manual.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import VersoManual
 
 import Manual.Intro

diff --git a/Manual/BuiltInTypes.lean b/Manual/BuiltInTypes.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/BuiltInTypes/Nat.lean b/Manual/BuiltInTypes/Nat.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/BuiltInTypes/String.lean b/Manual/BuiltInTypes/String.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/BuiltInTypes/String/FFI.lean b/Manual/BuiltInTypes/String/FFI.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/BuiltInTypes/String/Literals.lean b/Manual/BuiltInTypes/String/Literals.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/BuiltInTypes/String/Logical.lean b/Manual/BuiltInTypes/String/Logical.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/Intro.lean b/Manual/Intro.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/Language.lean b/Manual/Language.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/Language/Files.lean b/Manual/Language/Files.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/Language/Functions.lean b/Manual/Language/Functions.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/Language/InductiveTypes/LogicalModel.lean b/Manual/Language/InductiveTypes/LogicalModel.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 import Manual.Meta
 

diff --git a/Manual/Language/InductiveTypes/Structures.lean b/Manual/Language/InductiveTypes/Structures.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta

diff --git a/Manual/Meta.lean b/Manual/Meta.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
 

diff --git a/Manual/Meta/Attribute.lean b/Manual/Meta/Attribute.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Verso.Code.Highlighted

diff --git a/Manual/Meta/Basic.lean b/Manual/Meta/Basic.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import Lean.Data.Position
 import Lean.Parser
 

diff --git a/Manual/Meta/Bibliography.lean b/Manual/Meta/Bibliography.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import Lean.Data.Json
 import Lean.Elab.InfoTree.Types
 

diff --git a/Manual/Meta/CustomStyle.lean b/Manual/Meta/CustomStyle.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 import Lean.Data.Json
 

diff --git a/Manual/Meta/Example.lean b/Manual/Meta/Example.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 import Manual.Meta.Figure
 import Manual.Meta.Lean

diff --git a/Manual/Meta/Figure.lean b/Manual/Meta/Figure.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 import Lean.Elab.InfoTree.Types
 

diff --git a/Manual/Meta/Lean.lean b/Manual/Meta/Lean.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
 

diff --git a/Manual/Meta/Lean/Scopes.lean b/Manual/Meta/Lean/Scopes.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import Lean.Elab.Command
 import Lean.Environment
 

diff --git a/Manual/Meta/Marginalia.lean b/Manual/Meta/Marginalia.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import Verso
 import Verso.Doc.ArgParse
 import Verso.Doc.Elab.Monad

diff --git a/Manual/Meta/PPrint.lean b/Manual/Meta/PPrint.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import Lean.Data.RBMap
 import Lean.Data.Json
 import Lean.Widget.TaggedText

diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Verso.Code.Highlighted

diff --git a/Manual/Meta/Tactics.lean b/Manual/Meta/Tactics.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import Lean.Elab.Term
 import Lean.Elab.Tactic
 

diff --git a/Manual/Simp.lean b/Manual/Simp.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Lean.Parser.Term

diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Lean.Parser.Term

diff --git a/Manual/Tactics/Conv.lean b/Manual/Tactics/Conv.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Lean.Parser.Term

diff --git a/Manual/Tactics/Custom.lean b/Manual/Tactics/Custom.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Lean.Parser.Term

diff --git a/Manual/Tactics/Reference.lean b/Manual/Tactics/Reference.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Lean.Parser.Term

diff --git a/Manual/Tactics/Reference/Simp.lean b/Manual/Tactics/Reference/Simp.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Lean.Parser.Term

diff --git a/Manual/Terms.lean b/Manual/Terms.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
 import VersoManual
 
 import Manual.Meta