test: add registerTraceClass test

leanprover · Sep 16, 2021 · a29e81b · a29e81b
1 parent d32b4ff
commit a29e81b
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/tests/leanpkg/user_ext/UserExt/FooExt.lean b/tests/leanpkg/user_ext/UserExt/FooExt.lean
@@ -9,13 +9,16 @@ initialize fooExtension : SimplePersistentEnvExtension Name NameSet ←
     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
 

diff --git a/tests/leanpkg/user_ext/UserExt/Tst1.lean b/tests/leanpkg/user_ext/UserExt/Tst1.lean
@@ -1,7 +1,12 @@
 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