[mizar] Re: feature request: include a semantic representaion of the mml in the mizar distribution

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> On Wed, 20 Dec 2006, Jesse Alama wrote:
>
>> A wishlist item: put the semantic representions of the MML, as found
>> at
>>
>> http://mmlquery.mizar.org/mml/current ,
>>
>> in the MIZAR distribution.  I often work on MIZAR articles when I
>> don't have network access and wish that I could check out semantic
>> representation of some article of interest, but am unable to do so.
>> It would be nice if I could just open my web browser and explore the
>> semantic representation of the MML offline.
>>
>> Thoughts?
>
> I can't resist the impression that you are almost citing the words of
> Freek Wiedijk who requested the linked abstracts a few years ago
> ;-)))) Then we started to distribute it as a separate tarball. But
> now, the software which produced the linked abstracts has
> unfortunately been left discontinued.

That is unfortunate!  It would be great if the abstracts were part of
the distrbution, too.

> When Josef created the semantic representation in its current form,
> there came a natural idea of distributing it instead of the old linked
> abstract, there were only technical problems because Josef thought it
> best for us to store the representation of all MML versions, which is
> not possible at the moment on our server. But having at least the
> current version of MML rendered in the semantically linked form is
> certainly a good idea and we'll try to do so ASAP to help all those
> who sometimes prefer/must work off-line.

Thanks!

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*393: Incorrect beginning of a reasoning item