Re: [mizar] Strong Mizar wish: linking to consider (fwd)

[Czeslaw Bylinski <bylinski@math.uwb.edu.pl>]

---------- Forwarded message ----------
Date: Thu, 14 Mar 2002 15:02:20 -0500
From: Michael Kohlhase <Michael_Kohlhase@asuka.mt.cs.cmu.edu>
Reply-To: Michael Kohlhase <kohlhase+@cs.cmu.edu>
To: mizar-forum@mizar.uwb.edu.pl
Subject: Re: [mizar] Strong Mizar wish: linking to consider

Hi,

> On Mon, 11 Mar 2002, Claudio Sacerdoti Coen wrote:
>
> >  in case you are interested in exporting to XML and use stylesheets
> >  or other machinery to pretty-print the text (and make it more interactive),
> >  can I please suggest you to have a look at the forthcoming european
> >  IST project MOWGLI (http://mowgli.cs.unibo.it) and to the still active HELM
> >  project (http://www.cs.unibo.it/helm) that does something similar for
> >  Coq proofs.
>
> The first stage that is currently discussed, is using XML as an internal
> format for various Mizar files. Once this is done, we can think of export
> to other formats, be it HELM or OMDoc. I did not find any DTDs on the
> MOWGLI page ... maybe I missed something?

I am not sure that the HELM format is a good format to transform into,
since it is very oriented towards the internal data format in Coq. I
understood Claudio's remark as "first use some XML-format for Mizar" just
as Coq uses the HELM format, which I think is very reasonable.


> On Sun, 10 Mar 2002, Antoni Urban wrote:
>
> > I know what Piotr is referring to. I noticed the problem when I joined Mizar
> > year ago. I would also suggest to create the system feature of attaching
> > pictures to articles. And more importantly, I am ready to help Mizar system
> > programmers to design the new features.
>
> Someone more "official" should answer this.
> My personal experience with "improving Mizar" is, that one has to have an
> article accepted in MML, to be taken a bit seriously by the Mizar team.
> I do not like it, but it really prevents some misunderstandings about
> Mizar.