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

PVS Bug 1075


Synopsis:        PVS-Help post from qgxu@mail.shu.edu.cn requires approval
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Sun Jun 19 01:00:01 -0700 2011
Originator:      pvs-help-owner@csl.sri.com
Release:         PVS 5.0
Organization:    csl.sri.com
Environment: 
 System:          
 Architecture: 

Description: 
  --===============1691281384==
  Content-Type: text/plain; charset="us-ascii"
  MIME-Version: 1.0
  Content-Transfer-Encoding: 7bit
  
  As list administrator, your authorization is requested for the
  following mailing list posting:
  
      List:    PVS-Help@csl.sri.com
      From:    qgxu@mail.shu.edu.cn
      Subject: show proofs
      Reason:  Post to moderated list
  
  At your convenience, visit:
  
      http://lists.csl.sri.com/mailman/admindb/pvs-help
          
  to approve or deny the request.
  
  --===============1691281384==
  Content-Type: message/rfc822
  MIME-Version: 1.0
  
  X-Spam-Checker-Version: SpamAssassin 3.1.1 (2006-03-10) on postal.csl.sri.com
  X-Spam-Status: No, hits=-0.0 required=5.0 tests=AWL=-0.742,BAYES_50=0.001,
  	SARE_XMAIL_BULK3a=0.735,UNPARSEABLE_RELAY=0.001 autolearn=no 
  	version=3.1.1 date=Sun, 19 Jun 2011 00:58:36 -0700
  X-Spam-Level: 
  X-Original-Received: from mx1.csl.sri.com (mx1.csl.sri.com [130.107.1.29])
  	by postal.csl.sri.com (8.13.8/8.13.8) with ESMTP id p5J7wSaS035586
  	for <pvs-help@postal.csl.sri.com>; Sun, 19 Jun 2011 00:58:29 -0700 (PDT
 )
  	(envelope-from qgxu@mail.shu.edu.cn)
  X-Original-Received: from brightmail-external2.sri.com
  	(brightmail-external2.SRI.COM [128.18.85.116])
  	by mx1.csl.sri.com (8.13.8/8.13.8) with ESMTP id p5J7wQWV046965
  	for <pvs-help@csl.sri.com>; Sun, 19 Jun 2011 00:58:27 -0700 (PDT)
  	(envelope-from qgxu@mail.shu.edu.cn)
  X-AuditID: 80125574-b7b82ae0000023bd-ab-4dfdac23914a
  X-Original-Received: from mailgate-external4.sri.com
  	(mailgate-external4.SRI.COM [128.18.85.110])
  	by brightmail-external2.sri.com (Symantec Brightmail Gateway) with SMTP
  	id C1.07.09149.32CADFD4; Sun, 19 Jun 2011 00:58:27 -0700 (PDT)
  X-Original-Received: from sdmail5.shu.edu.cn (202.120.127.179)
  	by mailgate-external4.sri.com with SMTP; 19 Jun 2011 07:58:26 -0000
  X-Original-Received: from 58.198.100.167 (HELO SHU-X802) (envelope-from
  	qgxu@mail.shu.edu.cn)
  	by quarkmail.com (quarkmail-1.2.1) with ESMTP id S3203241Ab1FSH6P
  	for pvs-help@csl.sri.com; Sun, 19 Jun 2011 15:58:15 +0800
  Date: Sun, 19 Jun 2011 15:58:17 +0800
  From: "=?gb2312?B?0O3H7Ln6?=" <qgxu@mail.shu.edu.cn>
  To: "pvs-help" <pvs-help@csl.sri.com>
  Subject: show proofs
  Message-ID: <201106191558173235184@mail.shu.edu.cn>
  X-mailer: Foxmail 6, 15, 201, 22 [cn]
  Mime-Version: 1.0
  Content-Type: text/plain;
  	charset="gb2312"
  Content-Transfer-Encoding: 7bit
  X-Brightmail-Tracker: AAAAARhbEu0=
  X-SRI-Archive: pvs-help
  
  Hello, 
  every one
  
  When the command "show-proofs-pvs-file " is issued,  
   PVS give the error message "SPC-scroll, I-Igore.... B-break:" in the  min bu
 ffer and  the hints  "Error:  No methods applicable for generic function" in s
 ome buffer.
  
   the other simliar command such as  "show-proofs-theory" give me the same err
 or.
  
  Note: 1) Both PVS 5.0 and PVS 4.2 have the same  symptom.
           2) PVS is running in the Ubuntu 10.10 under the the VMware workstati
 on 7.0.1.  
          2) my emacs' version is  23.1.1. 
    
  Thanks for your help!
  
  2011-06-19 
  Q.G., XU
  
  
  --===============1691281384==
  Content-Type: message/rfc822
  MIME-Version: 1.0
  
  Content-Type: text/plain; charset="us-ascii"
  MIME-Version: 1.0
  Content-Transfer-Encoding: 7bit
  Subject: confirm ff04d776fe2541fc9c8b478f24f71d5afa5ea3ed
  Sender: pvs-help-request@csl.sri.com
  From: pvs-help-request@csl.sri.com
  
  If you reply to this message, keeping the Subject: header intact,
  Mailman will discard the held message.  Do this if the message is
  spam.  If you reply to this message and include an Approved: header
  with the list password in it, the message will be approved for posting
  to the list.  The Approved: header can also appear in the first line
  of the body of the reply.
  --===============1691281384==--

How-To-Repeat: 

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