summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/stex/stex-manual.tex
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/doc/latex/stex/stex-manual.tex')
-rw-r--r--Master/texmf-dist/doc/latex/stex/stex-manual.tex829
1 files changed, 829 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/stex/stex-manual.tex b/Master/texmf-dist/doc/latex/stex/stex-manual.tex
new file mode 100644
index 00000000000..92834af1c5e
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/stex/stex-manual.tex
@@ -0,0 +1,829 @@
+\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 <name-of-repository>|,
+ 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