TPHOLs becomes ITP (fwd)

[Josef Urban]

This seems to be good also for Mizar (I never quite understood how can Mizar
papers be presented at a higher order logic conference :-)

---------- Forwarded message ----------
Date: Wed, 27 Aug 2008 09:34:33 +0200
From: Tobias Nipkow <nipkow@...>
To: acl2@..., coq-club@...,
     hol-info@..., isabelle-users@...,
     metaprl-users@..., proofpower@..., pvs@...
Subject: [Hol-info] TPHOLs becomes ITP

The steering committee and business meeting of TPHOLs 2008 in Montreal
last week agreed on the following change of names: TPHOLs will become
ITP (Interactive Theorem Proving) not just in 2010 (as had already been
agreed) but that name change will become permanent after 2010. It was
felt that the broader scope of ITP is a more accurate reflection of the
actual focus of TPHOLs and its openness to other communities like ACL2
users.

Note that although ITP 2010 formally incorporates the TPHOLs and ACL2
Workshop series, no such commitment has been made beyond 2010; the new
agreement is only about changing the name.

This is not a formal vote, but if you have strong objections to this
decision, please address them to the TPHOLs Steering Committee by
replying to this email. We will try to take your arguments into account.

Tobias Nipkow
TPHOLs Steering Committee chair

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
hol-info@...
https://lists.sourceforge.net/lists/listinfo/hol-info

[Josef Urban]

Hi,

I just noted that PVS has been licensed under GPL since Dec 2006:
http://pvs.csl.sri.com/mail-archive/pvs-announce/msg00007.html .

Mizar is thus the last major proof assistant whose sources are closed, and
licensing unclear.

Josef

[Freek Wiedijk]

Hi Josef,

>Mizar is thus the last major proof assistant whose sources
>are closed, and licensing unclear.

Mizar also is one of the few major proof assistants that has
not been implemented using a functional programming language.
Mizar is a little bit different in many respects.

I was in Japan recently, visiting Nobuki Takayama, and
he told me that these licensing issues had been a reason
for him not to put Mizar on his KNOPPIX/Math DVD (see
<http://www.knoppix-math.org/>; it's a DVD with all kinds
of mathematical software packages that you can boot from
and then everything will just work.)

He told me that with a special arrangement it still could
be on the DVD after all, and that he might contact the Mizar
group about it.  But then it won't be on the version that you
can download (because that only can have "free" software),
but just on the physical disks that have been burned.

Personally I don't care so much for Mizar being open source.
I won't understand the sources anyway :-)  (I do sometimes
wonder whether if I dug into the sources, I could give
Mizar empty types.  But I guess not.)

Freek

[Josef Urban]

Hi Freek,

On Fri, 12 Sep 2008, Freek Wiedijk wrote:

>> Mizar is thus the last major proof assistant whose sources
>> are closed, and licensing unclear.
>
> I was in Japan recently, visiting Nobuki Takayama, and
> he told me that these licensing issues had been a reason
> for him not to put Mizar on his KNOPPIX/Math DVD (see
> <http://www.knoppix-math.org/>; it's a DVD with all kinds
> of mathematical software packages that you can boot from
> and then everything will just work.)

The same e.g. with David Wheeler's listing:
http://www.dwheeler.com/essays/high-assurance-floss.html#theoremprovers .
Non-FLOSS software is plainly ignored.

Josef

[Chisolm, Bill]

Josef Urban wrote:
> Mizar is thus the last major proof assistant whose sources are closed,
> and licensing unclear.

Freek Wiedijk wrote:
> Personally I don't care so much for Mizar being open source.
> I won't understand the sources anyway :-)

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?

It's not enough just to just consult the Mizar grammar on the web:
  _http://www.mizar.org/language/pages/term-expression.html
That grammar is ambiguous.  It allows multiple different ways of
parsing any particular expression.  The grammar does not tell us how
to apply the precedence levels that are specified in the mml.vct file.
It also does not tell us that there is even more background information
which is needed to parse an expression correctly.  The parser also must
know how many left and right operands each functor can accept,
under each functor definition that is available to the article.
The correct parse tree can actually be *changed* by adding or removing
functor definitions.  As a new user, I had to learn these unexpected
facts by trial and error.

This kind of information about Mizar is just not written anywhere, but
a person must know these things in order to be successful at writing
Mizar articles.  If the world were perfect, then these things would all
be neatly written in a well-organized reference manual.  However, that
manual may never be completed in our real world.

