vscode-pvs-1.0.58 pre-release

[Paolo Masci]

A new pre-release vscode-pvs-1.0.58 can be downloaded at the following link:

https://drive.google.com/file/d/1k9ERpuaZvNG_qQ_a95_tt9G-zj2X-Tk5/view?usp=sharing

What's new:

- inline command  'goto line-col' in the tcc file, to jump to the line in the pvs file that generated a given proof obligation (see attached screenshot)

- new icon 'typecheck file'

- minor bug fixes

This pre-release is shared here for public testing. It will be made available on the vscode marketplace in the next few days.

-Paolo

[Paolo Masci]

Hi Everyone, I'm sharing a new pre-release vscode-pvs-1.0.58-theta with few additional fixes & improvements: 

https://drive.google.com/file/d/1YCTwOu165tzuGhLDq3DESRKMGSgJbCam/view?usp=sharing

What's new:

- fix for search nasalib (latent bug was causing some results not being shown in certain cases)

- annotation @QED automatically added above a theorem after a successful proof attempt. Note: The annotation is added at the end of interactive proof sessions, and not when re-running in batch mode all proofs in a workspace. If the annotation is already present in your pvs file, vscode-pvs does nothing. I hope this and other similar functionalities that will be added in the future will encourage/help people to document their specs.

Try it out when you have time!

-Paolo