diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 0000000..3d63f57 --- /dev/null +++ b/.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 {} \; diff --git a/test/Imports.lean b/test/Imports.lean new file mode 100644 index 0000000..867bb79 --- /dev/null +++ b/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