type checking not responding issue on Mac VSCode-PVS

[yl182]

Hello,

I am a student working on a joint project using PVS, and encountered the following issue in type-checking step:

Environment:

• Mac 12.2.1

• VSCode and NodeJS

• PVS extension from VSCode marketplace

• with PVS Allegro installed (followed the instructions here https://github.com/nasa/vscode-pvs)

Issue:

• No matter which pvs file I type check, it always shows the message "Almost ready, please wait... (Typechecking [the pvs file path])" and sometimes "unable to connect to pvs server ...".

I have tried reboot and reinstall the PVS extension, and reinstall VSCode. Would it be likely that I forgot to do something?

Thank so much in advance.

[pmasci]

Hi, thank you for reaching out. Would you be able to share the content of the Output panel? There is probably an error message in that panel can help me understand what is going on.

To view the Output panel, use View -> Output Once the output panel is open:

• Please make sure you are looking at channel "pvs-server" (there's a dropdown menu in the panel where you can select the channel).
• Share a screenshot or copy-paste here the content of the Output panel, there is probably an error indicating why the server is not responding

Thanks, Paolo

[yl182]

Thank you, Paolo. I have copied the content in output panel:

[pvs-server] Checking dependencies... [pvs-language-server] Rebooting PVS (installation folder is /Users/zcy/Documents/pvs-7.1.0) [pvs-proxy] Starting pvs-proxy... [pvs-proxy] Rebooting pvs-server...

ACL_LOCALE=en_US.UTF-8 LC_ALL=en_US.UTF-8 LANG=en_US.UTF-8

/Users/zcy/Documents/pvs-7.1.0/pvs -raw -port 22334 No executable available in /Users/zcy/Documents/pvs-7.1.0/bin/arm-MacOSX

[pvs-proxy-legacy] Activating stand-alone pvs process

ACL_LOCALE=en_US.UTF-8 LC_ALL=en_US.UTF-8 LANG=en_US.UTF-8

/Users/zcy/Documents/pvs-7.1.0/pvs -raw [pvs-process] Process exited { code: 1, signal: null } [pvs-proxy] Checking port 9092... { code: 1, signal: null } [pvs-proxy] port 9092 is available :) [pvs-proxy] Starting GUI Server on http://0.0.0.0:9092 [pvs-proxy] Reboot complete! [pvs-proxy] Ready! [pvs-server] Checking dependencies... [pvs-proxy] New PVS path: /Users/zcy/Documents/pvs-7.1.0 [pvs-proxy] Rebooting pvs-server...

ACL_LOCALE=en_US.UTF-8 LC_ALL=en_US.UTF-8 LANG=en_US.UTF-8

/Users/zcy/Documents/pvs-7.1.0/pvs -raw -port 22334 No executable available in /Users/zcy/Documents/pvs-7.1.0/bin/arm-MacOSX

[pvs-proxy-legacy] Activating stand-alone pvs process

ACL_LOCALE=en_US.UTF-8 LC_ALL=en_US.UTF-8 LANG=en_US.UTF-8

/Users/zcy/Documents/pvs-7.1.0/pvs -raw [pvs-process] Process exited { code: 1, signal: null } [pvs-proxy] Reboot complete! { code: 1, signal: null } [pvs-server] Operation cancelled by the user [pvs-proxy] Error returned by pvs-server: Error: connect ECONNREFUSED 0.0.0.0:22334 at TCPConnectWrap.afterConnect [as oncomplete] (node:net:1157:16) { errno: -61, code: 'ECONNREFUSED', syscall: 'connect', address: '0.0.0.0', port: 22334 } [pvs-proxy] Connection refused when launching pvs from /Users/zcy/Documents/pvs-7.1.0

[pmasci]

From the log I see you have an Apple Silicon chip (M1) -- can you confirm? PVS needs an Intel Mac, the M1 chip is not supported for now.

We are working with SRI to resolve this problem with M1. I am afraid the only solution for now is to use a different laptop. Sorry about that. Paolo

[yl182]

Thank you. If I do not use VSCode and just write PVS from emacs, would the problem still be there? Or would it be a solution if I set up a Linux environment on the current machine?

[pmasci]

You can try, but I believe the problem is in PVS itself. I would recommend opening an issue on the PVS github repository (https://github.com/SRI-CSL/PVS), so SRI is aware there is a growing number of users with the M1

[mj357]

Hello. I am also a student and we've run into the same issue in our study group. I saw that PVS8.0 now supports MX chips natively.

When I'll get the time I'll try to install PVS8.0 manually, but seeing that this extensions installs PVS 7.1 I wonder what reason there is to not use 8.0? Will I run into issues?

Regardless, Ill comment again with my results after I tried.

Thank you :)

[pmasci]

Hi, thank you for reaching out.

The current version of vscode-pvs works only with PVS7.1, so you need Intel Mac or Linux. There are no typechecking issues on those machines as far as I know.

We are preparing a new release of vscode-pvs that supports PVS8.0. PVS8.0 has new APIs (websockets in PVS8.0 vs xml-rpc in PVS7.1), that is why the current version of vscode-pvs cannot be used with PVS8.0. To use PVS8.0, I am afraid you need to use the native emacs interface for now.

We will keep sharing updates here on github and on the PVS Google group about PVS8.0 support for vscode-pvs. It will be available in the coming months.

Thanks!