Are reflection tests run?

[JacquesCarette]

For example, is this file actually used?

It appears that these lines

agda-stdlib/tests/reflection/assumption/Main.agda

Lines 54 to 58 in 94906c0

	asss ← getContext
	goal ← inferType hole
	debugPrint "" 10
	(strErr "Context : "
	∷ concatMap (λ where (_ , arg info ty) → strErr "\n " ∷ termErr ty ∷ []) asss)

are wrong and instead should be printed "in context" which concatMap doesn't do.

The original report (on the Univalent Agda Discord) was that this code

printTelescope : Telescope → TC ⊤
printTelescope [] = returnTC tt
printTelescope ((id , (arg info t)) ∷ ts) =
 do printTelescope ts
    debugPrint "" 1 (strErr id ∷ strErr " : " ∷ termErr t ∷ [])

didn't do the right thing, and should instead have the second case be

printTelescope ((id , (arg info t)) ∷ ts) =
 do printTelescope ts
    inContext ts do
      debugPrint "" 1 (strErr id ∷ strErr " : " ∷ termErr t ∷ [])

The relation is that (apparently) the author of printTelescope was copying out (and expanding) the code in that example.

I have never used any of the reflection stuff myself, so I'm just reporting. @gallais seems to be the author.

[gallais]

They are run, however without any logging so this debugging code is not printed.