The MINLOG System

• About
• Documentation
• Installation
• ProofGeneral
• Mailing List

ProofGeneral

• From source (Linux)
• Debian and Ubuntu
• From Subversion

How to install from source (Linux and MacOSX)

Download the SVN snapshot, uncompress it, and build it and fix the path:

At the command line, in the directory where you have downloaded the tar:

 > tar xvf proofgeneral-latest.tar.gz 

build minlog:

 > cd proofgeneral/minlog > make

Fix the PGHOME path bin/proofgeneral to fit to your ProofGeneral installation directory, e.g. ~/proofgeneral:

 > cd ..  
 > emacs bin/proofgeneral

Start ProofGeneral:

 > bin/proofgeneral

Set the minlog path variables of ProofGeneral:

 M-x customize-group minlog

Set all the paths to Minlog to the right directory, e.g. to ~/minlog, if you installed Minlog there. Save the changes for now and further sessions by clicking on the save buttons at the top of the customize-buffer.

You are now ready to use it. Open a .scm file of your choice.

How to install debian package (for Debian and Ubuntu)

With apt-get

Use the following apt-get source (either added to /etc/apt/sources.list or as additional package source in Synaptics or similar programs):

 deb http://www.math.lmu.de/~logik/download/debian ./
 deb-src http://www.math.lmu.de/~logik/download/debian ./

Update the package information and install the package:

 > apt-get update > apt-get install minlog proofgeneral proofgeneral-minlog

That's it! Startup ProofGeneral

 > proofgeneral

Open a Minlog proof script, i.e.

 C-x f /usr/share/doc/minlog/example/tutorial.scm 

You should see something like that:

Manually with dpkg

Download the newest debian packages from here: debian packages. It is called something like this:

 proofgeneral_3.5-4_all.deb
 proofgeneral-minlog_3.5-4_i386.deb

At the command line, in the directory where you have downloaded the proofgeneral packages:

 > sudo dpkg -i proofgeneral_3.5-4_all.deb
 > sudo dpkg -i proofgeneral-minlog_3.5-4_i386.deb

How to set up access to ProofGeneral through Subversion (svn)

Requirements

• you work localy as member of group 6

or

• you work remotely with internet connection
• you need svn installed on your local system (ask your system administrator)
• you need a local account as member of group 6 (ask Kenji Miyamoto)

How to set it up

If you work localy as member of group 6

Just go to a directory where you want to have the proofgeneral subdirectory, e.g.

 cd ~/development

and now do

 svn checkout file:///home/math/logik/proofgeneral/svn/trunk proofgeneral

That's all. It will create ~/development/proofgeneral and all its subdirectories.

Follow the steps on the "From source" section to build it, to fix the paths and run it with Minlog.

If you work remotely with internet connection

 svn checkout svn+ssh://<user>@math60.math.lmu.de/home/math/logik/proofgeneral/svn/trunk proofgeneral

where <user> must be your user name on math60. Thats all. It will ask you for your password on math60 and will create ~/development/minlog and all its subdirectories. See How to use it below.

Follow the steps on the "From source" section to build it, to fix the paths and run it with Minlog.

There are many more ways to use svn. Use "man svn" to find out more or see http://svnbook.red-bean.com/ for a good introduction

By Stefan Schimanski.