User Tools
pvs:commands
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
pvs:commands [2016/08/29 15:36] jonathan [Restarting PVS] |
pvs:commands [2017/09/06 19:33] (current) jonathan |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ~~NOTOC~~ | ||
| ====== PVS/Emacs Shortcuts ====== | ====== PVS/Emacs Shortcuts ====== | ||
| [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:pvs:shortcuts:start#keyboard_shortcuts|SEL wiki]] | [[https://wiki.eecs.yorku.ca/project/sel-students/p:tutorials:pvs:shortcuts:start#keyboard_shortcuts|SEL wiki]] | ||
| + | |||
| + | ====== Restarting PVS ====== | ||
| + | If you have a run-away prover command (e.g. GRIND), you can type | ||
| + | ''C-c C-c'' (while in the *pvs* buffer), which will drop you into Lisp. | ||
| + | At the <rcl> prompt, type (''restore'') to get back to the previous | ||
| + | sequent. | ||
| + | |||
| + | If PVS has lost its mind, type ''M-x reset-pvs''. Note. During garbage | ||
| + | collection, this command will not engage immediately. | ||
| + | |||
| + | See Survival-Tips.pdf | ||
| ====== Emacs shortcuts with PVS ====== | ====== Emacs shortcuts with PVS ====== | ||
| Line 25: | Line 35: | ||
| M-x show-proofs-theory -- Show all proofs of theory | M-x show-proofs-theory -- Show all proofs of theory | ||
| + | M-x x-show-current-proof -- show current proof under x11 | ||
| step-proof, prs (C-c C-p s) Start proof and set up for stepping | step-proof, prs (C-c C-p s) Start proof and set up for stepping | ||
| Line 94: | Line 105: | ||
| the formula numbered f in Hidden to the sequent.</strong><br> | the formula numbered f in Hidden to the sequent.</strong><br> | ||
| </p> | </p> | ||
| - | <table border="1" cellpadding="10" width="760"> | + | <table border="1" cellpadding="10" width="600"> |
| <tbody> | <tbody> | ||
| <tr> | <tr> | ||
| Line 250: | Line 261: | ||
| </html> | </html> | ||
| - | ====== Restarting PVS ====== | ||
| - | If you have a run-away prover command (e.g. GRIND), you can type | ||
| - | ''C-c C-c'' (while in the *pvs* buffer), which will drop you into Lisp. | ||
| - | At the <rcl> prompt, type (''restore'') to get back to the previous | ||
| - | sequent. | ||
| - | If PVS has lost its mind, type ''M-x reset-pvs''. Note. During garbage | ||
| - | collection, this command will not engage immediately. | ||
| - | |||
| - | See Survival-Tips.pdf | ||
| ====== Proof Rules ====== | ====== Proof Rules ====== | ||
pvs/commands.1472484992.txt.gz · Last modified: 2016/08/29 15:36 (external edit)
Page Tools
