+ 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
New+ To 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: +
all+ Build the whole development. +
clean+ Cleans the whole development. +
cleanall+ Resets 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.mo+ Compiles "scriptname.ma" +
+
Delete+ Decompiles the whole development and removes it. +
Build+ Compiles all the scripts in the development. +
Clean+ Decompiles the whole development. +
Publish+ All 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). +
Close+ Closes 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. +