Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 503


Synopsis:        checkpoints confuse proof display
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Tue Jan  2 09:40:03 2001
Originator:      Hendrik Tews
Organization:    inf.tu-dresden.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  consider again the theory
  
      A : Theory
      begin
        a : Lemma 1 = 2
      end A
  
  with
  
      Proof scripts for theory A:
  
      A.a: unfinished [O](n/a s)
  
      ("" (ASSERT) (POSTPONE))
  
  invoke now edit-proof on a and set a checkpoint on postpone such
  that the Proof buffer looks like
  
      ;;; Proof for formula A.a
      ;;; developed with old decision procedures
      ("" (ASSERT) !!(POSTPONE))
  
  install now the proof and when it prompts at the checkpoint rule
  invoke M-x x-show-current-proof. Then the tk window contains the
  interesting proof command
  
      +(lisp (progn (ilisp:ilisp-save)
  		  (lisp (pvs-errors (call-x-show-proof)))))
  
  
  I used PVS Version 2.3 (patch level 1.2.2.120) with GNU Emacs
  20.7.2 (i386-debian-linux-gnu, X toolkit) of Tue Jun 20 2000 on
  raven on Debian Potato (Linux ithif51 2.2.18 #1 Fri Dec 15
  15:26:27 CET 2000 i686 unknown).
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools