[Date Prev][Date Next] [Chronological] [Thread] [Top]

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



Could somebody help him?

A.T.

-------- 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.