Typecheck time

[Giulia Sindoni]

Hello everyone,

I have a question on the Typecheck phase of a pvs theory.

I have two pvs theories that have very similar structure: they use same syntax and types, they import the same theories, the main theorem has to be proved using the same strategy. The first theory is ~176KB, the other one is ~108KB.

Now, at typecheck time (running pvs in batch mode I can get a measure of this) I have that that bigger theory is typechecked in ~14secs. The smaller theory is typechecked in ~250sesc (running the experiments of course on the same machine).

I'm scratching my head on this, as as I said I can't find any obvious difference between the two theories that would cause this increase in the  time needed to typecheck, and the slightly smaller one takes actually considerably more time at the typechecking stage (so it does't seems to be due to the size of the theory).

Giulia