[mizar] Re: installing mmlquery locally

[Jesse Alama <alama@stanford.edu>]

Hi Krzysztof,

Krzysztof Retel <retel@macs.hw.ac.uk> writes:

> I present one possible installation of MML Query engine locally.
>
> First you have to download:
> 1. kernel.tgz ,
> 2. present.tgz,
> 3. 4.76.859.tgz - current database for MML Query
>
> Untar all these files in directory e.g. MMLQ. We will install MML
> Query in directory: megrez, on the path: /home/user_name/
> 1. Once you untar all the files, move directories 'kernel' and
> present' into directory 'megrez'
>
> 2. Changed a first path in a file 'directories.pl' (in directory:
> megrez/kernel') into your installation path: i.e.
> $megrez_cvsroot = '/home/user_name/megrez';
>
> 3. Changed a directory path (line 11) in a file 'mmlquery' (directory:
> megrez/kernel') into a full path:
> ####### Change directory below if necessary
> require '/home/user_name/megrez/kernel/directories.pl';
> #######
>
> 4. Create a directory named: 'query' inside directory 'megrez'.
> 5. Move untar database directory '4.76.859' into: 'megrez/query'.
> 6. Create symbolic link inside: 'megrez/query', i.e.
> ln -s 4.76.859 current
> 7. Add symbolic link to: 'megrez/kerenel/mmlquery' in your executables.
>
> That's it.
> You can run mmlquery on top level by typing:
> mmlquery
> Once it run you should receive something similar to:
> retel@lxultra9:/data0/retel/megrez$ mmlquery
> MML Query, version 1.3.03, Copyright (c) 2001-2004, Grzegorz Bancerek
> Standard presentation
> mmlquery>
>
> To check if the current database is properly link type for instance a
> query: list of func from article NAT_1;
> You should received the following:
> mmlquery> list of func from article NAT_1;
> QUERY: 'list of func from article NAT_1'
> 2 element(s)
> NAT_1:func 1
> NAT_1:func 2
> mmlquery>
>
> This means everything works fine.
>
> By the way, you can use mmlquery engine on the emacs side (if you want
> to work locally, there is also an option to send queries into a remote
> server and view the answers through a web-browser).
> To do that:
> 1.you have to to install GAB
> (http://merak.pb.bialystok.pl/mmlquery/downloads/gab-4.76.759.tgz),
> and define properly a path to the unpacked GABs while customising
> Mizar Mode.
> 2. you have to set up properly the Mizar MMLQuery group while
> customising Mizar Mode.

Your instructions worked just fine -- thanks!  (I was surprised at how
huge the directory 4.76.959 was when unpacked -- almost two GB!)

Thanks again,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*14: Too many terms in an inference (http://www.mizar.org)