PVS successfully typechecks everything

[Max H]

So, I'm having this odd error with the VSCode-pvs on an ubuntu OS, where PVS sucessfully typechecks everything, even when it shouldn't pass. For example:

na : THEORY BEGIN

IMPORTING filethatdoesntexist

END

typechecks. (for some reason I cannot paste an image of the error). When I go to open the pvsio to prove these (correctly typed or not) it will load forever and not let me prove it.

Any ideas? Thanks in advance!

[Paolo Masci]

Hi, thank you for reaching out.

It is likely that something went wrong during the installation of PVS Allegro, so the backend of vscode-pvs is unable to provide the requested functionalities.

Please open the Output panel in vscode, on channel pvs-server and check if you see any error.

You can copy-paste the content of the pvs-server channel here in the case you need help with debugging the installation problem.
Thanks,

Paolo