test: reimplement package tests using Lake

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

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.*")

tests/pkg/.gitignore

@@ -0,0 +1 @@
+build/

tests/pkg/builtin_attr/UserAttr.lean

@@ -0,0 +1 @@
+import UserAttr.Tst

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

tests/pkg/builtin_attr/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package user_attr where
+  defaultFacet := PackageFacet.oleans

tests/pkg/builtin_attr/test.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf build
+lake build

tests/pkg/deriving/UserDeriving.lean

@@ -0,0 +1 @@
+import UserDeriving.Tst

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

tests/pkg/deriving/UserDeriving/Tst.lean

@@ -0,0 +1,6 @@
+import UserDeriving.Simple
+
+inductive Foo where
+  | mk₁
+  | mk₂
+  deriving Simple

tests/pkg/deriving/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package user_deriving where
+  defaultFacet := PackageFacet.oleans

tests/pkg/deriving/test.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf build
+lake build

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

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

tests/pkg/prv/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package prv where
+  defaultFacet := PackageFacet.oleans

tests/pkg/prv/test.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf build
+lake build 2>&1 | grep 'error: field.*private'

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

tests/pkg/user_attr/UserAttr/BlaAttr.lean

@@ -0,0 +1,5 @@
+import Lean
+
+open Lean
+
+initialize blaAttr : TagAttribute ← registerTagAttribute `bla "simple user defined attribute"

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

tests/pkg/user_attr/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package user_attr where
+  defaultFacet := PackageFacet.oleans

tests/pkg/user_attr/test.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf build
+lake build

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 ()

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"

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

tests/pkg/user_attr_app/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package user_attr where
+  supportInterpreter := true

tests/pkg/user_attr_app/test.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf build
+lake build && ./build/bin/user_attr

tests/pkg/user_ext/UserExt.lean

@@ -0,0 +1,5 @@
+import UserExt.Tst1
+import UserExt.Tst2
+
+show_foo_set
+show_bla_set

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}"

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}"

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

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

tests/pkg/user_ext/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package user_ext where
+  defaultFacet := PackageFacet.oleans

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'

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

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"
+}

tests/pkg/user_opt/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package user_opt where
+  defaultFacet := PackageFacet.oleans

tests/pkg/user_opt/test.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+rm -rf build
+lake build