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

Re: [PVS-Help] Type checking issue



Hi Sam:

The patch does not seem to work. 

It does seem to load:

Attempting to compile patch file patch-20141123
;;; Compiling file
;;;   /Users/jonathan/Applications/pvs-6.0-ix86-MacOSX-allegro/lib/pvs-patches/patch-20141123.lisp
; While file-compiling #'maybe-instantiate-from-decl-formals* in
#P"/Users/jonathan/Applications/pvs-6.0-ix86-MacOSX-allegro/lib/pvs-patches/patch-20141123.lisp"
; starting at file character position 19:
Warning: mk-modname should be given between 1 and 5 arguments.  It was
         given 6 arguments.
;;; Writing fasl file
;;;   /Users/jonathan/Applications/pvs-6.0-ix86-MacOSX-allegro/lib/pvs-patches/patch-20141123.n64fasl
;;; Fasl write complete

Regards

Jonathan

On Nov 26, 2014, at 1:51 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:

Hi Jonathan,

This is indeed a bug; I'm including a patch for it below.
Simply create a <PVS>/lib/pvs-patches/ directory (where <PVS> is where you
installed PVS), and copy it there.  It will be loaded automatically on
startup (you can look in the *pvs* buffer to see that it is being loaded,
along with the nasa lib patches).

Regards,
Sam

<patch-20141123.lisp>
Jonathan Ostroff <jonathan@xxxxxxxx> wrote:

The snippet below reproduces mysterious behaviour in a bigger project

===
tup_small : THEORY

 BEGIN

 ARR [T: TYPE]: TYPE =
 [# size    : nat
  , content : [below(size) -> T]
  #]

 TUP [T: TYPE] : TYPE = [T, nat]

 valid_bag? [T: TYPE] (a: ARR[TUP]): bool =
   TRUE

 END tup_small
===

When trying to type check, I get at the bottom a message that says SPC-Scroll, I-ignore etc.

There is also an Error:assertion report at the top.

I am wondering what I did wrong? 

Thanks,

Jonathan

[cid]