Re: PVS GPLed

> about many compilers having bugs that make them not
> compile the GMP source code correctly

That's how I read it, though I know no more than you!

> unrelated to the issues of the Mizar source code
> being "free"

Hmmm.  I've heard everything is related.

I was having a daytime nightmare about a possible world
in which some versions of a hypothetically liberated
Mizar reported that something was a theorem while
others said that it was not.

It seems that even checking alleged theorems about
concrete bignum arithmetic is getting increasingly
harder.

Bob