diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index e6593ec8a0..ca4847dcc0 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -147,7 +147,7 @@ rec { ln -sf ${lean-all}/* . ''; buildPhase = '' - ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)|laketest' -j$NIX_BUILD_CORES + ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)|laketest|leanpkgtest' -j$NIX_BUILD_CORES ''; installPhase = '' touch $out diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index d8c9a40ec3..78493d2513 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -126,6 +126,17 @@ FOREACH(T ${LEANT0TESTS}) COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T) +# LEAN PACKAGE TESTS +file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*") +FOREACH(T ${LEANPKGTESTS}) + if(IS_DIRECTORY ${T}) + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leanpkgtest_${T_NAME}" + WORKING_DIRECTORY "${T}" + COMMAND bash -c "${TEST_VARS} ./test.sh") + endif() +ENDFOREACH(T) + # LEAN SERVER TESTS file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/server/*.lean") FOREACH(T ${LEANTESTS}) @@ -149,7 +160,6 @@ FOREACH(T ${LEANTESTS}) ENDFOREACH(T) # Create a lake test for each subdirectory of `lake/examples` which contains a `test.sh` file. -# We skip the subdirectories `lean_packages` and `bootstrap` since `lake/examples/Makefile` does not consider them either. file(GLOB_RECURSE LEANLAKETESTS "${LEAN_SOURCE_DIR}/lake/examples/test.sh") FOREACH(T ${LEANLAKETESTS}) if(NOT T MATCHES ".*lean_packages.*") diff --git a/tests/pkg/.gitignore b/tests/pkg/.gitignore new file mode 100644 index 0000000000..567609b123 --- /dev/null +++ b/tests/pkg/.gitignore @@ -0,0 +1 @@ +build/ diff --git a/tests/pkg/builtin_attr/UserAttr.lean b/tests/pkg/builtin_attr/UserAttr.lean new file mode 100644 index 0000000000..28b59b3472 --- /dev/null +++ b/tests/pkg/builtin_attr/UserAttr.lean @@ -0,0 +1 @@ +import UserAttr.Tst diff --git a/tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean b/tests/pkg/builtin_attr/UserAttr/BlaAttr.lean similarity index 100% rename from tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean rename to tests/pkg/builtin_attr/UserAttr/BlaAttr.lean diff --git a/tests/pkg/builtin_attr/UserAttr/Tst.lean b/tests/pkg/builtin_attr/UserAttr/Tst.lean new file mode 100644 index 0000000000..76870872c4 --- /dev/null +++ b/tests/pkg/builtin_attr/UserAttr/Tst.lean @@ -0,0 +1,4 @@ +import UserAttr.BlaAttr + +@[bar] def f (x : Nat) := x + 2 +@[bar] def g (x : Nat) := x + 1 diff --git a/tests/pkg/builtin_attr/lakefile.lean b/tests/pkg/builtin_attr/lakefile.lean new file mode 100644 index 0000000000..8311eac741 --- /dev/null +++ b/tests/pkg/builtin_attr/lakefile.lean @@ -0,0 +1,5 @@ +import Lake +open System Lake DSL + +package user_attr where + defaultFacet := PackageFacet.oleans diff --git a/tests/pkg/builtin_attr/test.sh b/tests/pkg/builtin_attr/test.sh new file mode 100755 index 0000000000..438bb1c522 --- /dev/null +++ b/tests/pkg/builtin_attr/test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +rm -rf build +lake build diff --git a/tests/pkg/deriving/UserDeriving.lean b/tests/pkg/deriving/UserDeriving.lean new file mode 100644 index 0000000000..92d1187af1 --- /dev/null +++ b/tests/pkg/deriving/UserDeriving.lean @@ -0,0 +1 @@ +import UserDeriving.Tst diff --git a/tests/pkg/deriving/UserDeriving/Simple.lean b/tests/pkg/deriving/UserDeriving/Simple.lean new file mode 100644 index 0000000000..23026e847a --- /dev/null +++ b/tests/pkg/deriving/UserDeriving/Simple.lean @@ -0,0 +1,15 @@ +import Lean + +class Simple (α : Type u) where + val : α + +open Lean +open Lean.Elab +open Lean.Elab.Command +def mkSimpleHandler (declNames : Array Name) : CommandElabM Bool := do + dbg_trace ">> mkSimpleHandler {declNames}" + -- TODO: see examples at src/Lean/Elab/Deriving + return true + +initialize + registerBuiltinDerivingHandler ``Simple mkSimpleHandler diff --git a/tests/pkg/deriving/UserDeriving/Tst.lean b/tests/pkg/deriving/UserDeriving/Tst.lean new file mode 100644 index 0000000000..51970ac3d9 --- /dev/null +++ b/tests/pkg/deriving/UserDeriving/Tst.lean @@ -0,0 +1,6 @@ +import UserDeriving.Simple + +inductive Foo where + | mk₁ + | mk₂ + deriving Simple diff --git a/tests/pkg/deriving/lakefile.lean b/tests/pkg/deriving/lakefile.lean new file mode 100644 index 0000000000..42141814ea --- /dev/null +++ b/tests/pkg/deriving/lakefile.lean @@ -0,0 +1,5 @@ +import Lake +open System Lake DSL + +package user_deriving where + defaultFacet := PackageFacet.oleans diff --git a/tests/pkg/deriving/test.sh b/tests/pkg/deriving/test.sh new file mode 100755 index 0000000000..438bb1c522 --- /dev/null +++ b/tests/pkg/deriving/test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +rm -rf build +lake build diff --git a/tests/pkg/prv/Prv.lean b/tests/pkg/prv/Prv.lean new file mode 100644 index 0000000000..7d4ffe3509 --- /dev/null +++ b/tests/pkg/prv/Prv.lean @@ -0,0 +1,5 @@ +import Prv.Foo + +#check { name := "leo", val := 15 : Foo } +#check { name := "leo", val := 15 : Foo }.name +#check { name := "leo", val := 15 : Foo }.val -- Error diff --git a/tests/pkg/prv/Prv/Foo.lean b/tests/pkg/prv/Prv/Foo.lean new file mode 100644 index 0000000000..5a386ecd88 --- /dev/null +++ b/tests/pkg/prv/Prv/Foo.lean @@ -0,0 +1,6 @@ +structure Foo where + private val : Nat + name : String + +#check { name := "leo", val := 15 : Foo } +#check { name := "leo", val := 15 : Foo }.val diff --git a/tests/pkg/prv/lakefile.lean b/tests/pkg/prv/lakefile.lean new file mode 100644 index 0000000000..1ebd86098e --- /dev/null +++ b/tests/pkg/prv/lakefile.lean @@ -0,0 +1,5 @@ +import Lake +open System Lake DSL + +package prv where + defaultFacet := PackageFacet.oleans diff --git a/tests/pkg/prv/test.sh b/tests/pkg/prv/test.sh new file mode 100755 index 0000000000..7b870756d1 --- /dev/null +++ b/tests/pkg/prv/test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +rm -rf build +lake build 2>&1 | grep 'error: field.*private' diff --git a/tests/pkg/user_attr/UserAttr.lean b/tests/pkg/user_attr/UserAttr.lean new file mode 100644 index 0000000000..ec633fea1c --- /dev/null +++ b/tests/pkg/user_attr/UserAttr.lean @@ -0,0 +1,12 @@ +import UserAttr.Tst + +open Lean + +def tst : MetaM Unit := do + let env ← getEnv + assert! (blaAttr.hasTag env `f) + assert! (blaAttr.hasTag env `g) + assert! !(blaAttr.hasTag env `id) + pure () + +#eval tst diff --git a/tests/pkg/user_attr/UserAttr/BlaAttr.lean b/tests/pkg/user_attr/UserAttr/BlaAttr.lean new file mode 100644 index 0000000000..7314fc152b --- /dev/null +++ b/tests/pkg/user_attr/UserAttr/BlaAttr.lean @@ -0,0 +1,5 @@ +import Lean + +open Lean + +initialize blaAttr : TagAttribute ← registerTagAttribute `bla "simple user defined attribute" diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean new file mode 100644 index 0000000000..f80db320f8 --- /dev/null +++ b/tests/pkg/user_attr/UserAttr/Tst.lean @@ -0,0 +1,4 @@ +import UserAttr.BlaAttr + +@[bla] def f (x : Nat) := x + 2 +@[bla] def g (x : Nat) := x + 1 diff --git a/tests/pkg/user_attr/lakefile.lean b/tests/pkg/user_attr/lakefile.lean new file mode 100644 index 0000000000..8311eac741 --- /dev/null +++ b/tests/pkg/user_attr/lakefile.lean @@ -0,0 +1,5 @@ +import Lake +open System Lake DSL + +package user_attr where + defaultFacet := PackageFacet.oleans diff --git a/tests/pkg/user_attr/test.sh b/tests/pkg/user_attr/test.sh new file mode 100755 index 0000000000..438bb1c522 --- /dev/null +++ b/tests/pkg/user_attr/test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +rm -rf build +lake build diff --git a/tests/leanpkg/user_attr_app/UserAttr.lean b/tests/pkg/user_attr_app/Main.lean similarity index 85% rename from tests/leanpkg/user_attr_app/UserAttr.lean rename to tests/pkg/user_attr_app/Main.lean index 5eebfc9430..f6813143e0 100644 --- a/tests/leanpkg/user_attr_app/UserAttr.lean +++ b/tests/pkg/user_attr_app/Main.lean @@ -12,5 +12,5 @@ def tst : MetaM Unit := do #eval tst unsafe def main : IO Unit := do - initSearchPath (← Lean.findSysroot?) ["build"] + initSearchPath (← Lean.findSysroot?) ["build/lib"] withImportModules [{ module := `UserAttr.Tst : Import }] {} 0 fun env => pure () diff --git a/tests/pkg/user_attr_app/UserAttr/BlaAttr.lean b/tests/pkg/user_attr_app/UserAttr/BlaAttr.lean new file mode 100644 index 0000000000..7314fc152b --- /dev/null +++ b/tests/pkg/user_attr_app/UserAttr/BlaAttr.lean @@ -0,0 +1,5 @@ +import Lean + +open Lean + +initialize blaAttr : TagAttribute ← registerTagAttribute `bla "simple user defined attribute" diff --git a/tests/pkg/user_attr_app/UserAttr/Tst.lean b/tests/pkg/user_attr_app/UserAttr/Tst.lean new file mode 100644 index 0000000000..f80db320f8 --- /dev/null +++ b/tests/pkg/user_attr_app/UserAttr/Tst.lean @@ -0,0 +1,4 @@ +import UserAttr.BlaAttr + +@[bla] def f (x : Nat) := x + 2 +@[bla] def g (x : Nat) := x + 1 diff --git a/tests/pkg/user_attr_app/lakefile.lean b/tests/pkg/user_attr_app/lakefile.lean new file mode 100644 index 0000000000..c811a7c7b8 --- /dev/null +++ b/tests/pkg/user_attr_app/lakefile.lean @@ -0,0 +1,5 @@ +import Lake +open System Lake DSL + +package user_attr where + supportInterpreter := true diff --git a/tests/pkg/user_attr_app/test.sh b/tests/pkg/user_attr_app/test.sh new file mode 100755 index 0000000000..b17e5675dc --- /dev/null +++ b/tests/pkg/user_attr_app/test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +rm -rf build +lake build && ./build/bin/user_attr diff --git a/tests/pkg/user_ext/UserExt.lean b/tests/pkg/user_ext/UserExt.lean new file mode 100644 index 0000000000..b8531c360c --- /dev/null +++ b/tests/pkg/user_ext/UserExt.lean @@ -0,0 +1,5 @@ +import UserExt.Tst1 +import UserExt.Tst2 + +show_foo_set +show_bla_set diff --git a/tests/pkg/user_ext/UserExt/BlaExt.lean b/tests/pkg/user_ext/UserExt/BlaExt.lean new file mode 100644 index 0000000000..5284117fe9 --- /dev/null +++ b/tests/pkg/user_ext/UserExt/BlaExt.lean @@ -0,0 +1,23 @@ +import Lean + +open Lean + +initialize blaExtension : SimplePersistentEnvExtension Name NameSet ← + registerSimplePersistentEnvExtension { + name := `blaExt + addEntryFn := NameSet.insert + addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es + } + +syntax (name := insertBla) "insert_bla " ident : command +syntax (name := showBla) "show_bla_set" : command + +open Lean.Elab +open Lean.Elab.Command + +@[commandElab insertBla] def elabInsertBla : CommandElab := fun stx => do + IO.println s!"inserting {stx[1].getId}" + modifyEnv fun env => blaExtension.addEntry env stx[1].getId + +@[commandElab showBla] def elabShowBla : CommandElab := fun stx => do + IO.println s!"bla set: {blaExtension.getState (← getEnv) |>.toList}" diff --git a/tests/pkg/user_ext/UserExt/FooExt.lean b/tests/pkg/user_ext/UserExt/FooExt.lean new file mode 100644 index 0000000000..686ec53f82 --- /dev/null +++ b/tests/pkg/user_ext/UserExt/FooExt.lean @@ -0,0 +1,26 @@ +import Lean + +open Lean + +initialize fooExtension : SimplePersistentEnvExtension Name NameSet ← + registerSimplePersistentEnvExtension { + name := `fooExt + addEntryFn := NameSet.insert + addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es + } + +initialize registerTraceClass `myDebug + +syntax (name := insertFoo) "insert_foo " ident : command +syntax (name := showFoo) "show_foo_set" : command + +open Lean.Elab +open Lean.Elab.Command + +@[commandElab insertFoo] def elabInsertFoo : CommandElab := fun stx => do + trace[myDebug] "testing trace message at insert foo '{stx}'" + IO.println s!"inserting {stx[1].getId}" + modifyEnv fun env => fooExtension.addEntry env stx[1].getId + +@[commandElab showFoo] def elabShowFoo : CommandElab := fun stx => do + IO.println s!"foo set: {fooExtension.getState (← getEnv) |>.toList}" diff --git a/tests/pkg/user_ext/UserExt/Tst1.lean b/tests/pkg/user_ext/UserExt/Tst1.lean new file mode 100644 index 0000000000..9c15cbfac2 --- /dev/null +++ b/tests/pkg/user_ext/UserExt/Tst1.lean @@ -0,0 +1,14 @@ +import UserExt.FooExt +import UserExt.BlaExt + +set_option trace.myDebug true + +insert_foo hello + +set_option trace.myDebug false + +insert_foo world +show_foo_set + +insert_bla abc +show_bla_set diff --git a/tests/pkg/user_ext/UserExt/Tst2.lean b/tests/pkg/user_ext/UserExt/Tst2.lean new file mode 100644 index 0000000000..c7743d2044 --- /dev/null +++ b/tests/pkg/user_ext/UserExt/Tst2.lean @@ -0,0 +1,6 @@ +import UserExt.BlaExt +import UserExt.FooExt + +insert_foo test +insert_bla defg +insert_bla hij diff --git a/tests/pkg/user_ext/lakefile.lean b/tests/pkg/user_ext/lakefile.lean new file mode 100644 index 0000000000..373656ab3a --- /dev/null +++ b/tests/pkg/user_ext/lakefile.lean @@ -0,0 +1,5 @@ +import Lake +open System Lake DSL + +package user_ext where + defaultFacet := PackageFacet.oleans diff --git a/tests/pkg/user_ext/test.sh b/tests/pkg/user_ext/test.sh new file mode 100755 index 0000000000..acb3c736d9 --- /dev/null +++ b/tests/pkg/user_ext/test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +rm -rf build +lake build 2>&1 | grep 'world, hello, test' diff --git a/tests/pkg/user_opt/UserOpt.lean b/tests/pkg/user_opt/UserOpt.lean new file mode 100644 index 0000000000..6a4ef2093c --- /dev/null +++ b/tests/pkg/user_opt/UserOpt.lean @@ -0,0 +1,20 @@ +import UserOpt.Opts + +open Lean + +def tst1 : MetaM Unit := do + assert! !(myBoolOpt.get (← getOptions)) + assert! myNatOpt.get (← getOptions) == 100 + pure () + +#eval tst1 + +set_option myBoolOpt true +set_option myNatOpt 4 + +def tst2 : MetaM Unit := do + assert! myBoolOpt.get (← getOptions) + assert! myNatOpt.get (← getOptions) == 4 + pure () + +#eval tst2 diff --git a/tests/pkg/user_opt/UserOpt/Opts.lean b/tests/pkg/user_opt/UserOpt/Opts.lean new file mode 100644 index 0000000000..9b656a13eb --- /dev/null +++ b/tests/pkg/user_opt/UserOpt/Opts.lean @@ -0,0 +1,11 @@ +import Lean + +register_option myBoolOpt : Bool := { + defValue := false + descr := "my Boolean option" +} + +register_option myNatOpt : Nat := { + defValue := 100 + descr := "my Nat option" +} diff --git a/tests/pkg/user_opt/lakefile.lean b/tests/pkg/user_opt/lakefile.lean new file mode 100644 index 0000000000..80b02f4c67 --- /dev/null +++ b/tests/pkg/user_opt/lakefile.lean @@ -0,0 +1,5 @@ +import Lake +open System Lake DSL + +package user_opt where + defaultFacet := PackageFacet.oleans diff --git a/tests/pkg/user_opt/test.sh b/tests/pkg/user_opt/test.sh new file mode 100755 index 0000000000..438bb1c522 --- /dev/null +++ b/tests/pkg/user_opt/test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +rm -rf build +lake build