add test

.github/workflows/build.yml

@@ -0,0 +1,27 @@
+name: Build
+run-name: Build the project
+on: [push]
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+      - uses: actions/checkout@v4
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+      - run: lake build
+      - name: verify `lake exe graph` works
+        run: |
+          lake exe graph
+          rm import_graph.dot
+      - name: run tests
+        id: test
+        run: |
+          find test/*.lean -exec lake env lean {} \;

test/Imports.lean

@@ -0,0 +1,57 @@
+import ImportGraph.Imports
+import ImportGraph.RequiredModules
+
+open Lean
+
+def importTest : CoreM Unit := do
+  let x ← redundantImports
+  logInfo s!"{x.toArray}"
+
+/-
+info:
+Found the following transitively redundant imports:
+ImportGraph.RequiredModules
+-/
+#redundant_imports
+
+/-
+info:
+import ImportGraph.Imports
+-/
+#minimize_imports
+
+/-
+info:
+[ImportGraph.Imports]
+-/
+#find_home importTest
+
+
+open Elab Command in
+elab "#my_test" : command => do
+  -- functionality of `#redundant_imports`
+  let expected := #[`ImportGraph.RequiredModules]
+  let ri ← liftCoreM redundantImports
+  if (ri.toArray != expected) then
+    logError s!"Failed: `redundantImports` returned {ri.toArray} instead of {expected}"
+
+  -- functionality of `#find_home`
+  let expected := #[`ImportGraph.Imports]
+  let mi ← liftCoreM <| Lean.Name.findHome `importTest none
+  if (mi.toArray != expected) then
+      logError s!"Failed: `findHome` returned {mi.toArray} instead of {expected}"
+
+  -- functionality of `#find_home!`
+  let expected := #[`ImportGraph.Imports]
+  let mi! ← liftCoreM <| Lean.Name.findHome `importTest (← getEnv)
+  if (mi!.toArray != expected) then
+      logError s!"Failed: `findHome (!)` returned {mi!.toArray} instead of {expected}"
+
+  logInfo s!"{mi.toArray}"
+  pure ()
+
+/-
+info:
+#[ImportGraph.RequiredModules]
+-/
+#my_test