KrzysztofRetel's instruction for local installation of MmlQuery

I present one possible installation of MML Query engine locally.

First you have to download (from http://merak.pb.bialystok.pl/mmlquery/downloads/):

1. kernel.tgz ,
2. present.tgz,
3. 4.76.959.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/

• Once you untar all the files, move directories 'kernel' and 'present' into directory 'megrez'
• Change the first path in the file 'directories.pl' (in directory: 'megrez/kernel') into your installation path: i.e.

  $megrez_cvsroot = '/home/user_name/megrez';

• Change the 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';
#######

• Create a directory named: 'query' inside directory 'megrez'.
• Move untar-ed database directory '4.76.959' into: 'megrez/query'.
• Create symbolic link inside: 'megrez/query', i.e.

  ln -s 4.76.959 current

• Add symbolic link to: 'megrez/kernel/mmlquery' in your executables.

That's it. You can run mmlquery in shell top level by typing:

mmlquery

Once it runs, 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 linked, type for instance the following query:

 list of func from article NAT_1;

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>

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.959.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.
3. from Menu, select Mizar -> MML Query -> Query window (or just press C-c C-q in a .miz buffer)
4. insert again e.g. "list of func from article NAT_1", and press C-c RET (if you press C-c C-c instead, your query will be sent to the web version instead, and the result will appear in a browser - this is the standard way for people who do not have MML Query installed locally)

-- JosefUrban - 05 Mar 2007