Re: [mizar] [Fwd: Re: getting started with Mizar or some proof assistant]

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Just to have a clear answer here:

1. The MIZFILES variable has to be set before any work with Mizar. Using 
   Emacs before the variable is set is useless. If not sure, test the 
   Mizar installation first on command line with the "mizf" command,
   e.g.:  "cp $MIZFILES/mml/abcmiz_0.miz .; mizf abcmiz_0"

2. The instruction for installation of the Emacs mode distributed with 
   Mizar (file mizar.el) is in the beginning of that file (and yes, 
   it could be placed in the Mizar README or INSTALL file):

;;; Usage
;;
;; If you obtained this with your Mizar distribution, just append
;; the .emacs file enclosed there to your .emacs.

The default location of .emacs on Windows is described in the Emacs 
installation instructions at 
http://www.gnu.org/software/emacs/windows/faq3.html .

Josef


On Tue, 12 Apr 2005, Krzysztof Retel wrote:

> 
> > Could somebody help him?
> 
> I've sent him an email. I hope I will help him.
> And I think that it will be better (first of all) to show him some 
> examples that we were doing with our students.
> I will do that.
> 
> Krzysztof
> 
> >
> > -------- Original Message --------
> > Subject: 	Re: getting started with Mizar or some proof assistant
> > Date: 	Mon, 11 Apr 2005 17:01:08 EDT
> > From: 	Jasonc65@aol.com
> > To: 	trybulec@math.uwb.edu.pl
> >
> >
> >
> >In a message dated 4/11/2005 6:44:20 AM Eastern Standard Time, 
> >trybulec@math.uwb.edu.pl writes:
> >
> >> You have first install Mizar. The address is:
> >> 
> >> ftp://mizar.uwb.edu.pl/pub/system/current/
> >> 
> >> (where you live ? there are mirrors that may be better accessible for you)
> >> 
> >> With the instalation you will get the Mizar mode for GNU Emacs.
> >> 
> >
> >I have already done that.  That was what I was having trouble with.  I'm 
> >getting cryptic errors having to do with path variables.  And I can't find the 
> >autoexec.bat file in my computer and I forget where it goes.  All attempts to set 
> >the variable have failed because none of them gave me a permanent shell that 
> >was in effect when the code was being executed.  It is very frustrating having 
> >to search for files in rarely visited folders everytime I troubleshoot a 
> >software package that doesn't install from a wizard.  I was the other day having 
> >trouble with the MIZPATH variable.  The Mizar code for GNU Emacs simply isn't 
> >working on my system's present configuration and I have no clue how to fix it.  
> >I need foolproof instructions for in getting Mizar to work with Emacs now 
> >that they have been installed, including how to set up the .emacs file, the 
> >autoexec.bat file, the sytem variables, the Lisp functions, and everything else 
> >that needs to be set in order to make everything work.  Then I will need some 
> >sample proof file to run and exactly what keys to press in Emacs to make it run.
> >
> >  
> >
>