Documentation for IsaPlanner Developers
ML Text Editors
For developing IsaPlanner you need to write ML code. My suggestion is to use jEdit or emacs (not xemacs - the ml mode doesn't work properly for it!). On a Mac use I suggest eithercarbon emacs, or the recent version of AquaEmacs (which is variant of emacs 23.X). Also I use the development snapshot of ProofGeneral - I find it works a lot better for ML-coding and mac-interaction. I don't like the emacs/proof-general bundled with Isabelle2009-1 and Isabelle2009-2.
See UsefulEmacsSettings for my suggested emacs settings.
See UsefuljEditSettings. See also the jEdit plugin for PolyML, and also the jedit Isabelle plugin (isabelle jedit, but only on Isabelle-2009-2 or later).
Common Error Messages
Working in the wrong theory often leads to ERROR: Uninitialized theory data "IsaPlanner/cinfo", to fix this make sure your theory imports IsaP as well as whatever other theories you are wanting to use.
Debugging Tips: How to Hunt Code Monsters
/DebuggingReasoningTechniques has tips specific to IsaPlanner reasoning techniques and its tracing machinery.
/DebuggingSML has general ML debugging tips.
For Writing Code in IsaPlanner
/RepositoryManagement - how to manage the repository and get your code type-checked by other people's edits.
/NamingConventions - Please use these when you write IsaPlanner code
/CodingConventions - These too please
/CodeOrganisation - an outline to the IsaPlanner code
/HigherOrderMagic - there are lots of strange infix operators that do cool magic
Maps to the Dungeon
High Level Descriptions and Guides
/ReasoningStates - (type RState.T) snapshots of the proof planning process.
/ProofPlans - the underlying representation of proof plans
Foundational Library in IsaPlanner
/InstantiationEnvironment - working with instantiations
/GenericLibraries -- fresh name tables, collections sets etc. when to use what and why.
/Zippers -- allows nice navigation around terms; provides one-hole contexts.
/EmbeddingTerms -- describe the embedding of one term into another
/RippleMeasures -- Rippling is built as a collection of functors, this is how measures get constructed.
Foundational Libraries
/NameSet - sets of names, including creating new names and the usual set operations
/NameTab - tables with names as keys, can create new key entries
/BasicNames - with sets of names, tables, and such, all in one nice structure
/Renaming - renaming of names
/Names - BasicNames + Renaming
/ChangeNames - generalisation of renaming that allows renamed names to be of a different type.
Isabelle
Poly ML
Some coding tips for working with /PolyML.