X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_gettingstarted.xml;h=b0c0a863e55e1a8c9a69602730f360fa48d3bf30;hb=c78a913e4e45c1128b59ca8be9d53fc0c36fc9e0;hp=0066449b0294618bff6953768c8d80f40c519350;hpb=e43d7e9c2acfa6d1c74838ba15589833cfc275fc;p=helm.git diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml index 0066449b0..b0c0a863e 100644 --- a/helm/software/matita/help/C/sec_gettingstarted.xml +++ b/helm/software/matita/help/C/sec_gettingstarted.xml @@ -88,133 +88,60 @@ Authoring - - How to use developments + + How to compile a script - 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. + Scripts are compiled to base URIs. Base URIs are of the form + "cic:/matita/path" and are given once for all for a set + of scripts using the "root" file. - 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 - - - - - + A "root" file has to be placed in the root of a script set, + for example, consider the following files and directories, and + assume you keep files in "list" separated from files + in "sort" (for example the former directory may contain + functions and proofs about lists, while latter sorting algorithms + for lists): + + To be able to compile properly the contents of "list" + a file called root has to be placed in it. The file should be like + the following snippet. + + This file tells &appname; that objects generated by + "list.ma" have to be placed in + "cic:/matita/mydatastructures/list" while + objects generated by + "swap.ma" have to be placed in + "cic:/matita/mydatastructures/utils/swap". + + + Once you created the root file, you must generate a depend file. + Enter the "list" directory (the root of yuor file set) + and type "matitadep". Remember to regenerate the depend file + every time you alter the dependencies of your files (for example + including other scripts). + You can now compile you files typing "matitac". + + + To compile the "sort" directory, create a root file + in "sort/" like the following one and then run + "matitadep". + + The include_paths field can declare a list of paths separated by space. + Please omit any "/" from the end of base URIs or paths. + The authoring interface