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

Reply via email to