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

Re: [PVS-Help] Undump complains about path to library

Hello Hanne,

I'm not sure I can resolve all your classroom diversity issues, but here are 
some suggestions for the path problem.  PVS will try to find Field and Manip 
in places where it searches for libraries.  If you don't have the environment 
variable PVS_LIBRARY_PATH set when PVS is started, it will look for library 
and strategy files in <path>/pvs/lib .  If everyone's setup has Manip and 
Field in pvs/lib, I believe it will work all right, but haven't tested it.

To leave fewer things to chance, you can use a setup that involves setting the 
environment variable.  I do it as part of a startup script:Hanne Gottliebsen 

#! /bin/bash
export PVS_LIBRARY_PATH=~/<lib-path>
<pvs-path>/pvs $@

(Note that PVS_LIBRARY_PATH is written with underscores, not hyphens.  Maybe 
the error message was misleading.)

As far as I know, this should get you working.



Ben Di Vito
1 South Wright Street, MS 130
NASA Langley Research Center
Hampton, VA 23681   USA

voice: +1-757-864-4883     fax: +1-757-864-4234


On Thursday 14 April 2005 05:53, Hanne Gottliebsen wrote:
>  have a bunch of student who have submitted PVS dump file sto me as
> coursework.
> 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/")
> Another:
> %% 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?