Slow goal printing in Coq-HoTT theories/Spaces/No/Core.v

[Alizter]

In HoTT we have a file theories/Spaces/No/Core.v which has some goals that are slow to print. It would be good to investigate if we can speed these up. Specifically the local definition inner_package demonstrates the slow behaviour I have been observing.

[Alizter]

Testing this, pp_type 0 is much faster than 1 so it seems to be a printing issue.

[ejgallego]

Indeed, this is due to our printer doing DOM ops, thanks a lot for the example Ali, it is very useful.

Once we switch the printer from to a VDOM , we should be able to understand how things work.

Actually, (cc: @corwin-of-amber) I wonder if there could be some kind of drop-in replacement for jQuery that would operate on a VDom, rending on a final stage?

I proposed the vsCoq folks to help with this but they went their own route.