12. Shell Proof General
This instance of Proof General is not really for proof assistants at all, but simply provided as a handy way to use a degenerate form of script management with other tools.
Suppose you have a software tool of some kind with a command line interface, and you want to demonstrate several example uses of it, perhaps at a conference. But the command lines for your tool may be quite complicated, so you do not want to type them in live. Instead, you just want to cut and paste from a pre-recorded list. But watching somebody cut and paste commands into a window is almost as tedious as watching them type those commands!
Shell Proof General comes to the rescue. Simply record your commands in
a file with the extension .pgsh, and load up Proof General. Now
use the toolbar to send each line of the file to your tool, and have the
output displayed clearly in another window. Much easier and more
pleasant for your audience to watch!
If you wish, you may adjust the value of proof-prog-name in
‘pgshell.el’ to launch your program rather than the shell
interpreter.
We welcome feedback and suggestions concerning this subsidiary provision in Proof General. Please recommend it to your colleagues (e.g., the model checking crew).
This document was generated on April 18, 2024 using texi2html 1.82.