Plugin lists commented out code in the PVS workspace explorer, and tries to prove the commented out lemmas

[disteph]

I have a X.tccs file in my directory originating from a X.pvs file.
In the tccs file, which was automatically generated, I have

%% TCCs associated with theory [...]
%% This file was automatically generated by PVS, please **do not modify** by hand.
[...]: THEORY BEGIN

% The mapped-axiom TCC (at line 253, column 12) in decl nil for
	% term generated from IMPORTING 
	%  YYY
	%     {{ ... }}
	% IMP_[...]_TCC1: OBLIGATION
	%   EXISTS (x: [...]): TRUE
	  % untried
	  % IMP_[...]_TCC1: OBLIGATION
	%   EXISTS (x: [...]): TRUE

All of the lines above are commented out (except the line [...]: THEORY BEGIN); I assume it's just some information for the user. However, the PVS workspace explorer seems to look into those comments and list a tccs whose name is

% IMP_[...]_TCC1
(yes, the percent sign and the space seem to be part of the name string).
Then when trying to "play it" it fails with

Starting prover session for   % [...]_TCC1

Error: formula not found error
Additional details on the error can be inspected in the Output panel, on channel pvs-server.

and the Output panel doesn't show anything.
It looks to me like commented-out lines from the .tccs files should be ignored by whichever process is scanning the file to list the tccs in the PVS workspace explorer.

[pmasci]

Thank you Stephane.
I'm unable to reproduce the problem, could you please share the .pvs file?
Thanks

• Paolo

[pmasci]

I assume this problem has been resolved and the issue can be closed.
If that's not the case, please re-open the issue.

[aarondutle]

Closed as unreproducible. Please reopen if need be.