Opened 17 years ago

Last modified 11 years ago

#38 new enhancement

Add automated testing framework

Reported by: David Aspinall <da+pgtrac@…> Owned by: alex heneveld
Priority: critical Milestone:
Component: 1:pg-eclipse Keywords:
Cc:

Description (last modified by alex heneveld)

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 anonymous

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.

comment:2 Changed 17 years ago by David Aspinall

Owner: changed from David Aspinall to alexh
Status: newassigned

comment:3 Changed 16 years ago by alex heneveld

Description: modified (diff)
Owner: changed from alexh to alex heneveld
Status: assignednew

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.

comment:4 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.1.0

Milestone PG-Eclipse-1.1.0 deleted

Note: See TracTickets for help on using tickets.