\makeatletter \ifcsname if@infulldoc\endcsname\else \expandafter\newif\csname if@infulldoc\endcsname\@infulldocfalse \fi \makeatother \csname if@infulldoc\endcsname\else \def\bibfolder{../lib/bib} \input{stex-docheader} \infulldoctrue \csname bool_set_true:N\expandafter\endcsname\csname stex_dtx_tests_bool\endcsname \begin{document} \csname if@infulldoc\endcsname\else \title{ The {\stex{3}} Manual \thanks{Version {\fileversion} (last revised {\filedate})} } \author{Michael Kohlhase, Dennis Müller\\ FAU Erlangen-Nürnberg\\ \url{http://kwarc.info/} } \pagenumbering{roman} \maketitle \input{stex-abstract}\bigskip This is the user manual for the \sTeX package and associated software. It is primarily directed at end-users who want to use \sTeX to author semantically enriched documents. For the full documentation, see \href{\basedocurl/stex.pdf}{the \sTeX documentation} \makeatletter \renewcommand\part{% \clearpage \thispagestyle{plain}% \@tempswafalse \null\vfil \secdef\@part\@spart% } \newcounter{chapter} \numberwithin{section}{chapter} \renewcommand\thechapter{\@arabic\c@chapter} \renewcommand\thesection{\thechapter.\@arabic\c@section} \newcommand*\chaptermark[1]{} \setcounter{secnumdepth}{2} \newcommand\@chapapp{\chaptername} %\newcommand\chaptername{Chapter} \def\ps@headings{% \let\@oddfoot\@empty \def\@oddhead{{\slshape\rightmark}\hfil\thepage}% \let\@mkboth\markboth \def\chaptermark##1{% \markright{\MakeUppercase{% \ifnum \c@secnumdepth >\m@ne \@chapapp\ \thechapter. \ % \fi ##1}}% }% } \newcommand\chapter{\clearpage \thispagestyle{plain}% \global\@topnum\z@ \@afterindentfalse \secdef\@chapter\@schapter% } \def\@chapter[#1]#2{\refstepcounter{chapter}% \typeout{\@chapapp\space\thechapter.}% \addcontentsline{toc}{chapter}% {\protect\numberline{\thechapter}#1}% \chaptermark{#1}% \addtocontents{lof}{\protect\addvspace{10\p@}}% \addtocontents{lot}{\protect\addvspace{10\p@}}% \@makechapterhead{#2}% \@afterheading% } \def\@makechapterhead#1{% \vspace*{50\p@}% {\parindent \z@ \raggedright \normalfont \huge\bfseries \@chapapp\space \thechapter \par\nobreak \vskip 20\p@ \interlinepenalty\@M \Huge \bfseries #1\par\nobreak \vskip 40\p@ }% } \newcommand*\l@chapter[2]{% \ifnum \c@tocdepth >\m@ne \addpenalty{-\@highpenalty}% \vskip 1.0em \@plus\p@ \setlength\@tempdima{1.5em}% \begingroup \parindent \z@ \rightskip \@pnumwidth \parfillskip -\@pnumwidth \leavevmode \bfseries \advance\leftskip\@tempdima \hskip -\leftskip #1\nobreak\hfil \nobreak\hb@xt@\@pnumwidth{\hss #2% \kern-\p@\kern\p@}\par \penalty\@highpenalty \endgroup \fi} \renewcommand*\l@section{\@dottedtocline{1}{1.5em}{2.8em}} \renewcommand*\l@subsection{\@dottedtocline{2}{3.8em}{3.2em}} \renewcommand*\l@subsubsection{\@dottedtocline{3}{7.0em}{4.1em}} \def\partname{Part} \def\toclevel@part{-1} \def\maketitle{\chapter{\@title}} \let\thanks\@gobble \let\DelayPrintIndex\PrintIndex \let\PrintIndex\@empty \providecommand*{\hexnum}[1]{\text{\texttt{\char`\"}#1}} \makeatother \ExplSyntaxOn \int_set:Nn \l_document_structure_section_level_int {1} \ExplSyntaxOff \clearpage {% \def\\{:}% fix "newlines" in the ToC \tableofcontents } \clearpage \pagenumbering{arabic} \fi \long\def\ignore#1{} \begin{sfragment}{What is \sTeX?} Formal systems for mathematics (such as interactive theorem provers) have the potential to significantly increase both the accessibility of published knowledge, as well as the confidence in its veracity, by rendering the precise semantics of statements machine actionable. This allows for a plurality of added-value services, from semantic search up to verification and automated theorem proving. Unfortunately, their usefulness is hidden behind severe barriers to accessibility; primarily related to their surface languages reminiscent of programming languages and very unlike informal standards of presentation. \sTeX minimizes this gap between informal and formal mathematics by integrating formal methods into established and widespread authoring workflows, primarily \LaTeX, via non-intrusive semantic annotations of arbitrary informal document fragments. That way formal knowledge management services become available for informal documents, accessible via an IDE for authors and via generated \emph{active} documents for readers, while remaining fully compatible with existing authoring workflows and publishing systems. Additionally, an extensible library of reusable document fragments is being developed, that serve as reference targets for global disambiguation, intermediaries for content exchange between systems and other services. Every component of the system is designed modularly and extensibly, and thus lay the groundwork for a potential full integration of interactive theorem proving systems into established informal document authoring workflows. \paragraph{} The general \sTeX workflow combines functionalities provided by several pieces of software: \begin{itemize} \item The \sTeX package to use semantic annotations in {\LaTeX} documents, \item \RusTeX to convert |tex| sources to (semantically enriched) |xhtml|, \item The \mmt software, that extracts semantic information from the thus generated |xhtml| and provides semantically informed added value services. \end{itemize} % ---------------------------- \ignore{The objectives of this project will be achieved by developing a language and system that uses non-intrusive annotations to augment informal documents with semantic information (ranging from \textbf{fully formal} to \textbf{purely informal}) without impacting linguistic presentation or document layout. That way, the system remains compatible with established publishing pipelines and practices, while additionally providing flexiformal information that enables formal knowledge management services, and hence produces \emph{rich active documents}, satisfying \textbf{R3}, \textbf{R4} and \textbf{R5}. In particular, it will avoid commitment to a fixed logical foundation. Instead, it will be designed as a modular pipeline of consecutive and compositional annotations, semantics extraction and translation steps, extensible via new structuring mechanisms (\textbf{R1}), library content (\textbf{R2}), NLP techniques, foundations, translation methods and end-user services. Naturally, the benefits of formal knowledge management services scale with the amount of mathematics involved. Consequently I will primarily focus on those STEM fields in which mathematical methods are most prominently used (e.g. mathematics, physics, computer science). Since in those fields \LaTeX~is the most commonly used scientific writing tool, I will also primarily focus on \LaTeX~as a development and evaluation target, but the system will be designed such that all components apart from the surface language will be integrable with other writing tools (e.g. WYSIWYG word processors). \paragraph{} The basic architecture of the proposed system is sketched in \autoref{fig:architecture}. \begin{figure}\centering \resizebox{0.95\textwidth}{!}{\tikzinput[]{diagram}} {\small (Note, that the syntax used in the box on the top right is prototypical and subject to change during the project. Details and open questions regarding the syntax are discussed here: \url{https://github.com/KWARC/FoMID/issues/1})} \caption{Basic Architecture of the Proposed System}\label{fig:architecture} \end{figure} A user can write their content using standard \LaTeX\ in an IDE; ideally using semantic annotations provided by \sTeX %and the library developed in \OBJref{smglom} (as in the upper right of \autoref{fig:architecture}), but not necessarily so. The document is converted to xhtml with \omdoc annotations using \LaTeX ML in the background, thus becoming actionable by the \mmt system. Both the source document as well as the generated xhtml/\omdoc are accessible to a natural language processing pripeline that can supply additional inferred semantic information or suggest annotations to the user, in the latter case augmenting the source document directly. This pipeline can use both classical NLP techniques using the GLIF system, as well as machine learning models such as \cite{own:fifom}. A semiformal fragment is converted into an appropriate syntax tree (possibly containing opaque informal nodes), thus becoming amenable to flexiformal knowledge management services. In a consecutive step -- if sufficiently annotated --, these are additionally translated to a fully formal foundation, e.g. using the techniques from \cite{DMueller:phd:19,own:translations}, allowing more powerful services and conversion to established formal systems. All three representations are thus available from within the \mmt system for various knowledge management services, interfaces for which can be implemented in the IDE. Importantly, every non-trivial arrow in the figure is composable and extensible -- translations to a foundation can be provided by supplying an appropriate formalization and alignment-based translations (or entirely new methods), services can be implemented generically using the \mmt API, NLP techniques can be implemented both inside and alongside of GLIF, and the concrete syntax within \sTeX can be extended by convenience macros in \LaTeX\ (enabling new structuring mechanisms as in \textbf{R1} via \mmt extensions, see \cite{MueRabRot:rslffml20}) as well as via additions to the library, which will be extensible both from within the IDE as well as on MathHub, remaining backwards compatible with existing content in a surface language. Additionally, sufficiently disambiguated statements can be translated to the syntax of external systems (such as interactive theorem prover systems or computer algebra systems), which can thus be integrated as additional services into the system. } \end{sfragment} \begin{sfragment}{Quickstart} \begin{sfragment}{Setup} \begin{sfragment}{The \sTeX IDE} TODO: VSCode Plugin \end{sfragment} \begin{sfragment}{Manual Setup} Foregoing on the \sTeX IDE, we will need several pieces of software; namely: \begin{itemize} \item \textbf{The \sTeX-Package} available \href{https://github.com/slatex/sTeX/blob/latex3/doc/stex.pdf}{here}% \ednote{For now, we require the \texttt{latex3}-branch}. Note, that the CTAN repository for \LaTeX{} packages may contain outdated versions of the \sTeX package, so make sure, that your |TEXMF| system variable is configured such that the packages available in the linked repository are prioritized over potential default packages that come with your \TeX{} distribution. %If you are only interested in using semantic macros in (ultimately) %|pdf|s generated by |pdflatex|, this is all you need. \item \textbf{The \mmt System} available \href{https://github.com/uniformal/MMT/tree/sTeX}{here}% \ednote{For now, we require the \texttt{sTeX}-branch, requiring manually compiling the MMT sources}. We recommend following the setup routine documented \href{https://uniformal.github.io//doc/setup/}{here}. Following the setup routine (Step 3) will entail designating a |MathHub|-directory on your local file system, where the \mmt system will look for \sTeX/\mmt content archives. \item To make sure that \sTeX too knows where to find its archives, we need to set a global system variable |MATHHUB|, that points to your local |MathHub|-directory (see \sref{sec.stexarchives}). \item \textbf{\sTeX Archives} If we only care about {\LaTeX} and generating |pdf|s, we do not technically need \mmt at all; however, we still need the |MATHHUB| system variable to be set. Furthermore, \mmt can make downloading content archives we might want to use significantly easier, since it makes sure that all dependencies of (often highly interrelated) \sTeX archives are cloned as well. Once set up, we can run |mmt| in a shell and download an archive along with all of its dependencies like this: |lmh install |, or a whole \emph{group} of archives; for example, |lmh install smglom| will download all smglom archives. \item \textbf{\RusTeX} The \mmt system will also set up \RusTeX for you, which is used to generate (semantically annotated) |xhtml| from tex sources. In lieu of using \mmt, you can also download and use \RusTeX directly \href{https://github.com/slatex/RusTeX}{here}. \end{itemize} \end{sfragment} \end{sfragment} \begin{sfragment}{A First \sTeX Document} Having set everything up, we can write a first \sTeX document. As an example, we will use the |smglom/calculus| and |smglom/arithmetics| archives, which should be present in the designated |MathHub|-folder. The document we will consider is the following: \begin{framed}\begin{latexcode} \documentclass{article} \usepackage{stex} \usepackage{xcolor} \def\compemph#1{\textcolor{blue}{#1}} \begin{document} \usemodule[smglom/calculus]{series} \usemodule[smglom/arithmetics]{realarith} The \symref{series}{series} $\infinitesum{n}{1}{ \realdivide[frac]{1}{ \realpower{2}{n} } }$ \symref{converges}{converges} towards $1$. \end{document} \end{latexcode}\end{framed} Compiling this document with |pdflatex| should yield the output \begin{framed} The \textbf{series} $\textcolor{blue}{\sum}_{n=1}^{\textcolor{blue}\infty} \frac{1}{2^n}$ \textbf{converges} towards $1$. \end{framed} Note that the $\sum$ and $\infty$-symbols are highlighted in blue, and the words ``series'' and ``converges'' in bold. This signifies that these words and symbols reference \sTeX \emph{symbols} formally declared somewhere; associating their \emph{presentation} in the document with their (formal) definition - i.e. their semantics. The precise way in which they are highlighted (if at all) can of course be customized (see \ednote{somewhere later}). \begin{function}{\usemodule} The command |\usemodule[some/archive]{modulename}| finds some module in the appropriate archive -- in the first case (|\usemodule[smglom/calculus]{series}|), \sTeX looks for the archive |smglom/calculus| in our local MathHub-directory (see \sref{sec.stexarchives}), and in its source-folder for a file |series.tex|. Since no such file exists, and by default the document is assumed to be in \emph{english}, it picks the file |series.en.tex|, and indeed, in here we find a statement |\begin{smodule}{series}|. \iffalse\end{smodule}\fi \sTeX now reads this file and makes all semantic macros therein available to use, along with all its dependencies. This enables the usage of |\infinitesum| later on. Analogously, |\usemodule[smglom/arithmetics]{realarith}| opens the file |realarith.en.tex| in the |.../smglom/arithmetics/source|-folder and makes its contents available, e.g. |\realdivide| and |\realpower|. \end{function} \begin{function}{\symref,\symname} The command |\symref{symbolname}{text}| marks the |text| in the second argument as representing the |symbolname| in the first argument -- which is why the word ``series'' is set in boldface. In the pdf, this is all that happens. In the |xhtml| (which we will investigate shortly) however, we will note that the word ``series'' is now annotated with the full URI of the symbol denoting the \emph{mathematical concept of a series}. In other words, the word is associated with an unambiguous semantics. Notably, in both cases above (\emph{series} and \emph{converges}) the text that \emph{references} the symbol and the name of the symbol are identical. Since this occurs quite often, the shorthand |\symname{converges}| would have worked as well, where |\symname{foo-bar}| behaves exactly like |\symref{foo-bar}{foo bar}| - i.e. the text is simply the name of the symbol with ``|-|'' replaced by a space. \end{function} \begin{function}{\importmodule} If you investigated the contents of the imported modules (|realarith| and |series|) more closely, you'll note that none of them contain a symbol ``|converges|''. Yet, we can use |\symref| to refer to ``converges''. That is because the symbol |converges| is found in |smglom/calculus/source/sequenceConvergence.en.tex|, and |series.en.tex| contains the line |\importmodule{sequenceConvergence}|. The |\importmodule|-statement makes the module referenced available to all documents that include the current module. As such, a ``current module'' has to exist for |\importmodule| to work, which is why the command is only allowed within a |module|-environment. \end{function} \textcolor{red}{TODO} explain |xhtml| conversion, MMT compilation (requires an archive...?). \end{sfragment} \end{sfragment} \begin{sfragment}{Using \sTeX} \input{packages/stex-basics} \input{packages/stex-terms} \input{packages/stex-references} \end{sfragment} \begin{sfragment}[id=sec.stexarchives]{\sTeX Archives} \input{packages/stex-mathhub} \end{sfragment} \begin{sfragment}{Creating New Modules and Symbols} \textcolor{red}{TODO} \stexexample{ \begin{smodule}{assoctest} \symdef{foo}[args=iia]{\comp{a:}#1\comp{;b:}#2\comp{;c:}#3}{\comp[#1\comp{;}##1\comp+##2\comp;#2\comp]} $\foo {w_1}{w_2}{x,y,z}$ \end{smodule} } \input{packages/stex-modules} \input{packages/stex-symbols} \input{packages/stex-inheritance} \begin{sfragment}{Advanced Structuring Mechanisms} \input{packages/stex-features} \end{sfragment} \begin{sfragment}{Primitive Symbols (The \sTeX Metatheory)} \input{packages/stex-metatheory} \end{sfragment} \end{sfragment} \begin{sfragment}{\sTeX Statements (Definitions, Theorems, Examples, ...)} \input{packages/stex-statements} \input{packages/stex-proofs} \end{sfragment} \begin{sfragment}{Additional Packages} \input{packages/stex-tikzinput} \begin{sfragment}{Modular Document Structuring} \input{packages/stex-document-structure} \end{sfragment} \begin{sfragment}{Slides and Course Notes} \input{packages/stex-slides} \end{sfragment} \begin{sfragment}{Homework, Problems and Exams} \input{packages/stex-problem} \input{packages/stex-hwexam} \end{sfragment} \end{sfragment} \chapter{Stuff} \section{Modules} \begin{function}{\sTeX , \stex} Both print this \stex logo. \end{function} \subsection{Semantic Macros and Notations} Semantic macros invoke a formally declared symbol. To declare a symbol (in a module), we use \cs{symdecl}, which takes as argument the name of the corresponding semantic macro, e.g. |\symdecl{foo}| introduces the macro \cs{foo}. Additionally, \cs{symdecl} takes several options, the most important one being its arity. |foo| as declared above yields a \emph{constant} symbol. To introduce an \emph{operator} which takes arguments, we have to specify which arguments it takes. \begin{smodule}{SemanticMacrosExample} For example, to introduce binary multiplication, we can do |\symdecl{mult}[args=2]|. We can then supply the semantic macro with arbitrarily many notations, such as |\notation{mult}{#1 #2}|. \stexexample{ \symdecl{mult}[args=2] \notation{mult}{#1 #2} $\mult{a}{b}$ } Since usually, a freshly introduced symbol also comes with a notation from the start, the \cs{symdef} command combines \cs{symdecl} and \cs{notation}. So instead of the above, we could have also written \begin{center} |\symdef{mult}[args=2]{#1 #2}| \end{center} \symdecl{mult}[args=2] \notation{mult}{#1 #2} \notation{mult}[cdot]{#1 \comp{\cdot} #2} \notation{mult}[times]{#1 \comp{\times} #2} Adding more notations like |\notation{mult}[cdot]{#1 \comp{\cdot} #2}| or |\notation{mult}[times]{#1 \comp{\times} #2}| allows us to write |$\mult[cdot]{a}{b}$| and |$\mult[times]{a}{b}$|: \stexexample{ \notation{mult}[cdot]{#1 \comp{\cdot} #2} \notation{mult}[times]{#1 \comp{\times} #2} $\mult[cdot]{a}{b}$ and $\mult[times]{a}{b}$ } \notation{mult}[cdot]{#1 \comp{\cdot} #2} \notation{mult}[times]{#1 \comp{\times} #2} Not using an explicit option with a semantic macro yields the first declared notation, unless changed\ednote{TODO}. Outside of math mode, or by using the starred variant |\foo*|, allows to provide a custom notation, where notational (or textual) components can be given explicitly in square brackets. \stexexample{ $\mult*{\arg{a}\comp{\ast}\arg{b}}$ is the \mult{\comp{product of} \arg{$a$} \comp{and} \arg{$b$}} } In custom mode, prefixing an argument with a star will not print that argument, but still export it to \omdoc: \stexexample{ \mult{\comp{Multiplying} \arg*{$\mult{a}{b}$} again by \arg{$b$}} yields... } The syntax |*[|\meta{int}|]| allows switching the order of arguments. For example, given a 2-ary semantic macro |\forevery| with exemplary notation |\forall #1. #2|, we can write \stexexample{ \symdecl{forevery}[args=2] \forevery{\arg[2]{The proposition $P$} \comp{holds for every} \arg[1]{$x\in A$}} } When using |*[|$n$|]|, after reading the provided ($n$th) argument, the ``argument counter'' automatically continues where we left off, so the |*[1]| in the above example can be omitted. For a macro with arity $>0$, we can refer to the operator \emph{itself} semantically by suffixing the semantic macro with an exclamation point |!| in either text or math mode. For that reason \cs{notation} (and thus \cs{symdef}) take an additional optional argument |op=|, which allows to assign a notation for the operator itself. e.g. \stexexample{ \symdef{add}[args=2,op={+}]{#1 \comp+ #2} The operator $\add!$ adds two elements, as in $\add ab$. } |*| is composable with |!| for custom notations, as in: \stexexample{ \mult!{\comp{Multiplication}} (denoted by $\mult!*{\comp\cdot}$) is defined by... } The macro \cs{comp} as used everywhere above is responsible for highlighting, linking, and tooltips, and should be wrapped around the notation (or text) components that should be treated accordingly. While it is attractive to just wrap a whole notation, this would also wrap around e.g. the arguments themselves, so instead, the user is tasked with marking the notation components themself. The precise behaviour of \cs{comp} is governed by the macro \cs{@comp}, which takes two arguments: The tex code of the text (unexpanded) to highlight, and the URI of the current symbol. \cs{@comp} can be safely redefined to customize the behaviour. The starred variant |\symdecl*{foo}| does not introduce a semantic macro, but still declares a corresponding symbol. |foo| (like any other symbol, for that matter) can then be accessed via \cs{STEXsymbol}|{foo}| or (if |foo| was declared in a module |Foo|) via \cs{STEXModule}|{Foo}?{foo}|. both \cs{STEXsymbol} and \cs{STEXModule} take any arbitrary ending segment of a full URI to determine which symbol or module is meant. e.g. \cs{STEXsymbol}|{Foo?foo}| is also valid, as are e.g. \cs{STEXModule}|{path?Foo}?{foo}| or \cs{STEXsymbol}|{path?Foo?foo}| There's also a convient shortcut \cs{symref}|{?foo}{some text}| for \cs{STEXsymbol}|{?foo}![some text]|. \end{smodule} \subsubsection{Other Argument Types} So far, we have stated the arity of a semantic macro directly. This works if we only have ``normal'' (or more precisely: |i|-type) arguments. To make use of other argument types, instead of providing the arity numerically, we can provide it as a sequence of characters representing the argument types -- e.g. instead of writing |args=2|, we can equivalently write |args=ii|, indicating that the macro takes two |i|-type arguments. Besides |i|-type arguments, \sTeX has two other types, which we will discuss now. The first are \emph{binding} (|b|-type) arguments, representing variables that are \emph{bound} by the operator. This is the case for example in the above \cs{forevery}-macro: The first argument is not actually an argument that the |forevery| ``function'' is ``applied'' to; rather, the first argument is a new variable (e.g. $x$) that is \emph{bound} in the subsequent argument. More accurately, the macro should therefore have been implemented thusly: \begin{center}|\symdef{forevery}[args=bi]{\forall #1.\; #2}|\end{center} \begin{smodule}{OtherArgs} |b|-type arguments are indistinguishable from |i|-type arguments within \sTeX, but are treated very differently in \omdoc and by \mmt. More interesting \emph{within} \sTeX are |a|-type arguments, which represent (associative) arguments of flexible arity, which are provided as comma-separated lists. This allows e.g. better representing the \cs{mult}-macro above: \stexexample{ \symdef{mult}[args=a]{#1}{##1 \comp\cdot ##2} $\mult{a,b,c,{d^e},f}$ } As the example above shows, notations get a little more complicated for associative arguments. For every |a|-type argument, the \cs{notation}-macro takes an additional argument that declares how individual entries in an |a|-type argument list are aggregated. The first notation argument then describes how the aggregated expression is combined into the full representation. For a more interesting example, consider a flexary operator for ordered sequences in ordered set, that taking arguments |{a,b,c}| and |\mathbb{R}| prints $a \leq b \leq c\in \mathbb R$. This operator takes two arguments (an |a|-type argument and an |i|-type argument), aggregates the individuals of the associative argument using |\leq|, and combines the result with |\in| and the second argument thusly: \stexexample{ \symdef{numseq}[args=ai]{#1 \comp\in #2}{##1 \comp\leq ##2} $\numseq{a,b,c}{\mathbb R}$ } Finally, |B|-type arguments combine the functionalities of |a| and |b|, i.e. they represent flexary binding operator arguments. \ednote{what about e.g. \detokenize{\int_x\int_y\int_z f dx dy dz}?} \ednote{``decompose'' a-type arguments into fixed-arity operators?} \end{smodule} \subsubsection{Precedences} Every notation has an (upwards) \emph{operator precedence} and for each argument a (downwards) \emph{argument precedence} used for automated bracketing. For example, a notation for a binary operator \cs{foo} could be declared like this: \begin{center} |\notation{foo}[prec=200;500x600]{#1 \comp{+} #2}| \end{center} assigning an operator precedence of 200, an argument precedence of 500 for the first argument, and an argument precedence of 600 for the second argument. \sTeX insert brackets thusly: Upon encountering a semantic macro (such as \cs{foo}), its operator precedence (e.g. 200) is compared to the current downwards precedence (initially \cs{neginfprec}). If the operator precedence is \emph{larger} than the current downwards precedence, parentheses are inserted around the semantic macro. Notations for symbols of arity 0 have a default precedence of \cs{infprec}, i.e. by default, parentheses are never inserted around constants. Notations for symbols with arity $>0$ have a default operator precedence of $0$. If no argument precedences are explicitly provided, then by default they are equal to the operator precedence. Consequently, if some operator $A$ should bind stronger than some operator $B$, then $A$s operator precedence should be smaller than $B$s argument precedences. For example: \begin{smodule}{NotationsEx} \symdecl{plus}[args=2] \symdecl{times}[args=2] \stexexample{ \notation{plus}[prec=100]{#1 \comp{+} #2} \notation{times}[prec=50]{#1 \comp{\cdot} #2} $\plus{a}{\times{b}{c}}$ and $\times{a}{\plus{b}{c}}$ } \end{smodule} \subsection{Archives and Imports} \subsubsection{Namespaces} Ideally, \sTeX would use arbitrary URIs for modules, with no forced relationships between the \emph{logical} namespace of a module and the \emph{physical} location of the file declaring the module -- like \mmt does things. Unfortunately, \TeX\ only provides very restricted access to the file system, so we are forced to generate namespaces systematically in such a way that they reflect the physical location of the associated files, so that \sTeX can resolve them accordingly. Largely, users need not concern themselves with namespaces at all, but for completenesses sake, we describe how they are constructed: \begin{itemize} \item If \cs{begin}|{module}{Foo}| occurs in a file |/path/to/file/Foo[.|\meta{lang}|].tex| which does not belong to an archive, the namespace is |file://path/to/file|. \item If the same statement occurs in a file |/path/to/file/bar[.|\meta{lang}|].tex|, the namespace is |file://path/to/file/bar|. \end{itemize} In other words: outside of archives, the namespace corresponds to the file URI with the filename dropped iff it is equal to the module name, and ignoring the (optional) language suffix^^A \footnote{which is internally attached to the module name instead, but a user need not worry about that.}. If the current file is in an archive, the procedure is the same except that the initial segment of the file path up to the archive's |source|-folder is replaced by the archive's namespace URI. \subsubsection{Paths in Import-Statements} Conversely, here is how namespaces/URIs and file paths are computed in import statements, examplary \cs{importmodule}: \begin{itemize} \item \cs{importmodule}|{Foo}| outside of an archive refers to module |Foo| in the current namespace. Consequently, |Foo| must have been declared earlier in the same document or, if not, in a file |Foo[.|\meta{lang}|].tex| in the same directory. \item The same statement \emph{within} an archive refers to either the module |Foo| declared earlier in the same document, or otherwise to the module |Foo| in the archive's top-level namespace. In the latter case, is has to be declared in a file |Foo[.|\meta{lang}|].tex| directly in the archive's |source|-folder. \item Similarly, in \cs{importmodule}|{some/path?Foo}| the path |some/path| refers to either the sub-directory and relative namespace path of the current directory and namespace outside of an archive, or relative to the current archive's top-level namespace and |source|-folder, respectively. The module |Foo| must either be declared in the file \meta{top-directory}|/some/path/Foo[.|\meta{lang}|].tex|, or in \meta{top-directory}|/some/path[.|\meta{lang}|].tex| (which are checked in that order). \item Similarly, \cs{importmodule}|[Some/Archive]{some/path?Foo}| is resolved like the previous cases, but relative to the archive |Some/Archive| in the mathhub-directory. \item Finally, \cs{importmodule}|{full://uri?Foo}| naturally refers to the module |Foo| in the namespace |full://uri|. Since the file this module is declared in can not be determined directly from the URI, the module must be in memory already, e.g. by being referenced earlier in the same document. Since this is less compatible with a modular development, using full URIs directly is discouraged. \end{itemize} \csname if@infulldoc\endcsname\else\end{document}\fi