Manip: A Strategy Package for PVS

Current status:

• (3 Dec 2007) Work on Manip 1.2 has been completed. It is now capable of working with either the Allegro or CMU Lisp variants of PVS 4.1. Manip 1.2 (final) is now the current stable version. Users of the beta version of Manip 1.2 should upgrade to the final version.
• (28 Nov 2005) The beta release of Manip 1.2 adds a major new feature set based on syntax matching, allowing users to identify terms in a sequent using patterns expressed as parseable PVS text with embedded pattern variables. Other improvements in Manip are minor, such as a few new strategies for specialized tasks.
• The 1.1 release of Manip (18 Feb 2003) has been superseded.

Package files:

• Current version: 1.2, released 20 November 2007
• Requires: PVS 3.1 or higher (Allegro); PVS 4.1 (CMU Lisp)
• Installation, history: README (also see notes below)
• Documentation (PDF): User's manual (new material in Section 7, p. 34)
• Download (tar.gz): Manip package (includes manual)

Version 1.1:

• Version 1.1, released on 18 February 2003
• Requires: PVS 3.1 or 3.2
• Download (tar.gz): Manip package (includes manual)

Other documentation:

• Technical report, April 2002 (PDF): NASA/TM-2002-211647
(contains most of the version 1.1 user's manual plus additional material on package design considerations along with several proof examples)

Version 1.0:

• Version 1.0, released on 15 February 2002
• Requires: PVS 2.3 or 2.4
• Download (tar.gz): Manip package (includes manual)

Other items of interest:

• César Muñoz's Field package
• NASA Langley's PVS libraries page
• SRI's PVS home page

Note: The tag identifies links that are outside of the NASA domain.

Installation notes:

• (3 Dec 2007; version 1.2) To try out version 1.2 without affecting your working PVS environment, we suggest the following. Unpack the distribution in a test directory (e.g., ~/test) and create a symbolic link for the name Manip:

    cd ~/test
    tar -xvfz tar-path/Manip-1.2.tgz
    ln -s Manip-1.2 Manip
  

  Then create a PVS start-up script in your ~/bin directory, e.g., with the name pvs-manip-1.2. Here is a sample that works for the bash shell:

    #! /bin/bash
    # Run PVS with Manip 1.2 overriding Manip 1.1
    export PVS_LIBRARY_PATH=~/test:other-PVS-library-paths
    path-to-pvs/pvs $@
  

  Now you can fire up PVS using this script and try the new Manip 1.2 features. It would be best to do so in a new directory to avoiding disturbing your current PVS contexts. Making a fresh copy of an active PVS working directory is a good way to establish a test environment.
• (18 Feb 2003; version 1.1) The 1.1 release of Manip is designed to work with PVS 3.1 (14 Feb 2003). The previous 1.0 release of Manip will not work with PVS 3.1, and the new Manip 1.1 will not work with PVS 2.3/2.4. Users of 2.3/2.4 should use Manip 1.0. PVS 3.0 was short-lived and will not be supported. Version 1.1 exploits the new library enhancements in PVS. These features make it easier to access Manip and similar packages such as Field. Other improvements in Manip are minor, such as better error checking. The strategy set and user interfaces have not changed.
• (20 Mar 2002; version 1.0 only) The README file advises adding the following lines to your pvs-strategies file:

    (load (pvs-emacs-eval "(concat pvs-prover-manip-dir
                                   \"manip-strategies\")"))
  

  Splitting the text string across two lines in this manner can cause problems during startup. It would be better to place this all on a single line of text or perform the split as follows:

    (load (pvs-emacs-eval
            "(concat pvs-prover-manip-dir \"manip-strategies\")"))