A development is a set of scripts files that are strictly related (i.e. they depend on each other). Matita is able to automatically manage dependencies among the scripts in a development, compiling them in the correct order.
The include statement can be performed by Matita only if the mentioned script is compiled. If both scripts (the one that includes and the included) are part of the same development, the included script (and recursively all its dependencies) can be compiled automatically. Dependencies among scripts belonging to different developments is not implemented yet.
The "Developments..." item the File menu (or pressing Ctrl+D) opens the Developments window.
Developments window buttons
NewTo create a new Development the user needs to specify a name[1] and the root directory in which all scripts will be placed, eventually organized in subdirectories. The Development should be named as the directory in which it lives. A "makefile" file is placed in the specified root directory. That makefile supports the following targets:
allBuild the whole development.
cleanCleans the whole development.
cleanallResets the user environment (i.e. deleting all the results of compilation of every development, including the contents of the database). This target should be used only in case something goes wrong and Matita behaves incorrectly.
scriptname.moCompiles "scriptname.ma"
DeleteDecompiles the whole development and removes it.
BuildCompiles all the scripts in the development.
CleanDecompiles the whole development.
PublishAll the user developments live in the "user" space. That is, the result of the compilation of scripts is placed in his home directory and the tuples are placed in personal tables inside the database. Publishing a development means putting it in the "library" space. This means putting the result of compilation in the same place where the standard library lives. This feature will be improved in the future to support publishing the development in the "distributed library" space (making your development public).
CloseCloses the Developments window
[1] The name of the Development should be the name of the directory in which it lives. This is not a requirement, but the makefile automatically generated by matita in the root directory of the development will eventually generate a new Development with a name that follows this convention. Having more than one development for the same set of files is not an issue.