chore: check Lean import and copyright header in CI

leanprover · Jul 16, 2024 · 21e7b54 · 21e7b54
1 parent d4534a1
commit 21e7b54
Show file tree

Hide file tree

Showing 15 changed files with 108 additions and 10 deletions.
diff --git a/.github/workflows/formalities.yml b/.github/workflows/formalities.yml
@@ -0,0 +1,28 @@
+on:
+  push:
+  pull_request:
+
+name: Formalities
+
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Don't 'import Lean', use precise imports
+        if: always()
+        run: |
+          ! (find . -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')
+
+      - name: Verify .lean files start with a copyright header.
+        run: |
+          FILES=$(find ./src ./demo ./demo-toml -not -path '*/.lake/*' -type f -name "*.lean" -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/Extract.lean b/Extract.lean
@@ -1,4 +1,8 @@
-import Lean
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import SubVerso.Examples.Env
 
 open Lean

diff --git a/demo-toml/Demo.lean b/demo-toml/Demo.lean
@@ -1,5 +1,8 @@
--- This module serves as the root of the `Demo` library.
--- Import modules here that should be built as part of the library.
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import «Demo».Basic
 
 import SubVerso.Examples

diff --git a/demo-toml/Demo/Basic.lean b/demo-toml/Demo/Basic.lean
@@ -1 +1,6 @@
-def hello := "world"
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+def hello := "world"
diff --git a/demo-toml/Main.lean b/demo-toml/Main.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import «Demo»
 
 def main : IO Unit :=

diff --git a/demo/Demo.lean b/demo/Demo.lean
@@ -1,5 +1,8 @@
--- This module serves as the root of the `Demo` library.
--- Import modules here that should be built as part of the library.
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import «Demo».Basic
 
 import SubVerso.Examples

diff --git a/demo/Demo/Basic.lean b/demo/Demo/Basic.lean
@@ -1 +1,6 @@
-def hello := "world"
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+def hello := "world"
diff --git a/demo/Main.lean b/demo/Main.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import «Demo»
 
 def main : IO Unit :=

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

diff --git a/src/compat/SubVerso/Compat.lean b/src/compat/SubVerso/Compat.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023-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
 
 open Lean Elab Term

diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean
@@ -1,7 +1,13 @@
+/-
+Copyright (c) 2023-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.Environment
 import SubVerso.Highlighting
 import SubVerso.Compat
 import SubVerso.Examples.Env
-import Lean.Environment
+
 
 namespace SubVerso.Examples
 
@@ -284,7 +290,7 @@ elab_rules : command
     let addScope x := mkIdentFrom x (addMacroScope mod x.getId sc)
     let declName ← match sigName with
       | `(Lean.Parser.Command.declId|$x:ident) => pure x
-      | `(Lean.Parser.Command.declId|$x:ident.{$u:ident,*}) => pure x
+      | `(Lean.Parser.Command.declId|$x:ident.{$_u:ident,*}) => pure x
       | _ => throwErrorAt sigName "Unexpected format of name: {sigName}"
     let target ← liftTermElabM <| Compat.realizeNameNoOverloads declName
     let noClash ← match sigName with

diff --git a/src/examples/SubVerso/Examples/Env.lean b/src/examples/SubVerso/Examples/Env.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import SubVerso.Highlighting
 
 open Lean

diff --git a/src/highlighting/SubVerso/Highlighting.lean b/src/highlighting/SubVerso/Highlighting.lean
@@ -1,2 +1,7 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
 import SubVerso.Highlighting.Highlighted
 import SubVerso.Highlighting.Code
diff --git a/src/highlighting/SubVerso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean
@@ -1,5 +1,12 @@
+/-
+Copyright (c) 2023-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.Widget.InteractiveCode
 import Lean.Widget.TaggedText
 
+
 import SubVerso.Compat
 import SubVerso.Highlighting.Highlighted
 

diff --git a/src/highlighting/SubVerso/Highlighting/Highlighted.lean b/src/highlighting/SubVerso/Highlighting/Highlighted.lean
@@ -1,4 +1,11 @@
-import Lean
+/-
+Copyright (c) 2023-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.Expr
+import Lean.SubExpr -- for the To/FromJSON FVarId instances
 
 open Lean