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

[PVS-Help] Undump complains about path to library

I have a bunch of student who have submitted PVS dump file sto me as 

It is quite plausible that despite me trying to be clear about it, they 
all have different setups, some may be running PVs at home too.

I'm running on yet another setup (we're on different servers for a 
start, and my PVS instalation is local).

When I try to undump the files, in some cases PVS complains that

Library directory Field/ not found - check your PVS-LIBRARY-PATH

In the top of the .dmp files there is a list of commands like 
load-prelude-library issued. The paths here are all different from what 
I use.

One student may have:
%% PVS Version 3.2
%% 6.2 [Linux (x86)] (Nov 3, 2004 23:30)
(load-prelude-library "Field/")
(load-prelude-library "Manip/")

%% PVS Version 3.2
%% 6.2 [Linux (x86)] (Nov 3, 2004 23:30)
(load-prelude-library "/import/linux/pvs/lib/Field/")

The latter works for me, the first one does not. Do I need to manually 
edit those .dmp files to get this to work?

Or should I be setting my library path to my version of pvs/lib?

Dr. Hanne Gottliebsen    Department of Computer Science
hago@dcs.qmul.ac.uk      Queen Mary, University of London
Ph: +44 (0) 207 882 5259
   - I want a single-skin cotton tent like Mr Weasley's