Murali Vijayaraghavan

Debugging slow proofgeneral issues for Coq

1

I am wondering if there's a way to debug proofgeneral on Coq. Proofgeneral's response time slows down considerably even when I am viewing proof state and simply typing my code....

Future enhancement: distinct call (forward) & return (backward) sentries, and distinct call & return jumps

3

Let me preface by saying that this doesn't require any changes to the base spec and instead I am proposing this as a potential future extension to enforce stronger CFI...