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

Re: [mizar] PVS GPLed

On Fri, Sep 12, 2008 at 11:57:23AM -0700, Chisolm, Bill wrote:

> I, for one, would look at the source code if it were available.  There 
> seems to be a lot of essential information about Mizar that is not 
> written down anywhere.  I have learned some of that unwritten knowledge 
> by reading the mailing list, and by asking people.  I have learned even 
> more of it by doing experiments with Mizar.  But I still have questions
> about Mizar that I can't answer.  If the source code were available, I 
> would look there for an answer whenever Mizar does something that I 
> just don't understand.
> 
> As one example, I would like to understand the rules that Mizar uses 
> for parsing a Term-Expression.  This is not just a theoretical question 
> about the Mizar language.  It is a practical question, because anyone 
> who reads the MML will encounter many, many expressions whose correct 
> structure is hard to recognize.  How can a human reader predict which 
> way Mizar will parse an expression?

In such case I consult Josef's xml version of MML which answers all such
questions (OK, modulo weird links at times).

While I am not planning to study Mizar sources, I am strongly in favour that
the authors make the sources open.  I can understand that the authors may be
ashamed of their coding but if the sources are open then some energetic
volunteers will clean the code pretty soon (and preserve the semantics too).

Cheers,

-- 
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr