You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I am writing some IDE automation over proof general and want to implement a blocking version of proof-goto-point, so that the automation can then execute query commands on an uptodate state. I tried the following but it sometimes returns early. What is the right way to do it?
(defun proof-goto-point-and-wait ()
(proof-goto-point)
(sleep-for 1) ;; even with this, on commands that sometimes take long time to process like `Require Import ...`, this function sometimes returns earlier, in a state where the side effects of processing until current point is not yet visible
(proof-shell-wait))
The text was updated successfully, but these errors were encountered:
proof-goto-point being non-blocking is a key feature of Proof General: Emacs stays responsive, while Coq is working in the background, which can easily take minutes.
In the automated tests we have a similar problem, there we use wait-for-coq or variants of it, see for instance ci/simple-tests/coq-test-prelude-correct.el.
Note that there is also a Proof General internal way to solve this problem. You can add specific flags or callbacks to action list items, see proof-shell-action-list-item in generic/proof-shell.el. Automatic background compilation and proof tree visualization use this to get notifications when certain commands have been completely processed.
I am writing some IDE automation over proof general and want to implement a blocking version of
proof-goto-point
, so that the automation can then execute query commands on an uptodate state. I tried the following but it sometimes returns early. What is the right way to do it?The text was updated successfully, but these errors were encountered: