Name : Jesse Alama Email : j.alama@fct.unl.pt MIME media type name : Text MIME subtype name : Standards Tree -mizar Required parameters : none Optional parameters : none Encoding considerations : 8bit Security considerations : none Interoperability considerations : Published specification : A. Grabowski, A. Kornilowicz, and A. Naumowicz, "Mizar in a Nutshell", Journal of Formalized Reasoning 3(2), 2010, pp. 153--245. Applications which use this media : The mizar suite of tools Additional information : 1. Magic number(s) : none 2. File extension(s) : .miz 3. Macintosh file type code : none 4. Object Identifiers: none The mizar language is a language for formalized mathematical documents. Authors use this langauge to express definitions of mathematical concepts, and express and proof formal mathematical statements. The language has been developed since the 1970s and today is used in teaching logic and mathematics in various high school and universty settings. The library of mathematical knowledge formalized in the mizar language, the Mizar Mathematical Library, consists (at the time of application) of more than 1100 "articles" which, like an ordinary mathematical article in a journal, are coherent presentations and developments of mathematics. Person to contact for further information : 1. Name : Jesse Alama 2. Email : j.alama@fct.unl.pt Intended usage : Common This media type is intended to be used by text editors and affiliated programs that read text (e.g., web browsers). Author/Change controller : Adam Naumowicz Association of Mizar Users sum@mizar.uwb.edu.pl -- Jesse Alama http://centria.di.fct.unl.pt/~alama/
Hello Jesse, (;-)) a few quick comments but I am sure others will have some more. - I think you should refer to the RFC template you use, please see the mailing list archive - I think the change controller should be the association of Mizar users', as an institution with an address, and not the name of a person; an email can complement it for sure! - type and subtypes are commonly lowercase... why not continue so? - 8bit... is there a charset there? - can the specification be indicated with a publicly accessible URL? - and finally the personal suggestion: I know Mizar is intended to be manipulated by text editors. Could you add two lines in the additional information that say something such as: - Window clipboard flavor: "Mizar" - Macintosh Uniform Type Identifier: "org.mizar" conforms to "public.text" this way applications can offer fragments in multiple formats on the clipboard, one of them, say, being RTF and the other Mizar, for different objectives. paul Le 30 juin 2011 à 14:02, Jesse Alama a écrit :
Name : Jesse Alama
Email : j.alama@fct.unl.pt
MIME media type name : Text
MIME subtype name : Standards Tree -mizar
Required parameters : none
Optional parameters : none
Encoding considerations : 8bit
Security considerations : none
Interoperability considerations :
Published specification : A. Grabowski, A. Kornilowicz, and A. Naumowicz, "Mizar in a Nutshell", Journal of Formalized Reasoning 3(2), 2010, pp. 153--245.
Applications which use this media : The mizar suite of tools
Additional information :
1. Magic number(s) : none 2. File extension(s) : .miz 3. Macintosh file type code : none 4. Object Identifiers: none
The mizar language is a language for formalized mathematical documents. Authors use this langauge to express definitions of mathematical concepts, and express and proof formal mathematical statements. The language has been developed since the 1970s and today is used in teaching logic and mathematics in various high school and universty settings. The library of mathematical knowledge formalized in the mizar language, the Mizar Mathematical Library, consists (at the time of application) of more than 1100 "articles" which, like an ordinary mathematical article in a journal, are coherent presentations and developments of mathematics.
Person to contact for further information :
1. Name : Jesse Alama 2. Email : j.alama@fct.unl.pt
Intended usage : Common This media type is intended to be used by text editors and affiliated programs that read text (e.g., web browsers).
Author/Change controller : Adam Naumowicz Association of Mizar Users sum@mizar.uwb.edu.pl
-- Jesse Alama http://centria.di.fct.unl.pt/~alama/
Hi Paul, Paul Libbrecht wrote:
- I think you should refer to the RFC template you use, please see the mailing list archive
OK, thanks. I'll take a look.
- I think the change controller should be the association of Mizar users', as an institution with an address, and not the name of a person; an email can complement it for sure!
This wasn't clear to me when I was filling out the form at http://www.iana.org/cgi-bin/mediatypes.pl Item 13 in the form says "Person to contact for further information" with a link to RFC 4288, section 4.9. The Association of Mizar Users is definitely the best entity to put here. It is in charge of maintaining the mizar language and its suite of tools, and has, moreover, an email address (which is what I actually included when I filled out the form). I named Adam Naumowicz, a long-time member of the Association of Mizar Users and one of the core developers of Mizar, only because I was literally interpreting the request of the form. In fact, when I came to this part of the form, I was puzzled, so I asked Adam which of the core developers of Mizar (i.e., which person) would be suitable, he named a few candidates (he listed himself), so I put him down.
- type and subtypes are commonly lowercase... why not continue so?
You're right that they should be lowercase ("text", "mizar"). This again is a consequence of the form http://www.iana.org/cgi-bin/mediatypes.pl You can see for yourself that "Text" is one of the options, not "text". I suppose I put down "Mizar" just for the sake of parallelism, but in any case it should be "mizar".
- 8bit... is there a charset there?
I'm not sure I understand; can you say more? Valid mizar texts, these days, are pure ASCII, but they weren't always so and there's no guarantee that they will always be so. I put down 8-bit just to be on the safe side. Perhaps I'm getting something wrong here; let me know.
- can the specification be indicated with a publicly accessible URL?
One candidate might be http://www.mizar.org/language/ which gives some information about the language. Adam, do you have a better suggestion here?
- and finally the personal suggestion: I know Mizar is intended to be manipulated by text editors. Could you add two lines in the additional information that say something such as: - Window clipboard flavor: "Mizar" - Macintosh Uniform Type Identifier: "org.mizar" conforms to "public.text" this way applications can offer fragments in multiple formats on the clipboard, one of them, say, being RTF and the other Mizar, for different objectives.
Nice spot. Your suggestions look fine to me. Best, Jesse -- Jesse Alama http://centria.di.fct.unl.pt/~alama/
Le 1 juil. 2011 à 14:07, Jesse Alama a écrit :
- I think the change controller should be the association of Mizar users', as an institution with an address, and not the name of a person; an email can complement it for sure!
This wasn't clear to me when I was filling out the form at
http://www.iana.org/cgi-bin/mediatypes.pl Item 13 in the form says "Person to contact for further information" with a link to RFC 4288, section 4.9. The Association of Mizar Users is definitely the best entity to put here. It is in charge of maintaining the mizar language and its suite of tools, and has, moreover, an email address (which is what I actually included when I filled out the form). I named Adam Naumowicz, a long-time member of the Association of Mizar Users and one of the core developers of Mizar, only because I was literally interpreting the request of the form. In fact, when I came to this part of the form, I was puzzled, so I asked Adam which of the core developers of Mizar (i.e., which person) would be suitable, he named a few candidates (he listed himself), so I put him down.
I see a "nesting" here for section 13 but that seems to be interpretation. In all W3C templates, change controller and author do not need to be equal and I think we converge to say the asme here. [...]
- 8bit... is there a charset there?
I'm not sure I understand; can you say more? Valid mizar texts, these days, are pure ASCII, but they weren't always so and there's no guarantee that they will always be so. I put down 8-bit just to be on the safe side. Perhaps I'm getting something wrong here; let me know.
If you say ASCII then I would suggest to keep ascii. Is the CRLF requirement also a requirement? I wish others comment here. The reason I asked about charset is that the media-type parameter charset is the cause of numerous communication around here, especially in the xml world, i'd just like to avoid any error here if possible.
- can the specification be indicated with a publicly accessible URL?
One candidate might be
http://www.mizar.org/language/ which gives some information about the language. Adam, do you have a better suggestion here?
Such things as ASCII is not there.... this specifies the vocabulary not really the file format. thanks paul
Paul Libbrecht wrote:
If you say ASCII then I would suggest to keep ascii.
That is, you recommend that I specify a 7-bit encoding for the proposed media type?
Is the CRLF requirement also a requirement?
I'm not sure I understand what you're asking.
The reason I asked about charset is that the media-type parameter charset is the cause of numerous communication around here, especially in the xml world, i'd just like to avoid any error here if possible.
Ah, OK. I think this kind of encoding question doesn't apply to mizar texts.
- can the specification be indicated with a publicly accessible URL? One candidate might be
http://www.mizar.org/language/ which gives some information about the language. Adam, do you have a better suggestion here?
Such things as ASCII is not there.... this specifies the vocabulary not really the file format.
True, it doesn't specify the file format. Broadly, any ASCII document is, potentially, a mizar text. Of course, only those texts that adhere to the rules of the mizar language are acceptable to the mizar suite of tools. But in principle they can operate on any ASCII text. Does that clarify things? Jesse -- Jesse Alama http://centria.di.fct.unl.pt/~alama/
I believe that you sent this to the wrong (old) address. Instead, please see <https://www.ietf.org/mailman/listinfo/ietf-types> --Paul Hoffman On Jun 30, 2011, at 5:02 AM, Jesse Alama wrote:
Name : Jesse Alama
Email : j.alama@fct.unl.pt
MIME media type name : Text
MIME subtype name : Standards Tree -mizar
Required parameters : none
Optional parameters : none
Encoding considerations : 8bit
Security considerations : none
Interoperability considerations :
Published specification : A. Grabowski, A. Kornilowicz, and A. Naumowicz, "Mizar in a Nutshell", Journal of Formalized Reasoning 3(2), 2010, pp. 153--245.
Applications which use this media : The mizar suite of tools
Additional information :
1. Magic number(s) : none 2. File extension(s) : .miz 3. Macintosh file type code : none 4. Object Identifiers: none
The mizar language is a language for formalized mathematical documents. Authors use this langauge to express definitions of mathematical concepts, and express and proof formal mathematical statements. The language has been developed since the 1970s and today is used in teaching logic and mathematics in various high school and universty settings. The library of mathematical knowledge formalized in the mizar language, the Mizar Mathematical Library, consists (at the time of application) of more than 1100 "articles" which, like an ordinary mathematical article in a journal, are coherent presentations and developments of mathematics.
Person to contact for further information :
1. Name : Jesse Alama 2. Email : j.alama@fct.unl.pt
Intended usage : Common This media type is intended to be used by text editors and affiliated programs that read text (e.g., web browsers).
Author/Change controller : Adam Naumowicz Association of Mizar Users sum@mizar.uwb.edu.pl
-- Jesse Alama http://centria.di.fct.unl.pt/~alama/
Paul Hoffman wrote:
I believe that you sent this to the wrong (old) address. Instead, please see<https://www.ietf.org/mailman/listinfo/ietf-types>
Whoops, you're right. I've resent the message to the correct address (ietf-types@ietf.org). Thanks, Jesse -- Jesse Alama http://centria.di.fct.unl.pt/~alama/
participants (3)
-
Jesse Alama -
Paul Hoffman -
Paul Libbrecht