!4#3361

Stream: PR reviews

[Jujian Zhang]

!4#3361 (porting PiTensorProduct) causes a bors build error at line 317 due to a notation error

Could not generate matchers for a delaborator, so notation will not be pretty printed. Consider either adjusting the expansions or use `notation3 (prettyPrint := false)`.

I don't anything about notations and/or metaprogrammings, so I have marked this PR with help-wanted to see if anybody understands notation can fix this issue

[Patrick Massot]

This is clearly coming from 4!#4533.

[Patrick Massot]

You can indeed disable generating the pretty printer while @Kyle Miller is flying if you want to be able to move forward.

[Mario Carneiro]

use pretty_print := false, what's the declaration look like?

[Jujian Zhang]

It looks like this

notation3:100"⨂ₜ["R"] "(...)", "r:(scoped f => tprod R f) => r

[Kyle Miller]

Could you do set_option trace.notation3 true? It should hopefully say why it failed to make a pretty printer. Does tprod take two arguments? Or does it depend on a coercion? If it does, as a workaround you can write the term including the coercion function to help it out (and it doesn't support dot notation yet; it can only analyze basic function applications)

[Jujian Zhang]

I think I am doing something wrong, set_option trace.notation3 true gives an error: unknown option 'trace.notation3'

tprod indeed takes one argument and returns a multilinear map, its type signature is

PiTensorProduct.tprod.{u_1, u_2, u_3} {ι : Type u_1} (R : Type u_2) [inst✝ : CommSemiring R] {s : ι → Type u_3}
  [inst✝¹ : (i : ι) → AddCommMonoid (s i)] [inst✝² : (i : ι) → Module R (s i)] :
  MultilinearMap R s (PiTensorProduct R fun i ↦ s i)

so tprod R f is ↑(tprod R) f

[Kyle Miller]

@Jujian Zhang Ah, yeah, you need to merge master to get the trace.notation3 option locally. I did that and adjusted the notation3 command and hopefully when it rebuilds the warning goes away.

[Kyle Miller]

Documenting this in case it comes up again, to get notation3 to generate a pretty printer I changed

notation3:100 "⨂ₜ["R"] "(...)", "r:(scoped f => tprod R f) => r

to

notation3:100 "⨂ₜ["R"] "(...)", "r:(scoped f => FunLike.coe (tprod R) f) => r

since this is specifically what ↑(tprod R) f is. At least for now, the pretty printer generator is pretty simple and doesn't know how to undo coercions.