From 21e7b54f17924b09a5ca67beaedea0839f2502c4 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Jul 2024 07:39:13 +0200 Subject: [PATCH] chore: check Lean import and copyright header in CI --- .github/workflows/formalities.yml | 28 +++++++++++++++++++ Extract.lean | 6 +++- demo-toml/Demo.lean | 7 +++-- demo-toml/Demo/Basic.lean | 7 ++++- demo-toml/Main.lean | 5 ++++ demo/Demo.lean | 7 +++-- demo/Demo/Basic.lean | 7 ++++- demo/Main.lean | 5 ++++ demo/lakefile.lean | 5 ++++ src/compat/SubVerso/Compat.lean | 5 ++++ src/examples/SubVerso/Examples.lean | 10 +++++-- src/examples/SubVerso/Examples/Env.lean | 5 ++++ src/highlighting/SubVerso/Highlighting.lean | 5 ++++ .../SubVerso/Highlighting/Code.lean | 7 +++++ .../SubVerso/Highlighting/Highlighted.lean | 9 +++++- 15 files changed, 108 insertions(+), 10 deletions(-) create mode 100644 .github/workflows/formalities.yml diff --git a/.github/workflows/formalities.yml b/.github/workflows/formalities.yml new file mode 100644 index 0000000..bd35c0d --- /dev/null +++ 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 index 8cd905d..86d8c91 100644 --- 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 index 2e70ebc..4722907 100644 --- 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 index e99d3a6..a6c7968 100644 --- a/demo-toml/Demo/Basic.lean +++ b/demo-toml/Demo/Basic.lean @@ -1 +1,6 @@ -def hello := "world" \ No newline at end of file +/- +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 index 4a6d743..e2bab30 100644 --- 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 index ff48186..ea368d6 100644 --- 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 index e99d3a6..a6c7968 100644 --- a/demo/Demo/Basic.lean +++ b/demo/Demo/Basic.lean @@ -1 +1,6 @@ -def hello := "world" \ No newline at end of file +/- +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 index 4a6d743..e2bab30 100644 --- 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 index 59cf3c0..f79bf30 100644 --- 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 index 7e22a7b..50a4e0e 100644 --- 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 index 61922d8..2f2a748 100644 --- 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 index d07336d..1dd6adf 100644 --- 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 index 0a0ae0d..93169f5 100644 --- 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 index 8dbc337..c2a7007 100644 --- 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 index 2b8af2c..12ef238 100644 --- 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