HELM: an Hypertextual Electronic Library of Mathematics
Last update: 02 Feb 2000
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
and the ocaml-* stuff
(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):
- export MATHENGINECONF=/usr/local/etc/helm/helm-math-engine-configuration.xml
- export PATH=/usr/local/bin:$PATH
- export LD_LIBRARY_PATH=/usr/local/lib:$LD_LIBRARY_PATH
- In a first window run "http_getter.pl"
- In a second one run "start-xaland". If something goes wrong, then
create a local copy of start-xaland and edit it to reflect the path
of your local copy of jdk1.3, xaland.jar and xerces.jar.
- In the last one run "mmlinterface.opt", the actual GTK interface.
If the two trees you will see are empty, press "Update" to create
you up-to-date vision of the universe. Then browse freely the library.