Menu
▾
▴
#615 Cannot import a theory in another theory
Nothing seems to work when importing a theory within another theory. In particular, deploying either theory induces a crash of the Theory POG in the deployed theory. Also, the operators defined in the theories are not usable within a machine.
These problems occur with Rodin 2.5 and Theory plug-in 1.3.2 on Mac OS X. They can be reproduced by importing the attached project in a fresh empty workspace. I'm also attaching a log of the errors encountered by the platform during my tries.
Error log
Thanks Laurent for the bug.
This bug originates from the absence of the MathExtensions project. Wrongly, the code assumes the presenece of such project. The issue is a NPE because the gloabl project is not present. Will be solved in next release.
If the MathExtensions project is created and Rodin restarted, the probelm disappears.
A sub-bug was that some extension of theories are ignored because they could not be parsed. The problem was the incorrect propagation of extensions when loading them (e.g., added extensions of theoy A to ff because theory B needs them to parse and type check its extensions).
The sub-bug is actually the real bug I initially intended to report, but could not reproduce myself with a fresh workspace.
Congratulations Issam, for finding out what was in my mind.