search

slatex / sTeX

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

\inlineass[name= in foo.en does not induce exportable symbol in foo.de (even with sig=en in place) #425

Open kohlhase opened 2 months ago

kohlhase commented 2 months ago

This is a bit subtle: When typesetting smglom/mv/source/mod/equation.de.tex I get the error 

! Package stex Error: No symbol reflexive.cond found!

Type <return> to continue.
 ...                                              

l.9 ...e.cond]{\sr{reflexive?reflexive}{reflexiv}}
                                                   und

! Package stex Error: No symbol transitive.cond found!

Type <return> to continue.
 ...                                              

l.10 ...nd]{\sr{transitive?transitive}{transitiv}}
                                                   ist.

It seems that the problem is really in smglom/sets/source/mod/preorder.de.tex, which has 

  \inlineass[for=reflexive.cond]{\sr{reflexive?reflexive}{reflexiv}} und
  \inlineass[for=transitive.cond]{\sr{transitive?transitive}{transitiv}} ist.

and equation.de.tex has a \usemodule[smglom/sets]{mod?preorder} In and of itself, preorder.de.tex typesets fine, so the symbol is created and exported from preorder.en.tex, just (it seems) not into equation.de.tex

kohlhase commented 2 months ago

BTW, you can see this on the build server now. I have no idea why this has not appeared earlier, so this may be a regression

Jazzpirate commented 2 months ago

I think the problem is somewhere else: It's the \usestructure{proset} in preorder.de.tex (btw, there are two usestructures, the latter of which is redundant) - or, rather, the lack thereof in equation.de.tex.

\usestructure behaves like \usemodule in that it's ignored in sms mode and local to the tex group. \inlineass[for=reflexive.cond] (in preorder.de.tex) however is not just a usage of the symbol; it technically provides a type to the symbol (namely DED A for the marked-up proposition A). Within preorder.de.tex, that's fine because tex can't distinguish between "importing" and "using". But in sms-mode, tex ignores the usestructure (because it's just a "usage") and then fails at the \inlineass[for=], because the symbol really isn't in scope.

It should be mentioned that there is no reason in preorder.de.tex to use an \inlineass[for=...] as of yet anyway - it's a purely formal annotation that is already covered by preorder.en.tex, so the one in .de adds nothing. It's clear to me that it should also have some informal meaning as well, but then usestructure is the wrong thing to use (maybe a conservative extension?) and it's not yet clear what the markup would mean on the informal level...

kohlhase commented 2 months ago

I agree, \inlineass[name should definitely have an informal meaning, and I thought it alsready had. In particular, this will become very important in the "informal views" things that @Marcel is working on. In fact I am not sure why this has not popped up in his implementation yet.