Opened 17 years ago
Last modified 11 years ago
#38 new enhancement
Add automated testing framework
Reported by: | Owned by: | alex heneveld | |
---|---|---|---|
Priority: | critical | Milestone: | |
Component: | 1:pg-eclipse | Keywords: | |
Cc: |
Description (last modified by )
This is desperately wanted. We need a testing framework which allows testing of underlying models as well as UI interactions. We can follow the same mechanisms as used in Eclipse and JUnit. At the moment, code improvements and refactorings are too haphazard leading to many regression failures.
Change History (4)
comment:1 Changed 17 years ago by
comment:2 Changed 17 years ago by
Owner: | changed from David Aspinall to alexh |
---|---|
Status: | new → assigned |
comment:3 Changed 16 years ago by
Description: | modified (diff) |
---|---|
Owner: | changed from alexh to alex heneveld |
Status: | assigned → new |
accepting. will draft proposal using cruisecontrol and junit.
at this point i'm thinking there are three types of tests we want:
via a suite-builder for pointing a unit test case at a collection of proofs, e.g. we write a test case which tests a theory file parses completely, then build a suite which runs that test case against all theories in a predefined "parseable proof files" collection (and another test case for theory files which execute completely, etc...)
extending a fixture to write a test script asserting behaviour in a single proof, e.g. to load A.thy, send "next" 3 times, assert we've just proven Foo, send undo, assert the lemma "Foo" is now undone.
normal units (pojo and ui-plugin), typically simpler than the above two; e.g. asserting that preferences load, that we can connect to the prover, that a theory file opens with the right prover, etc.
Remark: the unit test framework could be (optionally) independent of Isabelle by recording Isabelle's responses to a particular sequence of PGIP messages. This factors out regression failures that might be due to Isabelle changing (e.g. the infamous XML bugs introduced at the last moment in Isabelle 2005). We should test Isabelle separately: I've started on this inside the Isabelle tree itself but it is far from comprehensive at the moment.