leanprover · david-christiansen · Jul 16, 2024 · Jul 16, 2024 · Jul 16, 2024 · Jul 16, 2024
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -15,16 +15,16 @@ jobs:
           - "4.6.0"
           - "4.7.0"
           - "4.8.0"
-          - "4.9.0-rc1"
-          - "nightly-2024-06-12"
+          - "4.9.0"
+          - "nightly-2024-07-12"
         platform:
           - os: ubuntu-latest
             installer: |
               curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
         # Mac runners are rare and expensive, so spot-check that the
         # subprocess support seems OK but be less thorough
         include:
-          - toolchain: "4.8.0"
+          - toolchain: "4.9.0"
             platform:
               os: macos-latest
               installer: |

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,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.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,6 +1,12 @@
-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.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