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

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 10 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
14 changes: 13 additions & 1 deletion generic/proof-script.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2011,7 +2011,19 @@ This function expects the buffer to be activated for advancing."
(lastpos (nth 2 (car semis)))
(vanillas (proof-semis-to-vanillas semis displayflags)))
(proof-script-delete-secondary-spans startpos lastpos)
(proof-extend-queue lastpos vanillas)))
(proof-extend-queue lastpos vanillas))

;; arm the timeout timer
;; cancelled 1. in `proof-shell-exec-loop' unless `proof-shell-busy' or
;; 2. in the case of error, in `proof-shell-error-or-interrupt-action'
(if (and proof-shell-timeout-warn
(not (eq (caar semis) 'comment)))
(setq proof-shell-timer
(run-with-timer proof-shell-timeout-warn nil
'message
(substitute-command-keys "This command is taking a while. \
Is it malformed? Do \\[proof-interrupt-process] to interrupt prover or
\\[proof-shell-exit] to terminate it.")))))

(defun proof-retract-before-change (beg end)
"For `before-change-functions'. Retract to BEG unless BEG and END in comment.
Expand Down
18 changes: 18 additions & 0 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 @@ -1190,6 +1202,12 @@ contains only invisible elements for Prooftree synchronization."
(pg-processing-complete-hint))
(pg-finish-tracing-display))

(unless proof-shell-busy
;; if the shell isn't still busy, cancel timer
(if (and proof-shell-timer proof-shell-timeout-warn)
(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))))))
(or (null proof-action-list)
Expand Down