[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] .pvs.lisp for multiple PVS versions


what is the right way to organize different patch sets for
different PVS versions?

Long explanation:
I am adopting an old specification, therefore I would like to run
both PVS 3.2 and PVS 3.1. For both versions I need to use some

In a first attempt I organized my .pvs.lisp as follows:

    #+(and pvs3.2 redhat6)  ;; redhat6 distinguishes PVS 3.3

    ;; patches for 3.2



    ;; patches for 3.1


This obviously fails because the reader macros "#+..." are not
present in the compiled .lfasl file.

My next version looked like 

    (if (and (member :pvs3.2 *features*)
	     (member :redhat6 *features*))

    ;; 3.2 patches


    (if (and (not (member :pvs3.2 *features*)) 
	     (member :redhat6 *features*))

    ;; 3.1 patches


This fails to compile under 3.1, because the arity of the
put-decl macro changed. Worse yet, an .pvs.lfasl compiled under
3.2 causes PVS 3.1 to crash with 

    Error: attempt to call `get-lhash' which is an undefined function.

Now I can imagine only the following solutions:

1. patch fun user-pvs-lisp-file to use a version specific file.
   But how to do that before the patch file is loaded?

2. run something like "while true; do rm -f .pvs.lfasl; done"

3. use links for .pvs.lisp and .pvs.lfasl and move these links in
   the pvs startup script.

Does anybody have some other suggestions?