X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_gettingstarted.xml;h=0066449b0294618bff6953768c8d80f40c519350;hb=c31e50505b5afd8fb53236bd5d500c225471eb9a;hp=b7b006590a39498117d0a7d267aaf6f293a66514;hpb=c9806f330ca060719dc21440b1b6d0dfe596f01f;p=helm.git diff --git a/matita/help/C/sec_gettingstarted.xml b/matita/help/C/sec_gettingstarted.xml index b7b006590..0066449b0 100644 --- a/matita/help/C/sec_gettingstarted.xml +++ b/matita/help/C/sec_gettingstarted.xml @@ -3,10 +3,224 @@ Getting started + If you are already familiar with the Calculus of (Co)Inductive + Constructions (CIC) and with interactive theorem provers with procedural + proof languages (expecially Coq), getting started with Matita is relatively + easy. You just need to learn how to type Unicode symbols, how to browse + and search the library and how to author a proof script. + How to type Unicode symbols - &TODO; + Unicode characters can be typed in several ways: + + Using the "Ctrl+Shift+Unicode code" standard Gnome shortcut. E.g. Ctrl+Shift+3a9 generates "Ω". + + Typing the ligature "\name" where "name" + is a standard Unicode or LaTeX name for the character. Pressing + "Alt+L" just after the last character of the name converts + the ligature to the Unicode symbol. This operation is + not required since Matita understands also the "\name" + sequences. E.g. "\Omega" followed by Alt+L generates + "Ω". + + Typing one of the following ligatures (and optionally + converting the ligature to the Unicode character has described before): + ":=" (which stands for ≝); "->" (which stands for + "→"); "=>" (which stands for "⇒"). + + + + + Browsing and searching + The CIC browser is used to browse and search the library. + You can open a new CIC browser selecting "New Cic Browser" + from the "View" menu of Matita, or by pressing "F3". + The CIC browser is similar to a traditional Web browser. + + Browsing the library + To browse the library, type in the location bar the absolute URI of + the theorem, definition or library fragment you are interested in. + "cic:/" is the root of the library. Contributions developed + in Matita are under "cic:/matita"; all the others are + part of the library of Coq. + Following the hyperlinks it is possible to navigate in the Web + of mathematical notions. Proof are rendered in pseudo-natural language + and mathematical notation is used for formulae. For now, mathematical + notation must be included in the current script to be activated, but we + plan to remove this limitation. + + + Looking at a proof under development + A proof under development is not yet part of the library. + The special URI "about:proof" can be used to browse the + proof currently under development, if there is one. + The "home" button of the CIC browser sets the location bar to + "about:proof". + + + + Searching the library + The query bar of the CIC browser can be used to search the library + of Matita for theorems or definitions that match certain criteria. + The criteria is given by typing a term in the query bar and selecting + an action in the drop down menu right of it. + + Searching by name + &TODO; + + + List of lemmas that can be applied + &TODO; + + + Searching by exact match + &TODO; + + + List of elimination principles for a given type + &TODO; + + + Searching by instantiation + &TODO; + + - &TODO; + + Authoring + + How to use developments + + 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 + + + + + + + + The authoring interface + &TODO; + + +