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

[PVS-Help] Patch from November fails on nasalib theories



Hi all,

When using the last patch I received (patch-20141114.lisp), using ./prove-all from the nasalib directory fails.

Attachment: patch-20141114.lisp
Description: Binary data


Here’s the first bit of the output:
Processing nasalib.all
Removing binary files from library
ints                     [OK: Cleaning]
structures               [OK: Cleaning]
reals                    [OK: Cleaning]
orders                   [OK: Cleaning]
… [clipped for brevity] …
lebesgue                 [OK: Cleaning]
probability              [OK: Cleaning]
Processing nasalib.all. Output in ./nasalib.summaries
PVS_LIBRARY_PATH=/Users/Dependable/Tools/pvs/nasalib
ints                     [OK: 363 proofs]
structures               [FAIL: Proving]
reals                    [FAIL: Proving]
orders                   [OK: 722 proofs]
trig                     [OK: 597 proofs]
analysis                 [OK: 1523 proofs]
sets_aux                 [OK: 361 proofs]
numbers                  [FAIL: Proving]
lnexp                    [OK: 238 proofs]
vectors                  [FAIL: Proving]
series                   [OK: 301 proofs]
algebra                  [OK: 452 proofs]
vect_analysis            [OK: 557 proofs]

My work around for this is to temporarily disable the patch, run ./prove-all, then restore the patch, but I thought I’d let y’all know about the problem, and of course, there might be a point where whatever’s causing the failure causes a problem for me elsewhere. (I.e., I have no currently strong need for this to be fixed.)

Best Regards,
Ben Hocking