X-Logic Source Release Information
Overview
The content of an X-Logic source release, how to prepare for and then build and install, and what little you can then do with it.
Current version of sources, what's in it and what's it good for.
What other software you need and what you should do before building.
How to do the actual build and install.
Well, at this stage its only good for doing more of the same. i.e. further developments to the various theories and libraries so far in progress.
About the Sources
Current version of sources, what's in it and what's it good for.
name and version
This is available as the file "x-logic-src.1.0.tar.gz". It should really be version "0.0.0.1", or maybe "-0.1".
content
The content of this file is the X-Logic source tree as exported from cvs after running "autoconf". Note that this is not the source tree you find in cvs on SourceForge which does contain some rubbish but is not currently being kept up to date (since I find that extremely hard to do for reasons I won't go into, and for some time to come I don't think anyone will miss it).
what it does
This contains sources for the website and various bits of hackery which make it possible to build the web site from the sources. The sources are mainly XML but contain embedded SML and HOL. Also some CSS and XSLT style sheets. There are some PERL and BASH scripts which are used in building the website from the sources.
re-use
It is intended that X-Logic will provide re-usable facilities for building web sites including fancy formal notations from XML literate scripts. However, the re-usability of this release is doubtful. I will be using this stuff for the OpenBrand.org website and that might result in a more usable system. Meanwhile, the sources attempt to install themselves, and the web site, if you do a make install. At this stage its a bit of a mess, but it does work insofar as it does build the X-Logic web site, running the ProofPower theorem prover in the process and incorporating theory listings from ProofPower after checking all the specifications and proof scripts.
Preparing to Build
What other software you need and what you should do before building.
What else you would need to build the site?

This list is probably not exhaustive, and you will probably find that running ./configure doesn't yet warn you of all the things you need that are missing. The configure script is deliberately written to carry on when it finds something missing so that parts of the build process may be complete

If you are on a recent version of Linux then what you need extra is:

  1. Java SDK 1.1 for the XSLT software (unless you use a non-java implementation).
  2. A SAX XML parser, usually there is one with the XSLT processor so its maybe best to use that one.
  3. An XSLT processor. At 1.0 this should be James Clarke's XT, though it might work with one of the others with an appropriate change to the makefile.
  4. The XML/DOM Perl CPAN module.
  5. New Jersey Standard ML. Version 110.0.3 is required for ProofPower. Isabelle also required standard ML.
  6. ProofPower HOL (PPHol and PPTex are the only essential components for the build)
  7. The fxp functional XML parser in SML with the fxplib library (version 1.4.1)
Isabelle, though not required for the build, is used for one of the models (xl metamodel 2), so if you wanted to tinker with that model you would need Isabelle, though no output from Isabelle is actually included in the web site.

preparing to build
In theory, to do the whole build and "install" the results all you need to do is this. It is not necessary or advisable to do the build or install process as user root. As far as I no there would be no harm done, but why take the risk?
  1. Get your environment right, i.e. get all the software declared above as prerequisite and make sure it is all accessible via appropriate environment variables.
  2. In this build the locations of the fxp library (FXPLIB=/usr/local/fxp/lib), and of the code of the fxp applications (FXPAPPS=/usr/local/fxp/fxp-1.4.1/src/Apps) is hard coded in the file x-logic/build/vars.mk.in. You will have to edit this file if these values do not correspond to the place where you have installed it.
  3. Add to your relevant paths the software which will be installed by x-logic to build the x-logic site. The relevant directories are $prefix/bin/x-logic, $prefix/lib/x-logic and $prefix/share/x-logic where "$prefix" defaults to "/usr/local/" but can be set to something else by parameter to "./configure". The $prefix/bin/x-logic directory should be added to your PATH variable and the $prefix/lib/x-logic directory to your PERL5LIB variable.
  4. Either make sure that the user you will use for the build has permission to create the installation directories, or else create them from a user that has and give write permission to the user doing the build. The relevant directories are $prefix/bin/x-logic, $prefix/lib/x-logic and $prefix/share/x-logic (prefix as above). Probably easiest to do everything as user local and use the default prefix.
  5. Unpack the tar file
  6. cd into the x-logic directory
Build and Install
How to do the actual build and install.
build and install to /usr/local
Information will be written to /usr/local/bin/x-logic, /usr/local/lib/x-logic and /usr/local/share/x-logic, some of this during "make ibuild".
  1. cd into the x-logic directory
  2. autoconf
  3. ./configure
  4. make ibuild (optional)
  5. make install
build and install elsewhere
Information will be written to PREFIX/bin/x-logic, PREFIX/lib/x-logic and PREFIX/share/x-logic, some of this during "make ibuild".
  1. cd into the x-logic directory
  2. autoconf
  3. ./configure ==prefix=PREFIX
  4. make ibuild (optional)
  5. make install
What its good for
Well, at this stage its only good for doing more of the same. i.e. further developments to the various theories and libraries so far in progress.
what the build does

The build first installs the hackery which is used in building the web site, and then it builds the website and then it installs the web site. The locations for these are determined when you run ./configure, and will default to something appropriate to your environment. On my Linux RH 6.1 system these defaults are /usr/local/share/x-logic /usr/local/bin/x-logic /usr/local/lib/x-logic /usr/local/lib/perl5/x-logic. This means that you need to have permission to create all these directories. If you want to confine the possible damage from running this very flaky build process with those permissions, then you can change the prefix used to determine the directories by parameter to "./configure", e.g.:

./configure --prefix=/home/x-logic/xl-install

causes all these directories to be created under directory "/home/x-logic/xl-install", instead of under "/usr/local".

paths
The following paths need to be setup to pick up the X-Logic build software. "PREFIX" is whatever the autoconf default is (/usr/local on RH 6.1) or whatever you chose to set it to when you ran "configure".
  1. The PATH variable should include PREFIX/bin/x-logic
  2. The PERL5LIB should include PREFIX/lib/x-logic

up quick index © RBJ

$Id: sources.xml,v 1.1.1.1 2000/12/04 17:22:10 rbjones Exp $