RepositoryManagement

Getting your code type-checked by other peoples edits

Developing Code

At very early stages of working on code you might want to not have it type-checked by everyone else; you might want to commit work in progress that does not type-check. For code that does not type-check yet, please put it in a directory with your own name, such as: src/dbg/lucas/

Testing Code

If you would like your code to be checked by other developers, for example to make sure they haven't broken something, or just to make sure you want it to typecheck (after the rest of IsaPlanner has been loaded) add a use call to:

src/test/ROOT.ML

Final Code

If you would like your code to be loaded as part of IsaPlanner, add it to:

src/theories/Pure/Pure_IsaP.thy

if it is theory independent, or:

src/theories/HOL/IsaP.thy

if it depends on HOL.

To move code from one place to another, you can use the subversion command:

svn mv OLD_LOCATION NEW_LOCATION