Opening up the source code will not be a substitute for the
comprehensive manual that has never been written.  But it will enable
some Mizar users to independently find answers to some of their
questions.  I am one user who would find that very helpful.

Bill Chisolm

[Piotr Rudnicki]

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

[Josef Urban]

On Fri, 12 Sep 2008, Piotr Rudnicki wrote:

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

But having available the correct parse of a term only answers one
question, it may still be difficult to guess the algorithms. And it is - I
tried quite hard to reverse-engineer the various algorithms before I had
Mizar sources, and never got it right. Others have tried and failed too.
Exercise in futility, stealing precious time of the (relatively few)
people who wanted to do some work with Mizar, and further decimating their
numbers.

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

And possibly even document Mizar :-). I never heard a serious explanation
of why the sources are closed, and as far as I know there was never a
serious rational discussion about it. I really would like to know the
reasons, and have a serious discussion about this. One thing I hear quite
often is that Mizar is badly documented, because the developer team is
small. Guess why?

Josef

[Jesse Alama]

"Chisolm, Bill" <bill.chisolm@...> writes:

> Josef Urban wrote:
>> Mizar is thus the last major proof assistant whose sources are closed,
>> and licensing unclear.
>
> Freek Wiedijk wrote:
>> Personally I don't care so much for Mizar being open source.
>> I won't understand the sources anyway :-)
>
> 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?
>
> It's not enough just to just consult the Mizar grammar on the web:
>   _http://www.mizar.org/language/pages/term-expression.html
> That grammar is ambiguous.  It allows multiple different ways of
> parsing any particular expression.  The grammar does not tell us how
> to apply the precedence levels that are specified in the mml.vct file.
> It also does not tell us that there is even more background information
> which is needed to parse an expression correctly.  The parser also must
> know how many left and right operands each functor can accept,
> under each functor definition that is available to the article.
> The correct parse tree can actually be *changed* by adding or removing
> functor definitions.  As a new user, I had to learn these unexpected
> facts by trial and error.
>
> This kind of information about Mizar is just not written anywhere, but
> a person must know these things in order to be successful at writing
> Mizar articles.  If the world were perfect, then these things would all
> be neatly written in a well-organized reference manual.  However, that
> manual may never be completed in our real world.
>
> Opening up the source code will not be a substitute for the
> comprehensive manual that has never been written.  But it will enable
> some Mizar users to independently find answers to some of their
> questions.  I am one user who would find that very helpful.

I'm not sure whether I've mentioned this before on the list, but in my
view keeping mizar's source code closed undermines one of the
philosophical goals of proof-checking, which is to make explicit as much
of the logical structure of a piece of mathematics as possible.  It's
not enough to make the full text of the MML available, nor is my point
negated by the existence of SUM, through which one can indeed get access
to the source code.  The source of the verification programs themselves
should be freely available for the mathematical knowledge formalized in
mizar to really matter (philosophically).

Jesse

--
Jesse Alama (alama@...)

[Freek Wiedijk]

Bill:

>I, for one, would look at the source code if it were
>available.

But would it help?  Understanding Mizar's behavior by
experimenting around with it to me seems much easier than
understanding it by looking at the implementation.  We're not
talking about an relatively abstract language like ML or
Haskell here, so the implementation is rather low level.

>As one example, I would like to understand the rules that
>Mizar uses for parsing a Term-Expression.

Really?  I've had many frustrations with Mizar (still have),
but this one I have never found confusing.

My problem generally is not that I don't understand how
Mizar parses a term, but mostly that I often am mystified
by the way it resolves the overloading.

>The correct parse tree can actually be *changed* by adding
>or removing functor definitions.

No.  The parse tree will be the same.  The interpretation of
the symbols will change, but the parse tree will be the same.

>If the world were perfect, then these things would all
>be neatly written in a well-organized reference manual.
>However, that manual may never be completed in our real
>world.

