HELM: an Hypertextual Electronic Library of Mathematics

Last update: 02 Feb 2000

Contact: sacerdot@cs.unibo.it

Project HELM is aimed at developing the tools for the creation, maintainance and exploitation of a distributed hypertextual library of formal mathematical knowledge. In this page you can download a GTK interface to the libraries of Coq V7 once exported to XML.



19 december 2000

HELM 0.0.1 (alpha version) released


To install the GTK interface (and all the other tools on which it depends), you have to install all the RPM packages below and all the ones of which they depend on. You can find the GtkMathView stuff here and the ocaml-* stuff here (you will find only the .spec files and you will have to build the RPM packages yourself). The documentation about the GTK interface usage will appear as soon as possible. For now, if you want to use it, you have to do the following operations (after all the required RPM packages has been installed, of course):



Precompiled binaries