Authoring

How to compile a script

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.

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):

  list/
    list.ma (* depending just on the standard library *)
    utils/
      swap.ma (* including list.ma *)
  sort/
    qsort.ma (* including utils/swap.ma *)

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.

  baseuri=cic:/matita/mydatastructures

This file tells Matita 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".

  baseuri=cic:/matita/myalgorithms
  include_paths=../list

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

TODO