Meven Lennon-Bertrand (Jun 25 2021 at 12:31): Meven Lennon-Bertrand (Jun 25 2021 at 12:31):Hi!
I am having regular freezes/crashes of VsCoq on one of my files, to the point where it becomes difficult to develop it. I’m really not sure what the problem is (nor if this is really a VsCoq problem), but calling coqc from the terminal on the same file does not seem to trigger the same issue.
The faulty file is the following : https://github.com/MevenBertrand/metacoq/blob/case-representation-bidir/pcuic/theories/bidirectional/BDStrengthening.v . The problem triggers when I step directly to an advanced point in the file. VsCoq seems to choke on some uses of lia, and either crashes or freezes my computer to the point where I have to kill the process to regain control – in some cases the only way to do this is to shut down. This does not trigger when working on other files (for instance the ones in the same folder) that I would say have similar lengths and features (including uses of lia). Also, stepping down slowly through the file seems to mitigate the error, although it is not always enough.
Does this ring a bell to anyone? How could I debug this to at least pinpoint what is responsible for the problem and report a meaningful issue?
Thanks!
Matthieu Sozeau (Jun 25 2021 at 14:19):I don't see anything unusual except maybe the many Lets
Last updated: Jun 04 2023 at 23:30 UTC