Hi, I just committed a fix for the bug that was described in coq/ex/test-cases/stale-load-path/README. As discussed before here, the fix calls proof-shell-exit in the deactivation-hook.
There are two problems: 1. When asserting in a buffer different from the active scripting buffer, then, as a result of killing the proof shell also the assert is undone. This is obviously something that we should fix before release. 2. I am not an expert in big coq projects. I just looked at compcert. But there a global load path is used, that is the same for all files. From this evidence I believe it would be beneficial to have an optimization that skips proof-shell-exit if the load path in the old and new buffer is equal. And now the problem is that I don't see a clean way to access the load path of the old and the new buffer inside the deactivation hook. Suggestions are welcome! Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
