Re: [PVS-Help] Parsing after changing imported theory

[Sam Owre <owre@csl.sri.com>]

Hi Rob,

This is clearly a bug - could you send me the specs, so I can recreate and
fix it?

Thanks,
Sam


> From:    "R. Colvin" <robert@itee.uq.edu.au>
> Subject: [PVS-Help] Parsing after changing imported theory
> Date:    Tue, 26 Oct 2004 12:47:26 +1000
> To:      pvs-help@csl.sri.com
> 
> 
> Hi, when I'm editing a theory A that imports B (in a different
> file), if I edit B (and typecheck) then return to A, type checking A
> sometimes gives the error
> 
> Error: the assertion (singleton? resolutions) failed.
> 
> and I am prompted 
> 
> SPC-scroll: I-ignore, K-keep, ..... or B-break:
> 
> I usually just press 'I'.  Then I make some syntactic error in A
> which forces a re-parse of the file.  After that type checking works
> fine.
> 
> Is this perhaps something to do with the way I switch between files
> in PVS/emacs?
> 
> Thanks,
> Rob