vscode-pvs-1.0.56 pre-release

[Paolo Masci]

A new vscode-pvs pre-release (1.0.56-gamma) is available at the following link:

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

This new version introduces the following enhancements/fixes:

 - Added syntax highlighting for math symbols representing keywords (∀ ∃ ⇒ ⇔ ¬)  

 - Added pvs patches 20210706..20210715a (fixes for assertion errors, judgements, importings, prf files)    

 - Improved performance of vscode-plot command (pvsio process cache)  

 - Improved proof-explorer (enabled copy-paste across proof attempts) 

 - Fix for pvsio importing (pvs_library_path)  

[Alberto Ercolani]

Hello Paolo, these features are great and the current implementation works very well.

Can I ask for an additional feature? I think it would be handy having an option in the dropdown menu of Proof Explorer to rerun a whole subtree.

Some sort of fast-forwarding to the last instruction of the subtree and execute the last as well.

Thanks,

Alberto

[Paolo Masci]

Done -- please try this new pre-release 1.0.56-delta: https://drive.google.com/file/d/1E1tEZNPbMwvDdpH3PGQigZjd7u1QXLGM/view?usp=sharing

In this new pre-release I have introduced the following changes:

- run-subtree in proof-explorer (see screenshot, the command is in the context menu opened when right-clicking on a node in proof-explorer)   

- moved show-proof icon from the editor toolbar to proof-explorer toolbar (see screenshot, the show-proof icon is next to the green check-mark icon)

- replaced the two icons in the editor toolbar for launching pvsio and pvsio-web with a single icon and a dialog for selecting the tool to be launched

Needless to say, feedback is welcome!

Thanks,

Paolo

 

[Alberto Ercolani]

Hello Paolo, I just tried the "run subtree" command.
I like the logic you employed for providing this command but I immediately ran into an unexpected situation. Say I have a proof tree of the shape:

1.
1.1
1.2
1.2.1
1.2.2
1.2.3 <

and want to execute the subtree 1.2.3 before any other. To do so, I would step through 1 and postpone 1.1, 1.2, 1.2.1, and 1.2.2. The execution of subtree 1.2.3 causes the execution of the whole proof, consequently executing all the branches I left behind. This specific use-case defeats the purpose of my request because causes the execution of all subtrees (siblings and possibly ancestors). This happens only when executing the deepest rightmost subtree.

Regards,

Alberto

[Paolo Masci]

Right... now I see why you suggested it's equivalent to fast-forward to the last instruction of the subtree + execute also that instruction.

This new pre-release 1.0.56-epsilon should do what you wanted: https://drive.google.com/file/d/1i7Wm4eTswgZQ4I4oKpXQEjwfwMGPAp-1/view?usp=sharing

Thanks,

Paolo

[Alberto Ercolani]

It does exactly what I requested, thanks!

Alberto

[Alberto Ercolani]

Hello Paolo,

I noticed that under "PVS Workspace Explorer" often the list of TCCs is incorrectly hidden. It happens independently from their status (proved, untried, unfinished.) Two show them one has to try to rerun their proof script until PVS-Code ceases to hide them.

Have a nice day,

Alberto

[Paolo Masci]

Thanks for reporting this issue. I have inspected the code for identifying TCCs, but I don't see anything clearly wrong -- can you share an example, or information on the structure of the TCCs that are not shown in workspace explorer (e.g., whether the TCCs have parameters, or special characters in the name, etc.). This would help me chase down the problem.

Thanks,

Paolo

[Alberto Ercolani]

That's interesting, I'm trying to reproduce the issue in a minimal context but it disappeared. I will post here a link to the minimal files required for triggering it.

Alberto

[Alberto Ercolani]

Ok, I have it.

https://mega.nz/folder/bn5klRJB#TCsakoUD73GzmNii3lbZgA

I also attach a picture of what I get after several attempts but the project on which I'm working triggers it consistently.

The problem here is that an unprovable TCC could be overlooked during the modelling phase and being spotted only later (or when it is too late during high-level lemmata proofs).

These 2 files will trigger the issue I encountered. To check its presence do the following:

1. Start a fresh instance of PVS-Code and open the folder workspace.

2. Typecheck "simulation.pvs", at this point the *.tccs files will be generated but 0/3 TCCs will be listed under PVS-Workspace Explorer.

3. Discharge all TCCS.

There's a <50% chance they will be listed as proved and then immediately hidden.

The bug is not deterministic, I had to replay these steps several times before I recognized it.

I first thought it was an interference due to GIT but I disabled it, so I think it is not the case.

Hope this code helps,

Alberto

[Paolo Masci]

This new pre-release 1.0.56-theta should resolve the problem with workspace explorer not refreshing the tccs:

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

This new pre-release features also several new proof-mate functionalities:

- compose proof sketches in proof-mate

- copy/paste commands/branches/trees between proof-mate and proof explorer

- run proof sketches directly in proof-mate

As always, feedback on these new functionalities is welcome!

Thanks,

Paolo