Add workflow to check for presence of copyright headers (#185)

### Description: Add a workflow to check whether the Copyright header is present in all Lean files (borrowed from [Lean's own workflow](https://github.com/leanprover/lean4/blob/master/.github/workflows/copyright-header.yml)). ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing successful on an Aarch64 machine? Yes. ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.
leanprover · Sep 24, 2024 · 27a2f3b · 27a2f3b
1 parent 1a642b2
commit 27a2f3b
Show file tree

Hide file tree

Showing 6 changed files with 48 additions and 18 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 . -type d \( -path "./.lake" \) -prune -o -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/Arm/Attr.lean b/Arm/Attr.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Shilpi Goel
+-/
+
 import Lean
 
 -- A minimal theory, safe for all LNSym proofs
@@ -9,21 +15,3 @@ register_simp_attr state_simp_rules
 register_simp_attr bitvec_rules
 -- Rules for memory lemmas
 register_simp_attr memory_rules
-
-/-
-syntax "state_simp" : tactic
-macro_rules
-  | `(tactic| state_simp) => `(tactic| simp only [state_simp_rules])
-
-syntax "state_simp?" : tactic
-macro_rules
-  | `(tactic| state_simp?) => `(tactic| simp? only [state_simp_rules])
-
-syntax "state_simp_all" : tactic
-macro_rules
-  | `(tactic| state_simp_all) => `(tactic| simp_all only [state_simp_rules])
-
-syntax "state_simp_all?" : tactic
-macro_rules
-  | `(tactic| state_simp_all?) => `(tactic| simp_all? only [state_simp_rules])
--/
diff --git a/Arm/FromMathlib.lean b/Arm/FromMathlib.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+
+
 -- This file has definitions temporarily lifted from Mathlib.
 -- We will move them into Lean shortly.
 

diff --git a/Arm/MinTheory.lean b/Arm/MinTheory.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Shilpi Goel
+-/
+
 import Arm.Attr
 
 -- These lemmas are from lean/Init/SimpLemmas.lean.

diff --git a/Proofs/SHA512/SHA512.lean b/Proofs/SHA512/SHA512.lean
@@ -1,2 +1,7 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Shilpi Goel
+-/
 import Proofs.SHA512.SHA512_block_armv8_rules
 import Proofs.SHA512.SHA512Sym
diff --git a/lakefile.lean b/lakefile.lean
@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Shilpi Goel
+-/
 import Lake
 open Lake DSL