You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Right now, when printing entities filtered by --failed or --unproved, the decision if the entity's proof tree has failed attempts results in multiple calls to Has_Failed_Attempts, Is_Unproved which each cause more similar calls into all dependent objects. This should be optimized, so that such properties are only calculated once.
* All concerned entities are now derived from Entity.T.
* Less ugly template file names.
* All entities are in the same tree now
* Enable Assertion checks.
* Enabled paralled compilation ('-j0' switch).
Which bears the question... when we are collecting the proof items, we now already know if the item would get filtered. So maybe don't add these to the tree at all. That should greatly simplify the output code.
Right now, when printing entities filtered by
--failed
or--unproved
, the decision if the entity's proof tree has failed attempts results in multiple calls to Has_Failed_Attempts, Is_Unproved which each cause more similar calls into all dependent objects. This should be optimized, so that such properties are only calculated once.For further discussion see this wiki-page
The text was updated successfully, but these errors were encountered: