Latest ARM Mac unstable version ( vscode-pvs-1.0.66-eta-20251209 ) erorring on startup

[0xmycf]

Hello!

I have installed PVS8.0 (from source) and have tried (now a few times) to install vscode-pvs-1.0.66-eta-20251209.vsix in visual studio code.

Some Info:

/usr/local/bin/code --version                                                                                                                                               
1.107.1
994fd12f8d3a5aa16f17d42c041e5809167e845a
arm64

MacOS 26.2 (25C56) with an M4 Chip.

Extension used: vscode-pvs-1.0.66-eta-20251209.vsix (Installed via Install from vsix in the vs-code menu)
PVS build from commit c8094c7c

It is kind of tricky to get any debug output / info from vscode. As soon as vscode is started an error pops up: PVS failed. Please restart using M-x reboot-pvs.. The only button I can press is Ok. As soon as I press ok, the popup appears again, in an endless loop. While this popup is open I cannot do anything else. For some odd reason, there was one occasion where it didnt pop up again, but the extension didnt work either.
After re-starting a couple of times and disabling the extension I was able to get this output:

PVS error : Critical Error (pvs)
This is an unrecoverable error. Reboot the PVS backend to keep using VSCode-PVS (M-x reboot-pvs).

Below you can see a printout of the backend output.


Loading VSCode-PVS patch /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/avoids-debugger-on-proving-session.lispWARNING: redefining PVS::STRAT-EVAL in DEFUN


VSCode-PVS patch /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/avoids-debugger-on-proving-session.lisp LOADED


Loading VSCode-PVS patch /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/lisp-rule-no-quoted-string.lispWARNING: redefining PVS::LISP-RULE in DEFUN


VSCode-PVS patch /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/lisp-rule-no-quoted-string.lisp LOADED


Loading VSCode-PVS patch /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/interface--pvs-emacs.lispWARNING: redefining PVS:PVS-LOG in DEFUN


VSCode-PVS patch /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/interface--pvs-emacs.lisp LOADED


Loading VSCode-PVS patch /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/rules.lispWARNING: redefining PVS::ADDRULE in DEFMACRO
WARNING: redefining PVS::DEFRULEPR* in DEFUN
WARNING: redefining PVS::DEFRULEPR in DEFMACRO
WARNING: redefining PVS::INTERNAL-PC-TYPECHECK in DEFUN
WARNING: redefining PVS::SORT-HASHTABLE in DEFUN

; file: /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/rules.lisp
; in: DEFUN HELP-RULE-FUN
;     (PVS::HELP-RULE PVS::RULE-NAME)
; 
; caught STYLE-WARNING:
;   The function HELP-RULE is called with one argument, but wants exactly two.
; 
; compilation unit finished
;   caught 1 STYLE-WARNING condition
WARNING: redefining PVS::HELP-RULE-FUN in DEFUN
WARNING: redefining PVS::HELP-RULE in DEFUN

