Welcome to the minimalist preliminary website of Levity.
If you have this address, you already know what it is.
(A prototype proof refactoring tool for Isabelle by Marcel Ruegenberg.)
The code can be obtained using hg clone http://home.in.tum.de/~ruegenbe/levity/levity
Alternatively, a (probably not up-to-date) snapshot can be obtained here.
Even though this project is the result of my thesis, which I have now handed in, the current state of the repository diverges from how it was at the time when I handed in the thesis. To obtain the "original" code, use the Mercurial/Hg client of your choice to find the correspondingly tagged revision.
Changes from the handed-in version:
- Various fixes that had to to with slightly unexpected behaviour in Isabelle/Scala. Resulting in the rename refactoring now working.
- Various refinements and tuning
- Implemented basic version of levitation, including (theorem) dependency tracking
Still missing and limitations:
- Possible infinite loop when parsing refactoring comments: When a refactoring does not remove the comment which triggered it (it should, however), the refactoring is applied again and again. The two refactorings that are currently implemented should, however, not have this problem.
Status:
- The tool is at the moment not ready for production. While no work has been done in the last few months, I plan to start working on Levity again very soon. In the meantime, feedback, bug reports and suggestions are appreciated.
Examples and additional refactorings will be available soon.
The Thesis
Thesis Talk
Slides from a short talk about Levity. Might be of only limited value by themselves.
download
Contact
mail to: ruegenbe [at] in [dot] tum [dot] de