Matita interactive theorem prover (or proof assistant), a tutorial introduction: installation.

Matita is an experimental proof assistant under development at the Computer Science Department of the University of Bologna.

 

Matita is based on the Calculus of (Co)Inductive Constructions (a derivative of Calculus of Constructions), and is compatible, to some extent, with Coq. It is a reasonably small and simple application, whose architectural and software complexity is meant to be mastered by students, providing a tool particularly suited for testing innovative ideas and solutions. Matita adopts a tactic based editing mode; (XML-encoded) proof objects are produced for storage and exchange.

 

At the same time, proofs are an integrated part of the formalism, allowing, via the Curry Howard isomorphism, a smooth interplay between specification and reasoning: proofs are objects of the language, and can be treated as normal data, naturally leading to a programming style akin to proof-carrying-code, where chunks of software come equipped with proofs of (some of) their properties.

 

Matita is currently adopted in the European Union "Certified Complexity" Project CerCo for the formal verification of a complexity-preserving compiler from a large subset of C to a microcontroller assembly of the kind traditionally used in embedded systems.

Matita vs Coq.

The system shares a common look&feel with the Coq proof assistant and its graphical user interface. The two systems have variants of the same logic, close proof languages and similar sets of tactics. From the user point of view the main lacking features with respect to Coq are:

 

    proof extraction;

    an extensible language of tactics;

    automatic implicit arguments;

    several ad-hoc decision procedures;

    several rarely used variants for most of the tactics;

    sections and local variables.

Still from the user point of view, the main differences with respect to Coq are:

    the language of tacticals that allows execution of partial tactical application;

    the unification of the concept of metavariable and existential variable;

    terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;

    ambiguous terms are disambiguated by direct interaction with the user;

    theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation.

 

Installation.

Using the LiveCD

In the following, we will assume you have installed virtualbox for your platform and downloaded the .iso image of the LiveCD

 

Creating the virtual machine

Click on the New button, a wizard will popup, you should ask to its questions as follows

 

1. The name should be something like Matita, but can be any meaningful string.
2. The OS type should be Debian
3. The base memory size can be 256 mega bytes, but you may want to increase it if you are going to work with huge formalizations.
4. The boot hard disk should be no hard disk. It may complain that this choice is not common, but it is right, since you will run a LiveCD you do not need to emulate an hard drive.

    

   Now that you are done with the creation of the virtual machine, you need to insert the LiveCD in the virtual cd reader unit.

The brand new virtual machine

 

Click on CD/DVD-ROM (that should display something like: Not mouted). Then click on mount CD/DVD drive and select the ISO image option. The combo-box should display no available image, you need to add the ISO image you downloaded from the Matita website clicking on the button near the combo-box. to start the virtual machine.

 

Mounting an ISO image

 

In the newely opened window click the Add button

Choosing the ISO image

A new windows will pop-up: choose the file you downloaded (usually matita-version.iso) and click open.

 

Choosing the ISO image

Now select the new entry you just added as the CD image you want to insert in the virtual CD drive. You are now ready to start the virtual machine.

 

Sharing files with the real PC

The virtual machine Matita will run on, has its own file system, that is completely separated from the one of your real PC (thus your files are not available in the emulated environment) and moreover it is a non-presistent file system (thus you data is lost every time you turn off the virtual machine).

 

Virtualbox allows you to share a real folder (beloging to your real PC) with the emulated computer. Since this folder is persistent, you are encouraged to put your work there, so that it is not lost when the virtual machine is powered off.

 

The first step to set up a shared folder is to click on the shared folder configuration entry of the virtual machine.

 

Set up a shared folder

Then you shuld add a shared folder clicking on the plus icon on the right

 

Choosing the folder to share

Then you have to specify the real PC folder you want to share and name it. A reasonable folder to share is /home on a standard Unix system, while /Users on MaxOSX. The name you give to the share is important, you should remember it.

Naming the shared folder

Once your virtual machine is up and running, you can mount (that meand have access to) the shared folder by clicking on the Mount VirtualBox share icon, and typing the name of the share.

Using it from the virtual machine

A window will then pop-up, and its content will be the the content of the real PC folder.

 

Installing from sources.

Install Matita from the sources is hard, you have been warned!

 

Getting the source code.

You can get the Matita source code in two ways:

1. go to the download page and get the latest released source tarball;

2. get the development sources from our SVN repository. You will need the components/ and matita/ directories from the trunk/helm/software/ directory, plus the configure and Makefile* stuff from the same directory.

   In this case you will need to run autoconf before proceding with the building instructions below.

Requirements.

In order to build Matita from sources you will need some tools and libraries. They are listed below.

 

Note for Debian (and derivatives) users:

If you are running a Debian GNU/Linux distribution, or any of its derivative like Ubuntu, you can use APT to install all the required tools and libraries since they are all part of the Debian archive.

apt-get install ocaml ocaml-findlib libgdome2-ocaml-dev liblablgtk2-ocaml-dev liblablgtkmathview-ocaml-dev liblablgtksourceview-ocaml-dev libsqlite3-ocaml-dev libocamlnet-ocaml-dev libzip-ocaml-dev libhttp-ocaml-dev ocaml-ulex08 libexpat-ocaml-dev libmysql-ocaml-dev camlp5

An official debian package is going to be added to the archive too.

 

Required tools and libraries

OCaml

the Objective Caml compiler, version 3.09 or above

Findlib

OCaml package manager, version 1.1.1 or above

OCaml Expat

OCaml bindings for the expat library

LablGTK

OCaml bindings for the GTK+ library , version 2.6.0 or above

GtkSourceView , LablGtkSourceView

extension for the GTK+ text widget (adding the typical features of source code editors) and its OCaml bindings

Ocamlnet

collection of OCaml libraries to deal with application-level Internet protocols and conventions

ulex

Unicode lexer generator for OCaml

CamlZip

OCaml library to access .gz files

 

Compiling and installing.

Once you get the source code the installations steps should be quite familiar.

First of all you need to configure the build process executing ./configure. This will check that all needed tools and library are installed and prepare the sources for compilation and installation.

 

Quite a few (optional) arguments may be passed to the configure command line to change build time parameters. They are listed below, together with their default values:

 

configure command line arguments

--with-runtime-dir=dir

(Default: /usr/local/matita) Runtime base directory where all Matita stuff (executables, configuration files, standard library, ...) will be installed

--enable-debug

(Default: disabled) Enable debugging code. Not for the casual user.

Then you will manage the build and install process using make as usual. Below are reported the targets you have to invoke in sequence to build and install:

make targets

world

builds components needed by Matita and Matita itself (in bytecode or native code depending on the availability of the OCaml native code compiler)

install

installs Matita related tools, standard library and the needed runtime stuff in the proper places on the filesystem.

If you liked this article, subscribe to the feed by clicking the image below to keep informed about new contents of the blog:

Do you consider this article interesting? Share it on your network of Twitter contacts, on your Facebook wall or simply press "+1" to suggest this result in searches in Google, Linkedin, Instagram or Pinterest. Spreading content that you find relevant helps this blog to grow. Thank you!

Share on Facebook Share on Twitter Share on Google Plus

About Hugo

Ubuntu is a Linux distribution that offers an operating system predominantly focused on desktop computers but also provides support for servers. Based on Debian GNU / Linux, Ubuntu focuses on ease of use, freedom in usage restriction, regular releases (every 6 months) and ease of installation.