"printer interrupted" in goal window

[Alizter]

When working on heavy terms such as those found in Coq-HoTT's theories/Algebra/AbGroups/TensorProduct.v the coq-lsp printer gets interrupted a lot leading to such scenes:

Not sure what is better to do here.

[ejgallego]

I guess the current workaround is just to wait for the printer to finish printing. The printer will be only interrupted if the client does a new request.

Possible strategies to mitigate this could be:

• make Coq printing less expensive
• using OCaml 5.3 we could finally put printing in its own domain, so no more interrupting needed!
• we could disable interruptions for printing, however that means that coq-lsp can get stuck with a large term and users won't be able to interrupt it

[ejgallego]

make Coq printing less expensive

We don't track stats for printing precisely yet, do you know how long do these terms take to print?

Likely it is worth submitting a kind: performance bug to Coq itself, I think there are many super-linear behaviors on Coq printing as of today that could be affecting you.

[Alizter]

We don't track stats for printing precisely yet, do you know how long do these terms take to print?

They can vary wildly. Some of the terms in the file I mentioned have terms that take 16GB of ram to print and can take 10 minutes or so. I am currently trying to improve performance in this file, but I don't have a lot of understanding why Coq is taking so long. The terms mostly consist of projections of chunky terms. If I manually unfold then I can get an efficient print, but Coq's simpl or cbn gets stuck trying to unfold useless stuff.

[Alizter]

By the way the files in question are currently in this PR: HoTT/Coq-HoTT#2021

[ejgallego]

We don't track stats for printing precisely yet, do you know how long do these terms take to print?

They can vary wildly. Some of the terms in the file I mentioned have terms that take 16GB of ram to print and can take 10 minutes or so. I am currently trying to improve performance in this file, but I don't have a lot of understanding why Coq is taking so long.

Likely many super-linear (like O(n^3) or even worse) factors in printing. Just with the info you posted you can open an upstream bug and hope Coq devs have a look into it (I think they will).

This has been a problem for a long time and you can find bugs about slow printing in the bug tracker (and people complaining when we made printing non-interruptible due to this)