search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
134 stars 31 forks source link

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

Open Alizter opened 1 week ago

Alizter commented 1 week ago

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 commented 1 week ago

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

ejgallego commented 1 week ago

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.