PVS‎ > ‎

Emacs

PVS runs under Emacs. PVS is just an Emacs augmented with PVS menus and commands, for dealing with theories and proofs:


This particular picture displays a split Emacs: the upper part is a theory buffer, hidden in part by PVS popup menus; the lower part is a proof buffer.
Theory management main commands
  • Ctrl-c Ctrl-f: prompts for the name of a theory (within current context) to be loaded and displayed in a name.pvs buffer; advice: the theory name does not include the .pvs suffix; never use Ctrl-x Ctrl-f pure Emacs command for this purpose, as it won't load the theory in the PVS sense;
  • Meta-x tc: type check current theory (and imported ones); many commands automatically trigger this one;
  • Meta-x show-tccs: show proof obligations (also called TCCs for Type Checking Conditions) for current theory, in a separate buffer;
  • PVS / Display Commands / x-theory-hierarchy (menu): lets you view a graphical representation of the current theory hierarchy, where the root is the theory in the current buffer;
  • Meta-x new-pvs-file: lets you create a new PVS theory with a given name (a file with same name and ".pvs" extension will automatically be generated and displayed in a buffer). Advice: do not put more than one theory in one ".pvs" file;
  • Meta-x view-prelude-file: lets you view all PVS prelude theories in one buffer;
  • Meta-x dump-pvs-files: lets you produce a dump from a root theory:
    • make sure that you have type checked the root theory before using this command (using Meta-x tc or better, Meta-x pri, from the root theory);
    • answer no to the question: "include libraries?",
    • use dmp.txt as suffix for the dump file;
    • see @ get started > About dumps and PVS directories for EIRBMMK convention on dump names,
    • visually check your dump after issuing the Meta-x dump-pvs-files command, to make sure it contains all your work, and not just the root theory, which happens without warning if you forgot to type check the root theory: an incomplete dump is useless;
  • Meta-x undump-pvs-files: lets you restore theories and proofs from a PVS dump.
Proof management main commands
  • Meta-x pr: start (or replay) a proof of the formula near the cursor;
  • Meta-x step-proof: replay an existing proof of formula next to cursor, step by step (<Tab>1 to go to next step;
  • Meta-x pri: try to prove all theories (current one, and imported theories), including TCCs, using existing proofs, or trying ad hoc strategies from untried formulas;
  • Meta-x show-proof: displays a lemma (or TCC) proof (cursor near this lemma or TCC) in the Proof buffer, so that you can either look at it, or edit it;
  • Ctrl-x Ctrl-s: attach the Proof buffer proof with the corresponding lemma (useful when you have - carefully!- edited the proof buffer by hand;
  • Ctrl-c Ctrl-i: attach the Proof buffer proof with some other lemma (cursor near this lemma);
  • Meta-x revert-proof: restore previous proof;
  • Meta-x show-orphaned-proofs: displays a buffer of lost proofs:
    • type s near the name of a lemma to display the orphan proof in the Proof buffer;
    • type d near the lemma name to delete this orphan proof;
  • PVS / Display Commands / x-show-current-proof menu: while performing a proof, lets you see a graphical representation of the current proof tree;
  • (undo) proof command: during a proof, undoes the effect of the last proof command, moving back to previous sequent;
  • (quit) proof command: lets you save and quit a partial proof under construction; you are advised to often quit your proof, as it automatically saves it in the relevant .prf file, and it takes no time going back to the same proof sequent using Meta-x pr.
What if ...?
Students or beginners are very good at pin pointing PVS flaws or bugs:

What to do if PVS crashes in the middle of a proof?

  • Type (restore) when prompted: this will take you back to the sequent before the proof command that triggered the crash, see example below:
  • Warning: Rewriting depth = 2950; Rewriting with ev_implies_eveni? 
  • Error: Stack overflow (signal 1000) 
  •   [condition type: SYNCHRONOUS-OPERATING-SYSTEM-SIGNAL] Restart actions (select using :continue):
     0: continue computation
     1: Return to Top Level (an "abort" restart)
    [1c] PVS(101): (restore)
    ev?_equals_eveni? :
      |-------
    [1]   ev? = eveni?
     
    Rule?

What to do if your PVS context is no longer coherent?

  1. Get out of PVS as cleanly as possible (so as not to loose theories or proofs) if you are running PVS;
  2. Remove .pvscontext file and *.bin files from your directory (or bin sub-directory):
    • rm .pvscontext
    • cd bin               # this is necessary for recent PVS versions
    • rm *.bin
  3. Restart PVS;
  4. Reconstruct your PVS library by doing Meta-x pri from the root theory.
Remark: if your context (library) relies upon other libraries, you may have to
  • cleanly quit all your PVS sessions;
  • perform 1--4 above steps, for each related library, bottom up (that is, starting with the libraries that do not rely upon any other library), cleanly exiting PVS after reconstruction of this library.
Note: PVS does not like you to work on a library A that relies upon a library B on which you have a PVS session running; PVS will think you are trying to cheat, by modifying B while working on A, and thus punish you by flagging all your proven formulas in A by “Proved Incomplete”. In other words, never simultaneously run PVS on two contexts A and B such that A depends upon B: if you need to modify B library, make sure you first exit PVS from A context.

My PVS dump does not include imported theories: what can I do?

  • Always do a type-checking from the root theory before using the Meta-x dump-pvs-files command.

How to switch to a different context without quitting PVS?

Although this is not really advisable, as it is often cleaner and reasonably fast to exit PVS and restart it from a different context, it is technically possible to do the switch without leaving PVS:

  • Meta-x change-context: lets you leave the current context and move to a different context (directory) of your choice.
    Abbreviation: Meta-x cc .
Remark: switching contexts using the above command has some drawbacks:
  • buffers associated with the previous context (theories, TCCs, ...) are still there, though inactive, and this may be confusing: you may want to kill all such buffers before switching to the new context;
  • if you exit PVS after the switch from A to B context, you are still in A directory.
Comments