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

[kohlhase]

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]

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]

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]

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.