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

Re: [PVS-Help] PVS4.0-cmu: Problem loading patches

Hi Mariano,

I found out about this problem when I tried to send somebody
some patches, and they had exactly your problem.
Unfortunately, I tested PVS 4.0 without a ~/.pvs.lisp file on
purpose, to make sure I wasn't accidentally testing the wrong

It turns out that Allegro handles the "~" correctly, and
expands it to the users home directory, but CMU Lisp treats it
as just another file character, and hence decides the
~/.pvs.lisp file doesn't exist.

Probably the easiest workaround for now is to add the following
to your ~/.pvsemacs file (which is read by Emacs after PVS
starts up):

(pvs-send-and-wait "#+cmu (load \"/home/mmoscato/.pvs.lisp\")")

Obviously, you should change this to your actual home

When I release the next version, you will be able to remove
this line (or the entire .pvsemacs file).


Mariano M. Moscato <mmoscato@gmail.com> wrote:

> Hi,
> I'm trying to migrate my work on PVS3.2 to PVS4.0-cmu.
> I have some patches that include in the file ~/.pvs.lisp. When I run
> PVS, it seems to ignore that patches.
> For testing purposes I only kept this line in ~/.pvs.lisp:
> (setq dummy-var "hello")
> When I run PVS4.0-allegro, I can (for example) print the value of this
> variable ("dummy-var"). But when I run PVS4.0-cmu, the variable isn't
> initialized.
> Will it be that PVS is not loading my patches?
> Has anyone had problems of this kind?
> Thanks in advance.
> Best regards.
> Mariano M. Moscato.