]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/help/C/sec_install.xml
comment out an incomplete proof
[helm.git] / matita / help / C / sec_install.xml
index 84ce6f0d6926d8efc0ac1cbc0605b31a9b0a740a..35d7ff900a6d3771b9b1b00825533493603710f6 100644 (file)
 
        </variablelist> </para>
 
+    </sect3>
+
+    <sect3 id="build_instructions">
+      <title>Instructions</title>
+
+      <para> Once you get the source code the installations steps should be
+       quite familiar.</para>
+
+      <para> First of all you need to configure the build process executing
+       <userinput>./configure</userinput>. This will check that all needed
+       tools and library are installed. You may need to pass on the command
+       line some of the parameters riported below:
+
+       <variablelist>
+         <title><application>configure</application> parameters</title>
+
+         <varlistentry>
+           <term>&TODO;</term>
+           <listitem><para>&TODO;</para></listitem>
+         </varlistentry>
+
+       </variablelist>
+
+      </para>
+
+      <para> Then you will manage the build process using <application><ulink
+           type="http"
+           url="http://www.gnu.org/software/make/">make</ulink></application>
+       as usual. Below are reported the targets you have to invoke in sequence
+       to build and install.
+
+       <variablelist>
+         <title><application>make</application> targets</title>
+
+         <varlistentry>
+           <term><userinput>world</userinput></term>
+           <listitem>
+             <para>builds components needed by &appname; and &appname; itself
+               (in bytecode only or in both bytecode and native code depending
+               on the availability of the OCaml native code compiler) </para>
+           </listitem>
+         </varlistentry>
 
+         <varlistentry>
+           <term><userinput>library</userinput></term>
+           <listitem>
+             <para>uses the (just built) <application>matitac</application>
+               compiler to build the &appname; standard library. </para>
+             <para>For this step you will need a working SQL database (for
+               indexing the standard library while you are compiling it). See
+               &TODO; for instructions on how to set it up.</para>
+           </listitem>
+         </varlistentry>
+
+         <varlistentry>
+           <term><userinput>install</userinput></term>
+           <listitem>
+             <para>installs &appname; related tools, standard library and the
+               needed runtime stuff in the proper places on the filesystem
+             </para>
+           </listitem>
+         </varlistentry>
+
+       </variablelist>
+
+      </para>
+      
     </sect3>
 
   </sect2>