From 357d03db09f8b136b1c049d2c982902112d1cc49 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 8 Jun 2006 12:00:35 +0000 Subject: [PATCH] developments added --- matita/help/C/sec_gettingstarted.xml | 127 ++++++++++++++++++++++++++- 1 file changed, 126 insertions(+), 1 deletion(-) diff --git a/matita/help/C/sec_gettingstarted.xml b/matita/help/C/sec_gettingstarted.xml index 5f9dda35a..be9a5f22c 100644 --- a/matita/help/C/sec_gettingstarted.xml +++ b/matita/help/C/sec_gettingstarted.xml @@ -90,8 +90,133 @@ Authoring How to use developments - &TODO; + + A development is a set of scripts files that are strictly related (i.e. + they depend on each other). &appname; 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 &appname; 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. + +
The Developments window + + + + + Screenshot of the Developments window. + +
+ + Developments window buttons + New + + + To create a new Development the user needs to specify a name + + 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. + + + 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 &appname; 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 + + + + + + -- 2.39.2