nasa/vscode-pvs

Problem with propax

Closed this issue · 1 comments

BrunoDutertre commented

Hi all

I've started playing with the VSCODE for PVS. I'm mostly happy with it, but some things
that. can be proved with regular PVS (from emacs) don't get proved from VScdoe.
This is related to the (propax) rule.

Here's an example:

simple: THEORY
  BEGIN 
    test: LEMMA TRUE
  END simple

Then when I try to prove test, the session looks like this:

Starting new prover session for simple@test

Installing rewrite rule sets.singleton_rew (all instances)

test :

  ├───────
{1}   TRUE

 >> (propax)

No change on: (propax)
Error: Proof-command error



 >> (assert)

No change on: (assert)
Error: Proof-command error
pmasci commented

Thank you Bruno -- we have now fixed this problem in vscode-pvs 1.0.26 (which we will be releasing soon)

  • 👍1