test: diff in lean

.github/workflows/bors.yml

@@ -136,6 +136,9 @@ jobs:
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
       - uses: actions/checkout@v4
+        with:
+          ## fetch the whole repository, useful to find a common fork
+          fetch-depth: 0
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
@@ -206,6 +209,12 @@ jobs:
             lake build --no-build
           fi
 
+      - name: decl-diff
+        run: |
+          git checkout master
+          git checkout -
+          ./scripts/decls_diff_hybrid.sh "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"
+
       - name: build archive
         id: archive
         run: |

.github/workflows/build.yml

@@ -143,6 +143,9 @@ jobs:
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
       - uses: actions/checkout@v4
+        with:
+          ## fetch the whole repository, useful to find a common fork
+          fetch-depth: 0
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
@@ -213,6 +216,12 @@ jobs:
             lake build --no-build
           fi
 
+      - name: decl-diff
+        run: |
+          git checkout master
+          git checkout -
+          ./scripts/decls_diff_hybrid.sh "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"
+
       - name: build archive
         id: archive
         run: |

.github/workflows/build.yml.in

@@ -122,6 +122,9 @@ jobs:
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
       - uses: actions/checkout@v4
+        with:
+          ## fetch the whole repository, useful to find a common fork
+          fetch-depth: 0
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
@@ -192,6 +195,12 @@ jobs:
             lake build --no-build
           fi
 
+      - name: decl-diff
+        run: |
+          git checkout master
+          git checkout -
+          ./scripts/decls_diff_hybrid.sh "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"
+
       - name: build archive
         id: archive
         run: |

.github/workflows/build_fork.yml

@@ -140,6 +140,9 @@ jobs:
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
       - uses: actions/checkout@v4
+        with:
+          ## fetch the whole repository, useful to find a common fork
+          fetch-depth: 0
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
@@ -210,6 +213,12 @@ jobs:
             lake build --no-build
           fi
 
+      - name: decl-diff
+        run: |
+          git checkout master
+          git checkout -
+          ./scripts/decls_diff_hybrid.sh "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"
+
       - name: build archive
         id: archive
         run: |

scripts/decls_diff_hybrid.sh

@@ -0,0 +1,50 @@
+#! /usr/bin/env bash
+
+# running `./scripts/decls_diff_hybrid.sh commit1 commit2`
+# creates two files, `tempDecls1.txt` and `tempDecls2.txt`,
+# the former containing all the declarations in `commit1`
+# the latter containing all the declarations in `commit2`
+
+# the location of the script
+scr=scripts/list_decls.lean
+commit1="${1}"
+commit2="${2}"
+temp1='tempDecls1.txt'
+temp2='tempDecls2.txt'
+currentHash="$(git rev-parse HEAD)"
+
+# `getDecls`
+# 1. retrieves the script file from either master or the PR commit
+# 2. gets the cache
+# 3. in the lean-script file, removes `--` before `list_decls` and parses the lean file
+getDecls () {
+  # we check out the script that is in the current branch
+  git checkout "${currentHash}" "${scr}"
+  lake exe cache get
+  sed 's=^--\(list_decls\)=\1=' "${scr}" |
+    lake env lean --stdin
+}
+
+# `processDeclsInOneCommit commitHash tempFile`
+# stores the declarations in `commitHash` in the file `tempFile`
+# makes sure to come back to the original git branch
+processDeclsInOneCommit () {
+  # check that the temporary file does not already exist, exiting otherwise
+  if [ -f "${2}" ]; then
+    printf 'File `%s` already exist, please rename and try again\n' "${2}"
+    exit 1
+  fi
+  git checkout "${1}"
+  getDecls > "${2}"
+  git switch -
+}
+
+# save the declarations in `commit1` to `tempDecls1.txt`
+processDeclsInOneCommit "${commit1}" "${temp1}"
+# save the declarations in `commit2` to `tempDecls2.txt`
+processDeclsInOneCommit "${commit2}" "${temp2}"
+# restore the cache in the initial branch
+lake exe cache get
+
+printf 'Declarations only in %s\n%s\n\n' "${commit1}" "$(comm -23 <(sort "${temp1}") <(sort "${temp2}"))"
+printf 'Declarations only in %s\n%s\n\n' "${commit2}" "$(comm -13 <(sort "${temp1}") <(sort "${temp2}"))"

scripts/list_decls.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2024 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import Mathlib --.Lean.Expr.Basic
+
+/-!
+# `list_decls`
+
+Building this file outputs the fully-qualified name of "every" declaration in the environment.
+-/
+
+namespace ListDecls
+open Lean Elab Meta Command
+
+/-- `listDeclsCore` is the main implementation of the `list_decls` command. -/
+def listDeclsCore {m : Type → Type} [Monad m] [MonadEnv m] (all? : Bool) :
+    m (Array Name) := do
+  let names ← (← getEnv).constants.map₁.foldM (init := #[]) (fun ns n c => do
+    if all? && (c.isUnsafe || (← n.isBlackListed)) then return ns else return ns.push n)
+  return names.qsort (·.toString < ·.toString)
+
+/-- The `list_decls` command prints the array of all non-unsafe, non-blacklisted declarations in
+the environment.
+
+To include *all* declarations, use `list_decls!`.
+-/
+elab (name := listDeclsCmd) "list_decls" tk:"!"? : command => do
+  IO.println <| "\n".intercalate <| (← listDeclsCore tk.isNone).map (·.toString) |>.toList
+
+@[inherit_doc listDeclsCmd]
+macro "list_decls!" : command => `(list_decls !)
+
+end ListDecls
+
+--list_decls