[Bug report] - Version 1.0.53

[Alberto Ercolani]

Good day Paolo,

i just noticed a bug in the last version of VSCode-PVS.

When a subtree is cut and pasted in Proof Explorer the paste process does not always end well because the pasted tree retains the old sub-trees numbering.

Suppose you have the tree 2.1.2.3 and want to cut and paste 1.2.3 inside 3.

Sometimes, the user gets 3.1.2.3 as expected, sometimes he/she gets something different, e.g. 3.2.2.1. The bug seems to arise when mutliple trees are cut and pasted in a sequence.

The wrong numbering prevents Proof Explorer from executing pasted subtrees that lie in place where they have been pasted. Eventually, in case the proof is completed they are automatically removed at save time, so they are mostly benign.

Regards,

Alberto

[Paolo Masci]

Thank you Alberto for reporting this problem.

Renaming proof branches turns out to be trickier than expected, and I need some time to double check that all use cases are correctly taken into account.

While I work on this, I have created a new pre-release vscode-pvs-1.0.54-beta that allows manual recover -- a proof branch can now be renamed in proof-explorer with the 'edit' function (right-click on the proof branch -> edit), and vscode will automatically rename all nodes belonging to the subtree of the renamed branch: https://drive.google.com/file/d/1o1MCQUhfYNWG-yPerROvK60rI9s2Q6hM/view?usp=sharing

This should do the trick for now.

This pre-release includes also some minor bug fixes for autocompletion and cut/paste operations in the prover console, and a new pvsio command vscode-plot(<expr>) that can be used in the prover console and pvsio to plot an expression (example expressions that can be plotted are at the end of this message).

Thanks,

Paolo

---

    %--------------------------------------------
    %% First example plots a list of ordered pairs
    %  as a scatter plot.

    %  Use vscode-pvs((: (1/2, 2), (2, -1), (3, -2/3) :)) 

    %  to plot this expression from the prover console of from pvsio 

    %--------------------------------------------
    scatterplot: list[[real, real]] = (: (1/2, 2), (2, -1), (3, -2/3) :)

    %--------------------------------------------
    %% Second example plots a data series
    %  as a linear plot
    %--------------------------------------------
    series1: list[real] = (: 1, -1 , -2/3 :)

    %--------------------------------------------
    %% Third example of wanting to plot a tuple of
    %  two lists: the first one represents the
    %  horizontal coordinates, the second list
    %  represents the vertical coordinates
    %--------------------------------------------
    series2: [ list[real], list[real] ] = ((: 1/2, 2, 3 :), (: 1, -1, -2/3 :))

    %--------------------------------------------
    %% Fourth example, plots a tuple of
    %  four lists: the first one represents the
    %  horizontal coordinates, the second and third
    %  represent the vertical coordinates of two
    %  different series
    %--------------------------------------------
    multiseries: [ list[real], list[real], list[real], list[real] ] = (
      (: 1/2 , 2 , 3 :),  % x datapoints
      (: 1, -1 , -2/3 :), % y1 datapoints
      (: 0, -4.1 , -3 :), % y2 datapoints
      (: 5, 1 , -2 :)  % y3 datapoints
    )

[Alberto Ercolani]

Hello Paolo, thanks i will give it a shot.

In the meantime i found a simple workaround that could be useful to somebody else.

Just copy and cut the target subtree T and take advantage of ProofMate that holds a copy of T.

Move to the proper branch and through ProofMate rerun T that is consequently added.

Regards,

Alberto