Changed rule WARNING: redefining PVS::FAILURE-RULE in DEFUN
HELP
Changed rule WARNING: redefining PVS::SKIP in DEFUN
FAIL
Changed rule WARNING: redefining PVS::POSTPONE in DEFUN
SKIP
Changed rule WARNING: redefining PVS::UNDO in DEFUN
POSTPONE
Changed rule WARNING: redefining PVS::LISP-RULE in DEFUN
UNDO
Changed rule WARNING: redefining PVS::PROP-AXIOM-RULE in DEFUN
WARNING: redefining NEGATE (#<STANDARD-CLASS PVS:NEGATION>) in DEFMETHOD
WARNING: redefining NEGATE (#<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING: redefining PVS::CHECK-PROP-AXIOM in DEFUN
WARNING: redefining PVS::CHECK-PROP-AXIOM* in DEFUN
WARNING:
   redefining ESSENTIALLY-TRUE? (#<STANDARD-CLASS PVS:NAME-EXPR>
                                 #<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING:
   redefining ESSENTIALLY-TRUE? (#<STANDARD-CLASS PVS:NEGATION>
                                 #<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING:
   redefining ESSENTIALLY-TRUE? (#<STANDARD-CLASS PVS:EQUATION>
                                 #<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING:
   redefining ESSENTIALLY-TRUE? (#<STANDARD-CLASS PVS:EXPR>
                                 #<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING:
   redefining NEG-TC-EQ (#<STANDARD-CLASS PVS:EXPR>
                         #<STANDARD-CLASS PVS:NEGATION>) in DEFMETHOD
WARNING:
   redefining NEG-TC-EQ (#<STANDARD-CLASS PVS:EXPR>
                         #<STANDARD-CLASS PVS:EXPR>) in DEFMETHOD
LISP
Changed rule WARNING: redefining PVS::DELETE-RULE-FUN in DEFUN
PROPAX
Changed rule WARNING: redefining PVS::APPLY-STEP in DEFUN
WARNING: redefining PVS::APPLY-STEP-BODY in DEFUN
WARNING:
   redefining COLLECT-SUBGOALS (#<STANDARD-CLASS PVS:PROOFSTATE>) in DEFMETHOD
WARNING:
   redefining COLLECT-SUBGOALS (#<BUILT-IN-CLASS COMMON-LISP:LIST>) in DEFMETHOD
DELETE
Changed rule APPLY
Changed rule SPLIT
Changed rule LIFT-IF
Changed rule LEMMA
Changed rule TYPEPRED
Changed rule TYPEPRED!
Changed rule IFF
Changed rule CASE
Changed rule EXTENSIONALITY
Changed rule NAME
Changed rule INSTANTIATE
Changed rule SKOLEM
Changed rule REVEAL
Changed rule HIDE
Changed rule REPLACE
Changed rule BETA
Changed rule SIMPLIFY
Changed rule AUTO-REWRITE
Changed rule STOP-REWRITE
Changed rule EXPAND
Changed rule WARNING: redefining PVS::SAME-NAME in DEFUN
SAME-NAME
Changed rule LABEL
Changed rule WARNING: redefining PVS::UNLABEL-HIDDEN-STEP in DEFUN
WARNING: redefining PVS::HIDDEN-SFORM-REDUCE in DEFUN
UNLABEL
Changed rule JUST-INSTALL-PROOF
Changed rule COMMENT
Changed rule FLATTEN-DISJUNCT
Changed rule SET-PRINT-LINES
Changed rule SET-PRINT-LENGTH
Changed rule SET-PRINT-DEPTH
Changed rule SET-RIGHT-MARGIN
Changed rule WARNING: redefining PVS::INVOKE-DECIDE in DEFUN
DECIDE
Changed rule COPY

VSCode-PVS patch /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/rules.lisp LOADED


Loading VSCode-PVS patch /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/patch-20260101-context--avoids-lock-on-package-when-intern-assert.lispWARNING: redefining PVS::PVS-CONTEXT-VERSION in DEFUN
WARNING: redefining PVS::PVS-CONTEXT-LIBRARIES in DEFUN
WARNING: redefining PVS::PVS-CONTEXT-DEFAULT-DECISION-PROCEDURE in DEFUN
WARNING: redefining PVS::CURRENT-PVS-CONTEXT in DEFUN
WARNING:
   redefining PVS-CONTEXT :AROUND (#<STANDARD-CLASS PVS::WORKSPACE-SESSION>) in DEFMETHOD
WARNING: redefining PVS::CURRENT-PVS-CONTEXT-CHANGED in DEFUN
WARNING: redefining PVS::CURRENT-CONTEXT in DEFUN
WARNING: redefining CONTEXT-PATH (#<STANDARD-CLASS PVS:CONTEXT>) in DEFMETHOD
WARNING:
   redefining CONTEXT-PATH (#<STANDARD-CLASS PVS:DECLARATION>) in DEFMETHOD
WARNING: redefining PVS::CURRENT-PVS-FILE in DEFUN
WARNING: redefining PVS:CURRENT-THEORY in DEFUN
WARNING: redefining PVS:CURRENT-THEORY-NAME in DEFUN
WARNING: redefining PVS::CURRENT-THEORY-NAME-WITH-DACTUALS in DEFUN
WARNING: redefining PVS::CURRENT-THEORY-NAME-DACTS in DEFUN
WARNING: redefining PVS::PVS-CONTEXT-YICES-EXECUTABLE in DEFUN
WARNING: redefining PVS::PVS-CONTEXT-YICES2-EXECUTABLE in DEFUN
WARNING: redefining PVS::PVS-CONTEXT-ENTRIES in DEFUN
WARNING: redefining PVS::CE-EQ in DEFUN
WARNING: redefining PVS::TE-EQ in DEFUN
WARNING: redefining PVS::FE-EQ in DEFUN
WARNING: redefining PVS::DE-EQ in DEFUN
WARNING: redefining ID (#<STRUCTURE-CLASS PVS::THEORY-ENTRY>) in DEFMETHOD
WARNING: redefining ID (#<STRUCTURE-CLASS PVS::FORMULA-ENTRY>) in DEFMETHOD
WARNING: redefining PVS::CW in DEFUN
WARNING: redefining PVS:CHANGE-WORKSPACE in DEFUN
WARNING: redefining PVS::CHANGE-CONTEXT in DEFUN
WARNING: redefining PVS::RESET-WORKSPACE in DEFUN
WARNING: redefining PVS::CONTEXT-PATHNAME in DEFUN
WARNING: redefining PVS:SAVE-CONTEXT in DEFUN
WARNING: redefining PVS::SC in DEFUN
WARNING: redefining PVS::WRITE-CONTEXT in DEFUN
WARNING: redefining PVS::WRITE-OBJECT-FILES in DEFUN
WARNING: redefining PVS::WRITE-OBJECT-FILE in DEFUN
WARNING:
   redefining GET-THEORY-WITH-FILENAME (#<STANDARD-CLASS PVS:DATATYPE-OR-MODULE>) in DEFMETHOD
WARNING: redefining BINPATH-ID (#<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING:
   redefining BINPATH-NAME (#<STANDARD-CLASS PVS:MODNAME>
                            #<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING: redefining PVS::ENSURE-BIN-SUBDIRECTORY in DEFUN
WARNING: redefining PVS::CONTEXT-IS-CURRENT in DEFUN
WARNING: redefining PVS::UPDATE-PVS-CONTEXT in DEFUN
WARNING: redefining PVS::INITIAL-CONTEXT in DEFUN
WARNING: redefining PVS::MAKE-PVS-CONTEXT in DEFUN
WARNING: redefining PVS::CONTEXT-PARAMETERS in DEFUN
WARNING: redefining PVS:UPDATE-CONTEXT in DEFUN
WARNING: redefining PVS::DELETE-FILE-FROM-WORKSPACE in DEFUN
WARNING: redefining PVS::REMOVE-CONTEXT-ENTRY-DEPS in DEFUN
WARNING: redefining PVS::UPDATE-CONTEXT-PROOF-STATUS in DEFUN
WARNING: redefining PVS::CREATE-CONTEXT-ENTRY in DEFUN
WARNING: redefining PVS::MD5-FILE in DEFUN
WARNING: redefining PVS::CREATE-THEORY-ENTRY in DEFUN
WARNING: redefining PVS::GET-BINFILE-DEPENDENCIES in DEFUN
WARNING:
   redefining LIB-DATATYPE-OR-THEORY? (#<STANDARD-CLASS PVS:DATATYPE-OR-MODULE>) in DEFMETHOD
WARNING:
   redefining LIB-DATATYPE-OR-THEORY? (#<STANDARD-CLASS PVS:INLINE-RECURSIVE-TYPE>) in DEFMETHOD
WARNING:
   redefining LIB-DATATYPE-OR-THEORY? (#<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING: redefining PVS::ADD-GENERATED-ADT-THEORIES in DEFUN
WARNING: redefining PVS::CREATE-FORMULA-ENTRY in DEFUN
WARNING: redefining PVS::HIDDEN-FORMULA-ENTRIES in DEFUN
WARNING: redefining PVS::CREATE-DECLARATION-ENTRY in DEFUN
WARNING: redefining PVS::FILE-DEPENDENCIES in DEFUN
WARNING: redefining PVS::FILE-DEPENDENCIES* in DEFUN
WARNING: redefining PVS::CIRCULAR-FILE-DEPENDENCIES in DEFUN
WARNING: redefining PVS::CIRCULAR-FILE-DEPENDENCIES* in DEFUN
WARNING: redefining DEP-FILENAME (#<STANDARD-CLASS PVS:MODULE>) in DEFMETHOD
WARNING:
   redefining DEP-FILENAME (#<STANDARD-CLASS PVS:RECURSIVE-TYPE>) in DEFMETHOD
WARNING: redefining PVS:CONTEXT-USINGCHAIN in DEFUN
WARNING: redefining PVS:GET-PVS-FILE-DEPENDENCIES in DEFUN
WARNING: redefining PVS::GET-PVS-FILE-DEPENDENCIES* in DEFUN
WARNING: redefining PVS:GET-THEORY-DEPENDENCIES in DEFUN
WARNING: redefining PVS::CONSISTENT-WORKSPACE-PATHS in DEFUN
WARNING: redefining PVS:RESTORE-CONTEXT in DEFUN
WARNING: redefining PVS::READ-CONTEXT-FILE in DEFUN
WARNING: redefining PVS::DUPLICATE-THEORY-ENTRIES? in DEFUN
WARNING: redefining PVS::COLLECT-THEORY-ENTRY-IDS in DEFUN
WARNING: redefining PVS::RESTORE-THEORIES in DEFUN
WARNING: redefining PVS::RESTORE-THEORIES* in DEFUN
WARNING: redefining PVS::RESTORE-THEORY in DEFUN
WARNING:
   redefining UPDATE-RESTORED-THEORIES (#<STANDARD-CLASS PVS:MODULE>) in DEFMETHOD
WARNING:
   redefining UPDATE-RESTORED-THEORIES (#<STANDARD-CLASS PVS:RECURSIVE-TYPE>) in DEFMETHOD
WARNING: redefining PVS::MAKE-NEW-CONTEXT-FROM-OLD in DEFUN
WARNING: redefining PVS::PVS-CONTEXT-UPGRADE-FUNCTION in DEFUN
WARNING: redefining PVS::UPGRADE-FROM-1.1-BETA in DEFUN
WARNING: redefining PVS::UPGRADE-FROM-1.0-BETA in DEFUN
WARNING: redefining PVS::SAME-MAJOR-VERSION-NUMBER in DEFUN
WARNING: redefining PVS::MAJOR-VERSION in DEFUN
WARNING: redefining PVS:PVS-RENAME-FILE in DEFUN
WARNING: redefining PVS:SHOW-CONTEXT-PATH in DEFUN
WARNING: redefining PVS::CURRENT-WORKSPACE in DEFUN
WARNING: redefining PVS:CURRENT-CONTEXT-PATH in DEFUN
WARNING:
   redefining VALID-CONTEXT-ENTRY (#<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING:
   redefining VALID-CONTEXT-ENTRY (#<STRUCTURE-CLASS PVS::CONTEXT-ENTRY>) in DEFMETHOD
WARNING: redefining PVS::VALID-CONTEXT-ENTRY* in DEFUN
WARNING: redefining PVS::VALID-CONTEXT-ENTRY-FILE in DEFUN
WARNING:
   redefining GET-CONTEXT-FILE-ENTRY (#<STANDARD-CLASS PVS:DATATYPE-OR-MODULE>) in DEFMETHOD
WARNING:
   redefining GET-CONTEXT-FILE-ENTRY (#<BUILT-IN-CLASS COMMON-LISP:PATHNAME>) in DEFMETHOD
WARNING:
   redefining GET-CONTEXT-FILE-ENTRY (#<BUILT-IN-CLASS COMMON-LISP:STRING>) in DEFMETHOD
WARNING:
   redefining GET-CONTEXT-FILE-ENTRY (#<STANDARD-CLASS PVS:DECLARATION>) in DEFMETHOD
WARNING: redefining PVS:CONTEXT-FILES-AND-THEORIES in DEFUN
WARNING: redefining PVS:GET-CONTEXT-THEORY-NAMES in DEFUN
WARNING: redefining PVS:GET-CONTEXT-THEORY-ENTRY in DEFUN
WARNING: redefining PVS::GET-CONTEXT-THEORY-ENTRY* in DEFUN
WARNING: redefining PVS::GET-CONTEXT-FORMULA-ENTRY in DEFUN
WARNING: redefining PVS:CONTEXT-FILE-OF in DEFUN
WARNING: redefining PVS:PVS-FILE-OF in DEFUN
WARNING: redefining PVS::CONTEXT-FILE-OF* in DEFUN
WARNING: redefining PVS:CONTEXT-ENTRY-OF in DEFUN
WARNING: redefining PVS::CONTEXT-ENTRY-OF-FILE in DEFUN
WARNING: redefining PVS:RESTORE-FROM-CONTEXT in DEFUN
WARNING: redefining PVS::GET-DECLARATION-ENTRY-DECL in DEFUN
WARNING: redefining PVS::GET-REFERENCED-DECLARATION in DEFUN
WARNING: redefining PVS::GET-REFERENCED-DECLARATION* in DEFUN
WARNING: redefining PVS::MIN-THEORY-WRT-IMPS in DEFUN
WARNING: redefining PVS::INVALIDATE-CONTEXT-FORMULA-PROOF-INFO in DEFUN
WARNING: redefining PVS::INVALIDATE-THEORY-PROOFS in DEFUN
WARNING: redefining PVS::INVALIDATE-PROOFS in DEFUN
WARNING:
   redefining VALID-PROOFS-FILE (#<STRUCTURE-CLASS PVS::CONTEXT-ENTRY>) in DEFMETHOD
WARNING:
   redefining VALID-PROOFS-FILE (#<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING: redefining PVS:SAVE-ALL-PROOFS in DEFUN
WARNING: redefining PVS::SAVE-PVS-FILE-PROOFS in DEFUN
WARNING: redefining PVS::HAS-PROOF? in DEFUN
WARNING: redefining PVS::TOGGLE-PROOF-PRETTYPRINTING in DEFUN
WARNING: redefining PVS:SAVE-PROOFS in DEFUN
WARNING: redefining PVS::SAVE-PROOFS-TO-FILE in DEFUN
WARNING: redefining PVS::SAVE-PROOFS-TO-JSON in DEFUN
WARNING: redefining PVS::PROOF-FILE-ALIST in DEFUN
WARNING: redefining PVS::PROOF-THEORY-ALIST in DEFUN
WARNING: redefining PVS::PROOF-DECLS-ALIST in DEFUN
WARNING: redefining PVS::PROOF-ELEMENT-ALIST in DEFUN
WARNING: redefining PVS::PROOF-DECL-REF-ALIST in DEFUN
WARNING: redefining PVS::BACKUP-PROOF-FILE in DEFUN
WARNING: redefining PVS::INVALID-PROOF-FILE in DEFUN
WARNING: redefining PVS::INVALID-PROOF-FILE* in DEFUN
WARNING: redefining PVS::CURRENT-PROOFS-CONTAIN-OLD-PROOFS in DEFUN
WARNING: redefining PVS::CURRENT-PROOFS-CONTAIN-OLD-PROOFS* in DEFUN
WARNING: redefining PVS::CURRENT-PROOFS-CONTAIN-OLD-PROOFS** in DEFUN
WARNING: redefining PVS::COLLECT-THEORIES-PROOFS in DEFUN
WARNING: redefining PVS::COLLECT-THEORIES-PROOFS* in DEFUN
WARNING: redefining PVS::COLLECT-THEORY-PROOFS in DEFUN
WARNING: redefining PVS::COLLECT-THEORY-PROOFS* in DEFUN
WARNING:
   redefining COLLECT-DECL-PROOFS (#<STANDARD-CLASS PVS:FORMULA-DECL>) in DEFMETHOD
WARNING:
   redefining COLLECT-DECL-PROOFS (#<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING: redefining PVS::MERGE-PROOFS in DEFUN
WARNING: redefining PVS::RESTORE-PROOFS in DEFUN
WARNING: redefining PVS::RESTORE-THEORY-PROOFS in DEFUN
WARNING: redefining PVS::RESTORE-DECLS-PROOFS in DEFUN
WARNING: redefining PVS::RESTORE-FORMULA-PROOFS in DEFUN
WARNING: redefining PVS::FE-STATUS-TO-PROOF-STATUS in DEFUN
WARNING:
   redefining MAKE-PROOF-INFOS-FROM-SEXP (#<STANDARD-CLASS PVS::TCC-DECL>
                                          #<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING:
   redefining MAKE-PROOF-INFOS-FROM-SEXP (#<STANDARD-CLASS PVS:FORMULA-DECL>
                                          #<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING: redefining PVS::DECL-TCCS-AND-PROOFS in DEFUN
WARNING: redefining PVS::DECL-TCCS in DEFUN
WARNING: redefining PVS::COLLECT-TCC-PROOFS in DEFUN
WARNING: redefining PVS::NUMERIC-SUFFIX in DEFUN
WARNING: redefining PVS::RESTORE-TCC-PROOFS in DEFUN
WARNING: redefining PVS::RESTORE-TCC-PROOFS* in DEFUN
WARNING: redefining PVS::TCC-EXPR-MATCHES in DEFUN
WARNING: redefining PVS::RESTORE-PROOF-TO-TCC in DEFUN
WARNING: redefining PVS::GET-SMALLER-PROOF-INFO in DEFUN
WARNING: redefining PVS::CONVERT-PROOF-FORM-TO-LOWERCASE in DEFUN
WARNING: redefining PVS::PVS-CLASS-NAMES in DEFUN
WARNING: redefining PVS::ALL-SUBCLASSES in DEFUN
WARNING: redefining PVS::CONVERT-REFERSTO-TO-LOWERCASE in DEFUN
WARNING: redefining PVS::FILTER-NIL-FORM in DEFUN
WARNING: redefining PVS::CONVERT-REFERSTO-TO-LOWERCASE* in DEFUN
WARNING: redefining PVS::COPY-PROOFS-TO-ORPHAN-FILE in DEFUN
WARNING: redefining PVS::PROOFS-EQUAL in DEFUN
WARNING: redefining PVS::PROOFS-EQUAL* in DEFUN
WARNING: redefining PVS::ORPH-PROOFS-EQUAL in DEFUN
WARNING: redefining PVS::ORPH-PROOFS-EQUAL* in DEFUN
WARNING: redefining PVS::READ-THEORY-PROOFS in DEFUN
WARNING: redefining PVS::READ-PVS-FILE-PROOFS in DEFUN
WARNING: redefining PVS::READ-PROOF-FILE-STREAM in DEFUN
WARNING: redefining PVS::MAKE-CURRENT-PROOFS-SEXPS in DEFUN
WARNING: redefining PVS::MAKE-CURRENT-PROOFS-SEXPS* in DEFUN
WARNING: redefining PVS::MAKE-CURRENT-PROOF-SEXPS in DEFUN
WARNING: redefining PVS::MAKE-CURRENT-PRFINFO-SEXP in DEFUN
WARNING: redefining PVS::READ-PROOF in DEFUN
WARNING: redefining PVS::READ-PROOF-DECLS in DEFUN
WARNING: redefining PVS::READ-PROOFS-OF-DECLS in DEFUN
WARNING: redefining PVS::READ-PROOFS-REFERS-TO in DEFUN
WARNING: redefining PVS::READ-TO-PAREN-OR-QUOTE in DEFUN
WARNING: redefining PVS::READ-TO-PAREN in DEFUN
WARNING: redefining PVS::READ-TO-LEFT-PAREN in DEFUN
WARNING: redefining PVS::READ-TO-RIGHT-PAREN in DEFUN
WARNING: redefining PVS::READ-CASE-SENSITIVE in DEFUN
WARNING: redefining PVS::UPCASE-SYMBOLS in DEFUN
WARNING: redefining PVS::UPCASE-T-AND-NIL in DEFUN
WARNING: redefining PVS::CONVERT-PROOF-IF-NEEDED in DEFUN
WARNING: redefining PVS::CONVERT-PROOF-IF-NEEDED* in DEFUN
WARNING: redefining PVS::CONVERT-PROOF-IF-NEEDED** in DEFUN
WARNING: redefining PVS::CONVERT-PROOF-FORM in DEFUN
WARNING: redefining PVS::UPPER-OR-NOT-ALPHA-P in DEFUN
WARNING: redefining PVS::FIND-FIRST-SYMBOL in DEFUN
WARNING: redefining PVS::CHECK-IF-CASE-CHANGE-NEEDED in DEFUN
WARNING: redefining PVS::TRANSFER-ORPHANED-PROOFS in DEFUN
WARNING: redefining PVS::READ-ORPHANED-PROOFS in DEFUN
WARNING: redefining PVS::READ-ORPHANED-FILE-ENTRIES in DEFUN
WARNING: redefining PVS::GET-ORPHANED-PROOF-ENTRY in DEFUN
WARNING: redefining PVS::GET-PROOFS-ENTRY in DEFUN
WARNING: redefining PVS:SHOW-PROOF-FILE in DEFUN
WARNING: redefining PVS:SHOW-ORPHANED-PROOFS in DEFUN
WARNING: redefining PVS:PVS-SELECT-PROOF in DEFUN
WARNING: redefining PVS:PVS-VIEW-PROOF in DEFUN
WARNING: redefining PVS:PVS-DELETE-PROOF in DEFUN
WARNING: redefining PVS:READ-STRATEGIES-FILES in DEFUN
WARNING: redefining PVS::LOAD-LIBRARY-STRATEGY-FILES in DEFUN
WARNING: redefining PVS::LOAD-LIBRARY-STRATEGY-FILE in DEFUN
WARNING: redefining PVS::LOAD-STRATEGIES-FILE in DEFUN
WARNING: redefining PVS::ADD-LOWERCASE-PROVER-IDS in DEFUN
WARNING: redefining PVS::ADD-LOWERCASE-PROVER-HASH-IDS in DEFUN
WARNING: redefining PVS::ADD-LOWER-CASE-PROVER-KEYWORDS in DEFUN
WARNING: redefining PVS::MAKE-PRF-PATHNAME in DEFUN
WARNING: redefining PVS:HANDLE-DELETED-THEORIES in DEFUN
WARNING: redefining PVS::RELOAD-THEORY-ORPHANED-PROOFS in DEFUN
WARNING: redefining PVS::COLLECT-ALL-THEORIES in DEFUN
WARNING: redefining PVS::COLLECT-PRELUDE-THEORIES in DEFUN
WARNING: redefining PVS::COLLECT-THEORIES in DEFUN
WARNING: redefining PVS::COLLECT-THEORY-FILE-PAIRS in DEFUN
WARNING: redefining PVS::COLLECT-THEORY-NAMES in DEFUN
WARNING: redefining PVS::COLLECT-THEORIES* in DEFUN
WARNING: redefining PVS::COLLECT-ELEMENT-IDS in DEFUN
WARNING: redefining PVS::FIND-ALL-USEDBYS in DEFUN
WARNING: redefining PVS::VERIFY-USEDBYS in DEFUN
WARNING: redefining PVS::INSTALL-PVS-PROOF-FILE in DEFUN
WARNING:
   redefining CLEAR-PROOF-STATUS (#<SYSTEM-CLASS COMMON-LISP:T>) in DEFMETHOD
WARNING: redefining PVS::AUTO-SAVE-PROOF-SETUP in DEFUN
WARNING: redefining PVS::AUTO-SAVE-PROOF in DEFUN
WARNING: redefining PVS::REMOVE-AUTO-SAVE-PROOF-FILE in DEFUN
WARNING: redefining PVS::COPY-AUTO-SAVED-PROOFS-TO-ORPHAN-FILE in DEFUN
WARNING: redefining PVS::RESTORE-PROOFS-FROM-SPLIT-FILE in DEFUN
WARNING: redefining PVS::RESTORE-PROOFS-FROM-SPLIT-FILE* in DEFUN
WARNING: redefining PVS::CLEANUP-PROOFS-PVS-FILE in DEFUN
WARNING: redefining PVS::COLLECT-DEFAULT-PROOFS in DEFUN
WARNING: redefining PVS::COLLECT-THEORY-DEFAULT-PROOFS in DEFUN
WARNING: redefining PVS::COLLECT-FORMULA-DEFAULT-PROOFS in DEFUN
WARNING: redefining PVS::MAXIMAL-THEORY-HIERARCHY-ELEMENTS in DEFUN
WARNING: redefining PVS::CHECK-BINFILES in DEFUN
WARNING: redefining PVS::CHECK-BINFILES* in DEFUN
WARNING: redefining PVS::CHECK-BINFILE in DEFUN
WARNING: redefining PVS::REMOVE-BINFILES in DEFUN
WARNING: redefining PROVED? (#<STRUCTURE-CLASS PVS::FORMULA-ENTRY>) in DEFMETHOD
WARNING:
   redefining UNPROVED? (#<STRUCTURE-CLASS PVS::FORMULA-ENTRY>) in DEFMETHOD
WARNING: redefining PVS::COLLECT-CURRENT-DEFAULT-PROOFS in DEFUN
WARNING: redefining PVS::COLLECT-DEFAULT-PROOFS-THEORIES in DEFUN
WARNING: redefining PVS::COLLECT-DEFAULT-PROOFS-THEORY in DEFUN
WARNING: redefining PVS::COLLECT-DEFAULT-PROOFS-THEORY* in DEFUN
WARNING: redefining PVS::ALL-PROOF-STATUSES in DEFUN
WARNING: redefining PVS::GIT-INIT in DEFUN
WARNING: redefining PVS::GIT-ADD in DEFUN
WARNING: redefining PVS::UNDER-GIT-CONTROL? in DEFUN
WARNING: redefining PVS::SAVE-CONTEXT-TO-JSON in DEFUN
WARNING: redefining PVS::CTX-ALIST in DEFUN
WARNING: redefining PVS::CE-ALIST in DEFUN
WARNING: redefining PVS::TE-ALIST in DEFUN
WARNING: redefining PVS::TE-DEPENDENCY in DEFUN
WARNING: redefining PVS::TE-FORMULA in DEFUN
WARNING: redefining PVS::DECL-ENTRY in DEFUN
WARNING: redefining PVS::CONSISTENT-FE-ENTRIES-AND-PROOFS in DEFUN


VSCode-PVS patch /Users/mycf/.vscode/extensions/paolomasci.vscode-pvs-1.0.66-eta-20251209/pvs-patches/patch-20260101-context--avoids-lock-on-package-when-intern-assert.lisp LOADED


debugger invoked on a SIMPLE-ERROR in thread
#<THREAD tid=259 "main thread" RUNNING {70135B0003}>:

It is nearly impossible for me to read the terminal ouput, as I cannot select it quick enough during startup. During that one occasion mentioned earlier, I was able to read the output, and it complained about missing libcrypto.dylib in /opt/homebrew/opt/openssl/lib, but I have installed openssl since then via homebrew.

Any help would be greatly appreciated!

[pmasci]

Hi, Thank you for reporting this issue.

The experimental build of vscode-pvs you are using is outdated -- it's trying to install PVS 8 from an old commit, as well as patches that are not needed anymore.

To resolve the issue, please try the following:

1. download this new experimental build of vscode-pvs: vscode-pvs-1.0.66-eta-04132026.vsix
2. after installing the new vsix file, please use M-x install-pvs to force a fresh clone/install of the latest version of PVS 8 from github

Please let us know if this resolves the issue.
Thanks,
-Paolo

[0xmycf]

The error still persists... I have deleted the full ~/PVS folder for a clean re-install too. Could it be that I am missing some other dependency locally? If you have any idea how I could provide you with more feedback let me know.

[pmasci]

Hi, let's try to debug the error by installing PVS8 manually from a terminal, as this should help you identify what in the installation sequence is broken or if there's any missing dependency.

Please make sure you have the following dependencies before proceeding:

• SBCL: sbcl --version
• xcode command line tools: xcode-select --version

Download the Makefile used by vscode-pvs to install PVS8:
curl -O https://raw.githubusercontent.com/nasa/vscode-pvs/refs/heads/master/vscode-pvs/extra/Makefile-PVS8

Run the install-pvs target in the downloaded Makefile, and pass the target PVS installation folder to the Makefile:
make install-pvs -f Makefile-PVS8 INSTALLATION_PATH=~/PVS8

Try to run PVS8 in headless mode:
cd ~/PVS8/pvs-8.0 && ./pvs -raw -port 23456

If PVS8 starts successfully, you should see a banner like the following:

NOTICE: Running in debug mode. Debugger will be invoked on errors.
  Specify ':debug nil' to turn it off on remote environments.
Hunchentoot server is started.
Listening on 127.0.0.1:23457.

PVS(1):

[pmasci]

I was able to reproduce a similar problem on a Linux machine -- in my case, PVS gives an exception because the hunchentoot server is not properly loaded (see output below).

Can you please confirm that your problem is also due to hunchentoot?
The output you provided in your earlier post seems to be truncated at the end, because I don't see the name of the handler that is causing the exception.
Thanks

$ ./pvs -raw -port 23456

debugger invoked on a SIMPLE-ERROR in thread
#<THREAD "main thread" RUNNING {1000EC8103}>:
  :HUNCHENTOOT is unknown handler.

$ sbcl --version
SBCL 2.1.11.debian
$ cat /etc/issue
Ubuntu 22.04.5 LTS

[0xmycf]

Yes, my output is:

$  ./pvs -raw -port 23456                                                                                                                                                      

debugger invoked on a SIMPLE-ERROR in thread
#<THREAD tid=259 "main thread" RUNNING {7010040003}>:
  :HUNCHENTOOT is unknown handler.

Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.

restarts (invokable by number or by possibly-abbreviated name):
  0: [ABORT] Exit from the current thread.

(CLACK.UTIL:FIND-HANDLER :HUNCHENTOOT)
   source: (ERROR "~S is unknown handler." SERVER)
0]

and

$ sbcl --version
SBCL 2.6.0

Though, there is also ~/PVS/sbcl/bin/sbcl with version 2.4.4

The output you provided in your earlier post seems to be truncated at the end, because I don't see the name of the handler that is causing the exception.

Yes that confused me too, but I posted the whole output I was able to see.

Thank you for investigating this!

[pmasci]

Hi, please try the following fix:

• edit Makefile.in in the pvs distribution, as indicated in this commit: SRI-CSL/PVS@752c53e
• re-run ./configure and make from the terminal to re-build pvs8
• try to launch again pvs in server mode (./pvs -raw -port 23456)

If you get no error, then the issue should be resolved and you should be able to use pvs8 within vscode-pvs.
Please let me know how it goes.
Thanks,
--Paolo

[pmasci]

We made further progress and this issue should now be resolved:

• a new release of the Visual Studio Code extension for PVS8 (VSCode-PVS8) is now available on the MarketPlace: https://marketplace.visualstudio.com/items?itemName=paolomasci.vscode-pvs8
• all the necessary changes to resolve the issue with the Hunchentoot library have been incorporated in PVS (version 8.1)

Thanks,
--Paolo

[0xmycf]

Hi Paolo!

This has resolved the issue for me. Thank you very much!