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!
ProofGeneral-devel mailing list