Attempting to compile patch file patch-20141123
;;; Compiling file
; While file-compiling #'maybe-instantiate-from-decl-formals* in
; 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
;;; Fasl write complete
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 youinstalled PVS), and copy it there. It will be loaded automatically onstartup (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
ARR [T: TYPE]: TYPE =
[# size : nat
, content : [below(size) -> T]
TUP [T: TYPE] : TYPE = [T, nat]
valid_bag? [T: TYPE] (a: ARR[TUP]): bool =
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?