Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Optional timeout warning when waiting for the proof shell #516

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
Open

Optional timeout warning when waiting for the proof shell #516

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
1f2120a
Add proof-shell-timeout-warn variables (see #514)
andyqhan Oct 12, 2020
99cd00c
Add shell-internal variable for timer (see #514)
andyqhan Oct 12, 2020
d8d6104
Implement timeout message (see #514)
andyqhan Oct 12, 2020
ebea62f
fix parentheses
andyqhan Oct 12, 2020
3ab6159
fix empty goals bug because of previous commit
andyqhan Oct 12, 2020
9a38852
change timer config to one variable
andyqhan Oct 12, 2020
f8c0c09
Change warning text to clarify C-c C-c vs C-c C-x
andyqhan Oct 13, 2020
11d8c59
cancel timer in the case of error or interrupt
andyqhan Oct 14, 2020
ae1b766
implement matafou's suggestions
Mar 21, 2021
989ef2e
Merge branch 'master' of https://github.com/ProofGeneral/PG
Mar 21, 2021
debe754
more fixes… seems to work lol
Mar 28, 2021
1cc7e70
arm timer every command, not every region
Apr 3, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions generic/proof-config.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1464,7 +1464,15 @@ outside of any proof.
:type 'function
:group 'proof-script)

(defcustom proof-shell-timeout-warn 30
"How many seconds (integer) to wait before PG warns us that
a command is taking a long time and might be malformed.

nil disables the timeout timer.

Default value is 30 (seconds)."
:type 'integer
:group 'proof-shell)

;;
;; 3c. tokens mode: turning on/off tokens output
Expand Down
32 changes: 30 additions & 2 deletions generic/proof-shell.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,6 +149,13 @@ This flag is set for the duration of `proof-shell-kill-function'
to tell hooks in `proof-deactivate-scripting-hook' to refrain
from calling `proof-shell-exit'.")

(defvar proof-shell-timer nil
"A timer that alerts the user when the current command sent to the
shell is taking too long and might be malformed. This is cancelled
in `proof-shell-exec-loop' or if there was an error and armed when
the next command is sent to the process.
Disable by setting `proof-shell-timeout-warn' to nil. Configure by
setting `proof-shell-timeout-warn' to an integer.")


;;
Expand Down Expand Up @@ -738,6 +745,11 @@ unless the FLAGS for the command are non-nil (see `proof-action-list')."
;; proof-action-list is empty on error.
(setq proof-action-list nil)
(proof-release-lock)
(unless proof-shell-busy
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not sure this test is necessary. Why would the shell be busy if an error is detected? Probably not harmful.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I left it in, but can remove if you'd like.

;; if the shell isn't still busy, cancel timer on error
(if (and proof-shell-timer proof-shell-timeout-warn)
(progn (cancel-timer proof-shell-timer)
(setq proof-shell-timer nil))))
(unless flags
;; Give a hint about C-c C-`. (NB: approximate test)
(if (pg-response-has-error-location)
Expand Down Expand Up @@ -916,6 +928,19 @@ used in `proof-add-to-queue' when we start processing a queue, and in
;; Replace CRs from string with spaces to avoid spurious prompts.
(if proof-shell-strip-crs-from-input
(setq string (subst-char-in-string ?\n ?\ string)))
;; arm the timer if we've received a user command (callback is proof-done-advancing)
(when (and (eq 'proof-done-advancing action)
proof-shell-timeout-warn)
(when proof-shell-timer
;; cancel previous timer, if it exists
(cancel-timer proof-shell-timer)
(setq proof-shell-timer nil))
(setq proof-shell-timer
(run-with-timer proof-shell-timeout-warn nil
'message
(substitute-command-keys "This command is taking a while. \
Is the syntax correct? Do \\[proof-interrupt-process] to interrupt prover or
\\[proof-shell-exit] to terminate it."))))

(insert string)

Expand Down Expand Up @@ -1020,7 +1045,6 @@ being processed."
"proof-append-alist: wrong queuemode detected for busy shell")
(cl-assert (eq proof-shell-busy queuemode)))))


(let ((nothingthere (null proof-action-list)))
;; Now extend or start the queue.
(setq proof-action-list
Expand Down Expand Up @@ -1188,7 +1212,11 @@ contains only invisible elements for Prooftree synchronization."
(proof-detach-queue)
(unless flags ; hint after a batch of scripting
(pg-processing-complete-hint))
(pg-finish-tracing-display))
(pg-finish-tracing-display)
(when (and proof-shell-timeout-warn proof-shell-timer)
;; cancel timer if there's nothing in the action lists
(progn (cancel-timer proof-shell-timer)
(setq proof-shell-timer nil))))

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The indentation seems wrong here. Would it be possible to fix that?

(and (not proof-second-action-list-active)
(let ((last-command (car (nth 1 (car (last proof-action-list))))))
Expand Down