search

slatex / sTeX

A semantic Extension of TeX/LaTeX
50 stars 9 forks source link

We need to document Metatheory.en.tex #356

Open kohlhase opened 2 years ago

kohlhase commented 2 years ago

In the IDE I get an ambiguous symbol warning on a \symname{object} with one of the candidates being in Metatheory.en.tex and have to decide whether that is already the right one or if I want to define/define it in MiKoMH/CompLog/source/kr/mod/semnet-nutshell.en.tex (as I am currently doing; hence the ambiguity) or if I want to extend SMGloM by a metaphysics archive, where I can define such things.

kohlhase commented 2 years ago

Also I am quite confused, the stex-doc documentation speaks of the stex-metatheory package, and on CTAN, there still seems to be a stex-metatheory.dtx but in the current sTeX from GIT I cannot find that. And somehow the ambiguity is with a file from MathHub/sTeX.

Screenshot 2022-09-26 at 07 40 00

This needs to be cleaned up!

Jazzpirate commented 2 years ago

It is here: https://github.com/slatex/sTeX/blob/main/source/stex/stex-metatheory.dtx

And in there, you will note \str_const:Nn \c_stex_metatheory_ns_str {http://mathhub.info/sTeX/meta}

There is no ambiguity - there is a duplication however. The metatheory in the sTeX package itself is embedded in stex.sty as to be self-contained. This works for latex, but not for MMT. Therefore, a copy of it exists as a individual .tex file in sTeX/meta-inf, that additionally imports basic MMT constants necessary for various MMT/OMDoc-things (record types, string/number literals etc, all metadata). MMT only ever uses the latter since it doesn't even know about stex.sty, latex/rustex only ever use the former, since it's loaded from the beginning :)

Jazzpirate commented 2 years ago

Metatheory?object is intended to be the equivalent of an Any or Top type in programming languages - everything is an object

Jazzpirate commented 2 years ago

In general, I would defer documenting the metatheory until we start properly introducing types in smglom - its primary purpose is to provide primitives and corresponding inference rules for MMT to type check content, and I strongly suspect that it will change significantly once we experiment with that more.

kohlhase commented 2 years ago

It is here: https://github.com/slatex/sTeX/blob/main/source/stex/stex-metatheory.dtx

And in there, you will note \str_const:Nn \c_stex_metatheory_ns_str {http://mathhub.info/sTeX/meta}

There is no ambiguity - there is a duplication however. The metatheory in the sTeX package itself is embedded in stex.sty as to be self-contained. This works for latex, but not for MMT. Therefore, a copy of it exists as a individual .tex file in sTeX/meta-inf, that additionally imports basic MMT constants necessary for various MMT/OMDoc-things (record types, string/number literals etc, all metadata). MMT only ever uses the latter since it doesn't even know about stex.sty, latex/rustex only ever use the former, since it's loaded from the beginning :)

That text is something that could/should go into the documentation. The other two as well. Knowing that it is mostly about types would make things much clearer.