I once started such a manual.  My "tutorial" ("... in nine
easy steps") was supposed to be part of it.  But no one in
the Mizar group seemed to think it would be useful (which I
still find very strange!), and by now I don't think I ever
will write it.  Not as long as Mizar doesn't support empty
types, doesn't have much simpler environments, doesn't have
binders, doesn't have the old style "from" :-)  Ah yes:
and doesn't support "then" after "consider".

Freek

[Freek Wiedijk]

Josef:

>I never heard a serious explanation
>of why the sources are closed,

I know two anecdotes related to this (but maybe for you
neither of them is serious):

- The current policy of only getting the sources when
  you write at least one serious Mizar article made _you_
  write some very nice Mizar articles.  So that policy
  payed off.

- The sources used to be open, but then the only effect
  of that was that some silly person made a version of
  Mizar that just was different in that all the keywords
  had been changed.  That was so irritating that after that
  the sources got closed.

Freek

[Michael Nedzelsky]

> I once started such a manual.  My "tutorial" ("... in nine
> easy steps") was supposed to be part of it.  But no one in
> the Mizar group seemed to think it would be useful (which I
> still find very strange!), and by now I don't think I ever
> will write it. Not as long as Mizar doesn't support empty
> types, doesn't have much simpler environments, doesn't have
> binders, doesn't have the old style "from" :-)  Ah yes:
> and doesn't support "then" after "consider".

> Freek

I think you tutorial is very useful (I have read it), and I put the
link to this tutorial on Mizar Wiki site: http://wiki.mizar.org about
two years ago.
It seems that new Mizar users simply doesn't aware of the existence of Mizar
Wiki and your tutorial.
Two years ago I tried to understand Mizar at low level, because I
like to understand how the things work. I still think it is possible
to create an alternative implementation of Mizar language, though
now I am a happy user of Isabelle system.

By the way, what do you mean by 'old style "from"'?

Michael Nedzelsky

[Freek Wiedijk]

Dear Michael,

>By the way, what do you mean by 'old style "from"'?

Nowadays to use a scheme you need to define predicates
and/or functors that match the arguments of the scheme using
"defpred" and "deffunc".  Mizar used to be able to figure
out by itself what the instantiations of the predicates and
functors in the scheme were just by looking at the shape
of the formulas.  I liked it that way.

I'm sure that sometimes it was ambiguous, and that the
implementation of _how_ it worked was a big mess.  But in
practice it worked well for me, and I miss my proof looking
clean, without all the "defpred" noise.  When presenting
Mizar in a talk this is often one of the things that makes
my examples less convincing.

Freek

[Josef Urban]

Freek,

>> I never heard a serious explanation
>> of why the sources are closed,
>
> I know two anecdotes related to this (but maybe for you
> neither of them is serious):

Right, they are anecdotes, and they are always told in that spirit.
Problem is that in eight years I really never heard any _serious_
argument, to say nothing about having a serious and rational discussion.
Nothing to match the arguments expressed in the couple of previous
e-mails, and told over and over in many other places (read e.g. the
last-but-one paragraph of
http://www.dwheeler.com/essays/high-assurance-floss.html).

> - The current policy of only getting the sources when
>  you write at least one serious Mizar article made _you_
>  write some very nice Mizar articles.  So that policy
>  payed off.

No, I can't see how anyone can claim that because I (or someone else) was
forced to write one Mizar article, the policy paid off. That does not
account for the damage this policy causes. For my Msc. work, I originally
rejected Mizar right in the beginning, because I could not easily get its
source. Then it took at least a year of useless workarounds before I was
forced by my PhD supervisor to write the article so that I could get the
sources. I would probably never decide to do this myself, and rather
turned to other open-source proof assistants (I was experimenting with
IMPS a lot at that time).

There were other people since, who struggled with reverse engineering
Mizar (without writing any article), and also others who rejected Mizar
because of non-openness. Obviously those who rejected it immediately are a
bit hard to count :-).

> - The sources used to be open, but then the only effect
>  of that was that some silly person made a version of
>  Mizar that just was different in that all the keywords
>  had been changed.  That was so irritating that after that
>  the sources got closed.

I can't see what is irritating about thousands versions of Linux kernel
being used by various people. Some of the patches will never be accepted
into "official Linux" by Torvals/Morton, some will, some will get strong
support from their users anyway. There are countless examples of this -
the year is now 2008, not 1980 :-). One of them is obviously all the
various flavours of HOL and Isabelle. It is a fairly speculative
subject, but AFAIK this diversity and parallelism has rather fostered the
development of HOL-based systems than not (think e.g. Isar vs. old-style
Isabelle, Meson vs. Metis vs. Sledgehammer, the cool HTML presentation for
Isabelle/ZF at http://formalmath.tiddlyspot.com/, etc.).

Also, last time I heard that someone in Germany did translate Mizar-MSE
keywords to German, it was in Bialystok, and accepted positively.

Josef

[Josef Urban]

On Mon, 15 Sep 2008, Freek Wiedijk wrote:

>> The correct parse tree can actually be *changed* by adding
>> or removing functor definitions.
>
> No.  The parse tree will be the same.  The interpretation of
> the symbols will change, but the parse tree will be the same.

This all depends on the exact definitions of these notions. I think a part
of what Bill means is that type/overloading disambiguation is part of
"parsing" (in Mizar lingo: "parsing" is distributed across the "Parser"
and "Analyzer" pass). With this definition "parse tree" (as in XML after
"Parser" and "Analyzer") really includes (actually: mainly consists of)
the "interpretation of symbols" ("constructors"), so it will be different.
Obviously a very frequent case is that there will be no parse tree when a
definition is changed/added/removed, because a type error will occur.

Josef

[Robert Boyer]

I tend to avoid having views about what others should
do, e.g., use the GPL or not, because it is too
difficult for me to think through.  But I cannot let
pass without comment your remark:

> I can't see what is irritating about thousands
> versions of Linux kernel being used by various
> people.

GMP is a Gnu library written in C that does bignum
arithmetic.  It is said to be quite fast.

From the front page, http://gmplib.org/:

   GMP is very often miscompiled!  We are seeing ever
   increasing problems with miscompilations of the GMP
   code. It has now come to the point where a compiler
   should be assumed to miscompile GMP. Please never
   use your newly compiled libgmp.a or libgmp.so
   without first running make check. If it doesn't
   complete without errors, don't trust the
   library. Please try another compiler release, or
   change optimization flags until it works. If you
   have the skill to isolate the problem, please report
   it to us if it is a GMP bug; else to the compiler
   vendor. (The compilers that cause problems are HP's
   unbundled compilers and GCC, in particular Apple's
   GCC releases.)

Ever increasing!

Bob


-------------------------------------------------------


Date: Mon, 15 Sep 2008 17:24:09 +0200 (CEST)
From: Josef Urban <urban@...>
To: mizar-forum@...
Subject: Re: [mizar] PVS GPLed


Freek,

>> I never heard a serious explanation
>> of why the sources are closed,
>
> I know two anecdotes related to this (but maybe for you
> neither of them is serious):

Right, they are anecdotes, and they are always told in that spirit.
Problem is that in eight years I really never heard any _serious_
argument, to say nothing about having a serious and rational discussion.
Nothing to match the arguments expressed in the couple of previous
e-mails, and told over and over in many other places (read e.g. the
last-but-one paragraph of
http://www.dwheeler.com/essays/high-assurance-floss.html).

> - The current policy of only getting the sources when
>  you write at least one serious Mizar article made _you_
>  write some very nice Mizar articles.  So that policy
>  payed off.

No, I can't see how anyone can claim that because I (or someone else) was
forced to write one Mizar article, the policy paid off. That does not
account for the damage this policy causes. For my Msc. work, I originally
rejected Mizar right in the beginning, because I could not easily get its
source. Then it took at least a year of useless workarounds before I was
forced by my PhD supervisor to write the article so that I could get the
sources. I would probably never decide to do this myself, and rather
turned to other open-source proof assistants (I was experimenting with
IMPS a lot at that time).

There were other people since, who struggled with reverse engineering
Mizar (without writing any article), and also others who rejected Mizar
because of non-openness. Obviously those who rejected it immediately are a
bit hard to count :-).

> - The sources used to be open, but then the only effect
>  of that was that some silly person made a version of
>  Mizar that just was different in that all the keywords
>  had been changed.  That was so irritating that after that
>  the sources got closed.

I can't see what is irritating about thousands versions of Linux kernel
being used by various people. Some of the patches will never be accepted
into "official Linux" by Torvals/Morton, some will, some will get strong
support from their users anyway. There are countless examples of this -
the year is now 2008, not 1980 :-). One of them is obviously all the
various flavours of HOL and Isabelle. It is a fairly speculative
subject, but AFAIK this diversity and parallelism has rather fostered the
development of HOL-based systems than not (think e.g. Isar vs. old-style
Isabelle, Meson vs. Metis vs. Sledgehammer, the cool HTML presentation for
Isabelle/ZF at http://formalmath.tiddlyspot.com/, etc.).

Also, last time I heard that someone in Germany did translate Mizar-MSE
keywords to German, it was in Bialystok, and accepted positively.

Josef

[Josef Urban]

I think an even better example of what might be "irritating" (e.g. to
kernel hackers) is the number of malicious kernel rootkits based on their
work. Or the large "antisocial" parts of internet "irritating" Chinese
censors. For me, there is an infinite distance between the friendly
warning by the GMP people, and the "Chinese solution" :-).

Josef

On Mon, 15 Sep 2008, Robert Boyer wrote:

> I tend to avoid having views about what others should
> do, e.g., use the GPL or not, because it is too
> difficult for me to think through.  But I cannot let
> pass without comment your remark:
>
>> I can't see what is irritating about thousands
>> versions of Linux kernel being used by various
>> people.
>
> GMP is a Gnu library written in C that does bignum
> arithmetic.  It is said to be quite fast.
>
>> From the front page, http://gmplib.org/:
>
>   GMP is very often miscompiled!  We are seeing ever
>   increasing problems with miscompilations of the GMP
>   code. It has now come to the point where a compiler
>   should be assumed to miscompile GMP. Please never
>   use your newly compiled libgmp.a or libgmp.so
>   without first running make check. If it doesn't
>   complete without errors, don't trust the
>   library. Please try another compiler release, or
>   change optimization flags until it works. If you
>   have the skill to isolate the problem, please report
>   it to us if it is a GMP bug; else to the compiler
>   vendor. (The compilers that cause problems are HP's
>   unbundled compilers and GCC, in particular Apple's
>   GCC releases.)
>
> Ever increasing!
>
> Bob
>
>
> -------------------------------------------------------
>
>
> Date: Mon, 15 Sep 2008 17:24:09 +0200 (CEST)
> From: Josef Urban <urban@...>
> To: mizar-forum@...
> Subject: Re: [mizar] PVS GPLed
>
>
> Freek,
>
>>> I never heard a serious explanation
>>> of why the sources are closed,
>>
>> I know two anecdotes related to this (but maybe for you
>> neither of them is serious):
>
> Right, they are anecdotes, and they are always told in that spirit.
> Problem is that in eight years I really never heard any _serious_
> argument, to say nothing about having a serious and rational discussion.
> Nothing to match the arguments expressed in the couple of previous
> e-mails, and told over and over in many other places (read e.g. the
> last-but-one paragraph of
> http://www.dwheeler.com/essays/high-assurance-floss.html).
>
>> - The current policy of only getting the sources when
>>  you write at least one serious Mizar article made _you_
>>  write some very nice Mizar articles.  So that policy
>>  payed off.
>
> No, I can't see how anyone can claim that because I (or someone else) was
> forced to write one Mizar article, the policy paid off. That does not
> account for the damage this policy causes. For my Msc. work, I originally
> rejected Mizar right in the beginning, because I could not easily get its
> source. Then it took at least a year of useless workarounds before I was
> forced by my PhD supervisor to write the article so that I could get the
> sources. I would probably never decide to do this myself, and rather
> turned to other open-source proof assistants (I was experimenting with
> IMPS a lot at that time).
>
> There were other people since, who struggled with reverse engineering
> Mizar (without writing any article), and also others who rejected Mizar
> because of non-openness. Obviously those who rejected it immediately are a
> bit hard to count :-).
>
>> - The sources used to be open, but then the only effect
>>  of that was that some silly person made a version of
>>  Mizar that just was different in that all the keywords
>>  had been changed.  That was so irritating that after that
>>  the sources got closed.
>
> I can't see what is irritating about thousands versions of Linux kernel
> being used by various people. Some of the patches will never be accepted
> into "official Linux" by Torvals/Morton, some will, some will get strong
> support from their users anyway. There are countless examples of this -
> the year is now 2008, not 1980 :-). One of them is obviously all the
> various flavours of HOL and Isabelle. It is a fairly speculative
> subject, but AFAIK this diversity and parallelism has rather fostered the
> development of HOL-based systems than not (think e.g. Isar vs. old-style
> Isabelle, Meson vs. Metis vs. Sledgehammer, the cool HTML presentation for
> Isabelle/ZF at http://formalmath.tiddlyspot.com/, etc.).
>
> Also, last time I heard that someone in Germany did translate Mizar-MSE
> keywords to German, it was in Bialystok, and accepted positively.
>
> Josef
>
>

[Freek Wiedijk]

Josef:

>>No.  The parse tree will be the same.  The interpretation of
>>the symbols will change, but the parse tree will be the same.
>
>This all depends on the exact definitions of these notions.

I understand what you're saying here.

Still I want to make the point that the _tree_ (as a tree)
will be the same.  The tree structure of the term just
depends on the symbols and their priorities.

However, the constructors that those symbols refer to
obviously _does_ depend on the notations and registrations
that are visible.

Freek

[Freek Wiedijk]

Bob:

>GMP is a Gnu library written in C that does bignum
>arithmetic.  It is said to be quite fast.
>
>From the front page, http://gmplib.org/:
>
>   GMP is very often miscompiled!  We are seeing ever
>   increasing problems with miscompilations of the GMP
>   code. It has now come to the point where a compiler
>   should be assumed to miscompile GMP. Please never
>   use your newly compiled libgmp.a or libgmp.so
>   without first running make check. If it doesn't
>   complete without errors, don't trust the
>   library. Please try another compiler release, or
>   change optimization flags until it works. If you
>   have the skill to isolate the problem, please report
>   it to us if it is a GMP bug; else to the compiler
>   vendor. (The compilers that cause problems are HP's
>   unbundled compilers and GCC, in particular Apple's
>   GCC releases.)
>
>Ever increasing!

This is a very interesting quote, thanks for posting it!

So do I understand it correctly that this is not about
users not knowing how to deal with the GMP source code in
a proper way (related to users not knowing how to deal with
Mizar source code in a proper way), but instead about many
compilers having bugs that make them not compile the GMP
source code correctly (and therefore it is unrelated to
the issues of the Mizar source code being "free")?

Unrelated to this: I always claim that bugs in proof
assistants are like compiler bugs, and are therefore not a
serious reason for worry.  But this quote seems to suggest
that compiler bugs _are_ a serious reason for worry!

Freek

[Chisolm, Bill]

Wow, I'm surprised by how much discussion followed from my comments.
That's a good thing, I think.

I have read about the policy of making the sources available to those
who have written Mizar articles.  I was not sure whether that policy
is still in effect.  I'm glad to hear that it is.  I would like to
write a Mizar article, so perhaps I will be able get access under
that policy.  It's still an open question whether I can actually write
an article that the committee would want to include in the MML.

> >The correct parse tree can actually be *changed* by adding
> >or removing functor definitions.
>
> No.  The parse tree will be the same.  The interpretation of
> the symbols will change, but the parse tree will be the same.

I'll post an example (soon) showing what I meant by this remark.
To me, it looks like the parse tree is changing, but perhaps there
is another explanation for what happens.  I'll post the example under
a new title: "Question about functor precedence."

> I once started such a manual.  My "tutorial" ("... in nine
> easy steps") was supposed to be part of it.  But no one in
> the Mizar group seemed to think it would be useful (which I
> still find very strange!), and by now I don't think I ever
> will write it.

I have read your tutorial.  I don't know why some people said it
would not be useful.  I found it helpful.  Perhaps the people who said
that were underestimating how difficult it is for someone to learn
Mizar when starting from zero.  I applaud everyone who has written
materials to help new Mizar users.  Many thanks, Freek!

As I was learning about Mizar, the one document that helped me the
most was Michal Muzalewski's paper from 1993, "An Outline of PC Mizar".
The paper is still an excellent resource, although it does not
reflect many changes in Mizar that have occurred since 1993.  If only
someone had the time to revise that document...  If I remember
correctly, I found the paper through a link from Freek's web page.

Bill

[Freek Wiedijk]

Bill:

>Perhaps the people who said that were underestimating how
>difficult it is for someone to learn Mizar when starting
>from zero.

I think this is the problem with Mizar and its documentation.
The people in Bialystok are so used to their system that
they cannot imagine how difficult this is.

Personally I actually think that Mizar is a rather easy
system, but that it just has a few _very_ difficult barriers
that hides this fact quite effectively.  Getting a Mizar
environment right without being an expert is almost
impossible, and finding lemmas in the library also is
almost impossible.  Apart from that the system is quite
easy and nice.

>As I was learning about Mizar, the one document that helped
>me the most was Michal Muzalewski's paper from 1993,
>"An Outline of PC Mizar".  The paper is still an excellent
>resource, although it does not reflect many changes in Mizar
>that have occurred since 1993.  If only someone had the
>time to revise that document...  If I remember correctly,
>I found the paper through a link from Freek's web page.

<http://www.cs.ru.nl/~freek/mizar/mizarmanual.pdf>, I think.

Freek