From 9c97972a2e94fc01c34f67848c5634a8864b142a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 9 Nov 1998 18:50:23 +0000 Subject: Added proof-rsh-command to help complete documentation (was allocated to tms but he said he wouldn't get around to it) --- doc/NewDoc.texi | 26 +++++++++++------- generic/proof-config.el | 70 +++++++++++++++++++++++++++++++------------------ generic/proof-shell.el | 6 ++++- todo | 3 --- 4 files changed, 66 insertions(+), 39 deletions(-) diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi index 7f5a8c4d..a8c18e31 100644 --- a/doc/NewDoc.texi +++ b/doc/NewDoc.texi @@ -794,7 +794,9 @@ For more help, see @inforef{Easy Customization, ,xemacs}. @cindex{Toolbar follow mode} @cindex{Toolbar disabling} @cindex{Proof script indentation} -@cindex{indentation} +@cindex{Indentation} +@cindex{Remote shell} +@cindex{Running proof assistant remotely} @c @cindex{formatting proof script} @@ -890,19 +892,25 @@ The configuration settings appear in the customization group Proof-General -> Internals -> Prover Config @end lisp -Some examples of settings you may like to tweak are: +One basic example of a setting you may like to tweak is: -proof-assistant-home-page +@defvar proof-assistant-home-page +Web address for information on proof assistant. +@end var - -More details of the settings are given in @xref{Adapting Proof General -to New Provers}. +Most of the others are more complicated. More details of the settings +are given in @xref{Adapting Proof General to New Provers}. To browse +them, you can look through the customization groups +@code{prover-config}, @code{proof-script} and @code{proof-shell}. The +group @code{proof-script} contains the configuration variables for +scripting, and the group @code{proof-shell} contains those for +interacting with the proof assistant. Unfortunately, although you can use the customization mechanism to set and save these variables, saving them may have no effect because the -default settings are mostly hard-wired into the proof assistant code. -@c FIXME: this is a problem, code does need fixing. -At present there is no easy way to get around this. +default settings are often hard-wired into the proof assistant code. At +present there is no easy way to get around this other than by editing +the source code. Please contact us if this proves to be a problem. @node LEGO Proof General diff --git a/generic/proof-config.el b/generic/proof-config.el index c047f342..5a5bc089 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -64,11 +64,6 @@ :type 'boolean :group 'proof-general) -(defcustom proof-one-command-per-line nil - "*If non-nil, format for newlines after each proof command in a script." - :type 'boolean - :group 'proof-general) - (and (featurep 'toolbar) (defcustom proof-toolbar-wanted t "*Whether to use toolbar in proof mode." @@ -112,11 +107,32 @@ you a reprimand!)" ;; confident about it. (I don't). -da "If non-nil, enable indentation code for proof scripts. Currently the indentation code can be rather slow for large scripts, -or may be critical on the setting of regular expressions for -particular provers." +and is critical on the setting of regular expressions for particular +provers. Enable it if it works for you." + :type 'boolean + :group 'proof-general) + +(defcustom proof-one-command-per-line nil + "*If non-nil, format for newlines after each proof command in a script. +This option is not fully-functional at the moment." :type 'boolean :group 'proof-general) +(defcustom proof-rsh-command "" + "Shell command prefix to run a command on a remote host. +For example, + + ssh bigjobs + +Would cause Proof General to issue the command 'ssh bigjobs isabelle' +to start Isabelle remotely on our large compute server called 'bigjobs'. + +The protocol used should be configured so that no user interaction +(passwords, or whatever) is required to get going." + :type 'string + :group 'proof-general) + + ;; ;; Faces. ;; We ought to test that these work sensibly: @@ -424,25 +440,27 @@ to `nil' of the proof assistant does not support nested goals." :type 'function :group 'proof-script) -(defcustom proof-atomic-sequence-lists nil - "list of instructions for setting up atomic sequences of commands (ACS). - -Each instruction is -a list of the form `(END START &optional FORGET-COMMAND)'. END is a -regular expression to recognise the last command in an ACS. START -is a function. Its input is the last command of an ACS. Its output -is a regular exression to recognise the first command of the ACS. -It is evaluated once and the output is successively matched agains -previously processed commands until a match occurs (or the -beginning of the current buffer is reached). The region determined -by (START,END) is locked as an ACS. Optionally, the ACS is -annotated with the actual command to retract the ACS. This is -computed by applying FORGET-COMMAND to the first and last command -of the ACS." - ;; FIXME customize broken on choices with function in them? - ;;:type '(repeat (cons regexp function (choice (const nil) function))) - :type '(repeat (cons regexp function function)) - :group 'proof-shell) +; Not yet implemented. +; +;(defcustom proof-atomic-sequence-lists nil +; "list of instructions for setting up atomic sequences of commands (ACS). + +;Each instruction is +;a list of the form `(END START &optional FORGET-COMMAND)'. END is a +;regular expression to recognise the last command in an ACS. START +;is a function. Its input is the last command of an ACS. Its output +;is a regular exression to recognise the first command of the ACS. +;It is evaluated once and the output is successively matched agains +;previously processed commands until a match occurs (or the +;beginning of the current buffer is reached). The region determined +;by (START,END) is locked as an ACS. Optionally, the ACS is +;annotated with the actual command to retract the ACS. This is +;computed by applying FORGET-COMMAND to the first and last command +;of the ACS." +; ;; FIXME customize broken on choices with function in them? +; ;;:type '(repeat (cons regexp function (choice (const nil) function))) +; :type '(repeat (cons regexp function function)) +; :group 'proof-shell) (defconst proof-no-command "COMMENT" diff --git a/generic/proof-shell.el b/generic/proof-shell.el index d3bc5bc0..78e60a7c 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -192,7 +192,11 @@ Does nothing if proof assistant is already running." (message (format "Starting %s process..." proc)) ;; Starting the inferior process (asynchronous) - (let ((prog-name-list (proof-string-to-list proof-prog-name " "))) + (let ((prog-name-list (proof-string-to-list + (concat + proof-rsh-command + " " + proof-prog-name) " "))) (apply 'make-comint (append (list proc (car prog-name-list) nil) (cdr prog-name-list)))) ;; To send any initialisation commands to the inferior process, diff --git a/todo b/todo index 2646ce38..0a8c3076 100644 --- a/todo +++ b/todo @@ -149,9 +149,6 @@ C proof-find-next-terminator doesn't work properly: bug. Perhaps just use new implementation of proof-assert-until-point (30min) -B Add proof-rsh-command and note in documentation about how to - use widely-advertised "remote shell" feature. (1hr tms) - B Add proof-quit-command: some provers may like a quit command to be sent to the shell, not just EOF ! (see proof-stop-shell). Also reconcile proof-restart-script and proof-stop-shell, see -- cgit v1.2.3