"printer interrupted" in goal window

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq

GNU Lesser General Public License v2.1

143 stars 31 forks source link

"printer interrupted" in goal window #806

Open Alizter opened 1 month ago

Alizter commented 1 month ago

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

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

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

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

By the way the files in question are currently in this PR: https://github.com/HoTT/Coq-HoTT/pull/2021

ejgallego commented 1 month ago

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)