chore: copyright header housekeeping and CI

leanprover · Mar 21, 2024 · 624d174 · 624d174
1 parent 01cd34e
commit 624d174
Show file tree

Hide file tree

Showing 32 changed files with 158 additions and 10 deletions.
diff --git a/.github/workflows/copyright-header.yml b/.github/workflows/copyright-header.yml
@@ -0,0 +1,20 @@
+name: Check for copyright header
+
+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 ./src -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/src/verso-blog/Verso/Genre/Blog.lean b/src/verso-blog/Verso/Genre/Blog.lean
@@ -1,3 +1,9 @@
+/-
+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
 import SubVerso.Examples
 

diff --git a/src/verso-blog/Verso/Genre/Blog/Basic.lean b/src/verso-blog/Verso/Genre/Blog/Basic.lean
@@ -1,3 +1,9 @@
+/-
+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
 
 import SubVerso.Highlighting

diff --git a/src/verso-blog/Verso/Genre/Blog/Generate.lean b/src/verso-blog/Verso/Genre/Blog/Generate.lean
@@ -1,3 +1,9 @@
+/-
+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 Verso.Genre.Blog.Basic
 import Verso.Genre.Blog.Template
 import Verso.Genre.Blog.Theme

diff --git a/src/verso-blog/Verso/Genre/Blog/LexedText.lean b/src/verso-blog/Verso/Genre/Blog/LexedText.lean
@@ -1,3 +1,9 @@
+/-
+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
 import Verso.Parser
 

diff --git a/src/verso-blog/Verso/Genre/Blog/Site.lean b/src/verso-blog/Verso/Genre/Blog/Site.lean
@@ -1,3 +1,9 @@
+/-
+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 Verso.Doc
 import Verso.Genre.Blog.Basic
 

diff --git a/src/verso-blog/Verso/Genre/Blog/Site/Syntax.lean b/src/verso-blog/Verso/Genre/Blog/Site/Syntax.lean
@@ -1,3 +1,9 @@
+/-
+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
 
 import Verso.Genre.Blog.Site

diff --git a/src/verso-blog/Verso/Genre/Blog/Template.lean b/src/verso-blog/Verso/Genre/Blog/Template.lean
@@ -1,3 +1,9 @@
+/-
+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
 
 import SubVerso.Highlighting

diff --git a/src/verso-blog/Verso/Genre/Blog/Theme.lean b/src/verso-blog/Verso/Genre/Blog/Theme.lean
@@ -1,3 +1,9 @@
+/-
+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 Verso.Genre.Blog.Site
 import Verso.Genre.Blog.Template
 

diff --git a/src/verso-manual/Verso/Genre/Manual.lean b/src/verso-manual/Verso/Genre/Manual.lean
@@ -1,3 +1,9 @@
+/-
+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 Verso.Doc
 import Verso.Doc.Concrete
 import Verso.Doc.TeX

diff --git a/src/verso-manual/Verso/Genre/Manual/Html.lean b/src/verso-manual/Verso/Genre/Manual/Html.lean
@@ -1,3 +1,9 @@
+/-
+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 Verso.Output.Html
 
 namespace Verso.Genre.Manual.Html

diff --git a/src/verso-manual/Verso/Genre/Manual/Html/Style.lean b/src/verso-manual/Verso/Genre/Manual/Html/Style.lean
@@ -1,3 +1,9 @@
+/-
+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
+-/
+
 namespace Verso.Genre.Manual.Html.Css
 
 def pageStyle : String := r####"

diff --git a/src/verso-manual/Verso/Genre/Manual/Slug.lean b/src/verso-manual/Verso/Genre/Manual/Slug.lean
@@ -1,3 +1,9 @@
+/-
+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
 import Verso.Method
 

diff --git a/src/verso-manual/Verso/Genre/Manual/TeX.lean b/src/verso-manual/Verso/Genre/Manual/TeX.lean
@@ -1,3 +1,9 @@
+/-
+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
+-/
+
 namespace Verso.Genre.Manual.TeX
 
 def preamble (title : String) (authors : List String) (date : String) : String :=

diff --git a/src/verso/Verso.lean b/src/verso/Verso.lean
@@ -1,3 +1,9 @@
+/-
+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
+-/
+
 -- This module serves as the root of the `Verso` library.
 -- Import modules here that should be built as part of the library.
 import Verso.Build

diff --git a/src/verso/Verso/Build.lean b/src/verso/Verso/Build.lean
@@ -1,3 +1,9 @@
+/-
+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
 
 import Verso.Doc

diff --git a/src/verso/Verso/Doc.lean b/src/verso/Verso/Doc.lean
@@ -1,8 +1,9 @@
 /-
-Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+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
 
 namespace Verso

diff --git a/src/verso/Verso/Doc/ArgParse.lean b/src/verso/Verso/Doc/ArgParse.lean
@@ -1,3 +1,9 @@
+/-
+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
 import Verso.Doc
 import Verso.Hover

diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+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
 -/

diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+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
 -/

diff --git a/src/verso/Verso/Doc/Elab/ExpanderAttribute.lean b/src/verso/Verso/Doc/Elab/ExpanderAttribute.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+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
 -/

diff --git a/src/verso/Verso/Doc/Elab/InlineString.lean b/src/verso/Verso/Doc/Elab/InlineString.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+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
 -/

diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+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
 -/

diff --git a/src/verso/Verso/Doc/Html.lean b/src/verso/Verso/Doc/Html.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+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
 -/

diff --git a/src/verso/Verso/Doc/Lsp.lean b/src/verso/Verso/Doc/Lsp.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+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
 -/

diff --git a/src/verso/Verso/Doc/Suggestion.lean b/src/verso/Verso/Doc/Suggestion.lean
@@ -1,3 +1,9 @@
+/-
+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
 
 namespace Verso.Doc.Suggestion

diff --git a/src/verso/Verso/Doc/TeX.lean b/src/verso/Verso/Doc/TeX.lean
@@ -1,3 +1,9 @@
+/-
+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 Verso.Doc
 import Verso.Method
 import Verso.Output.TeX

diff --git a/src/verso/Verso/Hover.lean b/src/verso/Verso/Hover.lean
@@ -1,3 +1,9 @@
+/-
+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
 
 namespace Verso.Hover

diff --git a/src/verso/Verso/Output.lean b/src/verso/Verso/Output.lean
@@ -1 +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 Verso.Output.Html
+import Verso.Output.TeX
diff --git a/src/verso/Verso/Output/TeX.lean b/src/verso/Verso/Output/TeX.lean
@@ -1,3 +1,9 @@
+/-
+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
 
 open Lean

diff --git a/src/verso/Verso/Parser.lean b/src/verso/Verso/Parser.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+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
 -/

diff --git a/src/verso/Verso/Syntax.lean b/src/verso/Verso/Syntax.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+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
 -/