[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: LOST PROOF FILES
I'd like to look into this problem immediately, but I need some means of
recreating the problem. Could you send a dump of your specification (use
M-x dump-pvs-files) and perhaps the scenario(s) that cause these problems?
> From: Victoria Chernyakhovsky <email@example.com>
> Subject: LOST PROOF FILES
> Date: Mon, 27 Apr 1998 14:22:04 EDT
> To: Sam Owre <firstname.lastname@example.org>, email@example.com
> We are fighting with a PVS bug in the PVS Version 2.1 (patch level
> 2.417). We would appreciate any help.
> We have a large specification with several theory files. All lemmas were
> proven correct with PVS 2.1 (patch2 version 2.414). If we rerun the
> proofs automatically we get 100% of the lemmas proven correct (after
> disabling the bin-files). However, if we introduce a change and want to
> reprove the lemmas in question, the system breaks.
> * In some cases, the prover was actually breaking and PVS had to be
> restarted. This serious problem was removed by applying more basic proof
> * Continuing with further proofs, the PVS environment seems to exhibit
> an inconsitant behavior. Independent of the completeness of a proof, the
> proof file is corrupted. In general only some of the proofs of the
> theory are stored in the prf-file.
> We are seeking for any kind of advice to overcome these problems. As we
> have updated our Emacs version to 20.2.1 we are basically restricted to
> patch level 2.417. However, if these problems can not be overcome we
> would appreciate to get a hold of the earlier version of PVS 2.1 (patch2
> version 2.414). As we are trying to overcome these problems for several
> weeks, we would appreciate immediate access to the previous version.
> Thank you for your help and we would be glad to receive any immediate
> Victoria Chernyakhovsky