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.tex972
1 files changed, 365 insertions, 607 deletions
diff --git a/Master/texmf-dist/doc/latex/stex/stex-manual.tex b/Master/texmf-dist/doc/latex/stex/stex-manual.tex
index 92834af1c5e..31b9c4eaeb2 100644
--- a/Master/texmf-dist/doc/latex/stex/stex-manual.tex
+++ b/Master/texmf-dist/doc/latex/stex/stex-manual.tex
@@ -6,14 +6,12 @@
\csname if@infulldoc\endcsname\else
-\def\bibfolder{../lib/bib}
+\def\bibfolder#1{../lib/bib/#1}
\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{
@@ -33,7 +31,7 @@
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}
+ \href{\basedocurl/stex-doc.pdf}{the \sTeX documentation}.
\makeatletter
\renewcommand\part{%
@@ -137,6 +135,19 @@
\long\def\ignore#1{}
+\begin{dangerbox}
+ Boxes like this one contain implementation details that are
+ mostly relevant for more advanced use cases, might be useful
+ to know when debugging, or might be good to know to better understand
+ how something works. They can easily be skipped on a first read.
+\end{dangerbox}
+
+\begin{mmtbox}
+ Boxes like this one explain how some \sTeX concept relates to the \mmt/\omdoc system,
+ philosophy or language; see \cite{uniformal:on,Kohlhase:OMDoc1.2} for introductions.
+\end{mmtbox}
+
+
\begin{sfragment}{What is \sTeX?}
Formal systems for mathematics (such as interactive theorem provers)
@@ -173,143 +184,98 @@ 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.
+\item The \sTeX package collection to use semantic annotations in {\LaTeX} documents,
+\item \RusTeX \cite{RusTeX:on} to convert |tex| sources to (semantically enriched) |xhtml|,
+\item The \mmt system~\cite{uniformal:on}, that extracts semantic information from the
+ thus generated |xhtml| and provides semantically informed added value services.
+ Notably, \mmt integrates the \RusTeX system already.
\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{sfragment}{Setup}
+ There are two ways of using \sTeX: as a
+ \begin{enumerate}
+ \item way of writing {\LaTeX} more modularly (object-oriented Math) for creating PDF
+ documents or
+ \item foundation for authoring active documents in HTML5 instrumented with knowledge
+ management services.
+ \end{enumerate}
+ Both are legitimate and useful. The first requires a significantly smaller
+ tool-chain, so we describe it first. The second requires a much more substantial
+ (and experimental) toolchain of knowledge management systems. Both workflows profit
+ from an integrated development environment (IDE), which (also) automates setup as
+ far as possible (see \sref{sec.sTeX-IDE}).
+
+ \begin{sfragment}[id=sec.minimal-setup]{Minimal Setup for the PDF-only Workflow}
+ In the best of all worlds, there is no setup, as you already have a new version of
+ {\TeX}Live on your system as a {\LaTeX} enthusiast. If not now is the time to
+ install it; see \cite{TeXLive:on}. You can usually update {\TeX}Live via a package
+ manager or the {\TeX}Live manager \textbf{tlmgr}.
+
+ Alternatively, you can install \sTeX from CTAN, the Comprehensive {\TeX} Archive
+ Network; see \cite{stexCTAN:on} for details.
+ \end{sfragment}
+
+ \begin{sfragment}[id=sec.git-setup]{GIT-based Setup for the \sTeX Development Version}
+ If you want use the latest and greatest \sTeX packages
+ that have not even been released to CTAN,
+ then you can directly clone them from the \sTeX development
+ repository \cite{sTeX:github:on} by the following command-line instructions:
+\begin{lstlisting}[language=bash]
+ cd <stexdir>
+ git clone https://github.com/slatex/sTeX.git
+\end{lstlisting}
+ and keep it updated by pulling updates via \lstinline|git pull| in the cloned \sTeX
+ directory.
+ Then update your \lstinline|TEXINPUTS| environment variable, e.g. by placing the following line in your \lstinline|.bashrc|:
+\begin{lstlisting}[language=bash]
+export TEXINPUTS="$(TEXINPUTS):<sTeXDIR>//:"
+\end{lstlisting}
+ \end{sfragment}
+
+ \begin{sfragment}[id=sec.stex-archives]{\sTeX Archives (Manual Setup)}
+ Writing semantically annotated \sTeX becomes much easier, if we can use
+ well-designed libraries of already annotated content. \sTeX provides such
+ libraries as \sTeX archives -- i.e. GIT repositories at
+ \url{https://gl.mathhub.info} -- most prominently the SMGLoM libraries at
+ \url{https://gl.mathhub.info/smglom}.
+
+ To do so, we set up a \textbf{local MathHub} by creating a MathHub directory
+ \lstinline|<mhdir>|. Every \sTeX archive as an \textbf{archive path}
+ \lstinline|<apath>| and a name \lstinline|<archive>|. We can clone the \sTeX
+ archive by the following command-line instructions:
+\begin{lstlisting}[language=bash]
+ cd <mhdir>/<apath>
+ git clone https://gl.mathhub.info/smglom/<archive>.git
+\end{lstlisting}
+ Note that \sTeX archives often depend on other archives, thus you should be
+ prepared to clone these as well -- e.g. if \texttt{pdflatex} reports missing
+ files.
+ 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}).
+\begin{lstlisting}[language=bash]
+export MATHHUB="<mhdir>''
+\end{lstlisting}
+ \end{sfragment}
+
+ \begin{sfragment}[id=sec.sTeX-IDE]{The \sTeX IDE}
+ We are currently working on an \sTeX IDE as an \sTeX plugin for |VScode|;
+ see~\cite{sTeX-IDE:on}. It will feature a setup procedure that automates the setup
+ described above (and below). For additional functionality see the (now obsolete)
+ plugin for \sTeX1 \cite{stexls:on,stexls-vscode-plugin:on}.
+ \end{sfragment}
+
+ \begin{sfragment}{Manual Setup for Active Documents and Knowledge Management Services}
+ Foregoing on the \sTeX IDE, we will need several additional (on top of the minimal
+ setup above) 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
+ \href{https://github.com/uniformal/MMT/tree/sTeX}{here}.
+ We recommend following
the setup routine documented
\href{https://uniformal.github.io//doc/setup/}{here}.
@@ -317,513 +283,305 @@ which can thus be integrated as additional services into the system.
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
+ \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}}
+ \end{sfragment}
+
+ \input{stex-tutorial}
-\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}
+\begin{sfragment}{Creating \sTeX Content}
+
\input{packages/stex-basics}
-
- \input{packages/stex-terms}
- \input{packages/stex-references}
-\end{sfragment}
+ \begin{sfragment}{How Knowledge is Organized in \sTeX}
+
+ \sTeX content is organized on multiple levels:
+ \begin{enumerate}
+ \item \sTeX \textbf{archives} (see \sref{sec.stexarchives})
+ contain individual |.tex|-files.
+ \item These may contain \sTeX \textbf{modules}, introduced via
+ \stexcode"\begin{smodule}{ModuleName}".\iffalse\end{smodule}\fi
+ \item Modules contain \sTeX \textbf{symbol declarations}, introduced via
+ \stexcode"\symdecl{symbolname}", \stexcode"\symdef{symbolname}" and some other
+ constructions. Most symbols have a \emph{notation} that can
+ be used via a \emph{semantic macro} \stexcode"\symbolname" generated
+ by symbol declarations.
+ \item \sTeX \textbf{expressions} finally are built up from
+ usages of semantic macros.
+ \end{enumerate}
+
+ \begin{mmtbox}
+ \begin{itemize}
+ \item \sTeX archives are simultaneously \mmt archives, and the same directory
+ structure is consequently used.
+ \item \sTeX modules correspond to \omdoc/\mmt \emph{theories}.
+ \stexcode"\importmodule"s (and similar constructions) induce \mmt |include|s and
+ other \emph{theory morphisms}, thus giving rise to a \emph{theory graph} in the
+ \omdoc sense~\cite{RabKoh:WSMSML13}.
+ \item Symbol declarations induce \omdoc/\mmt \emph{constants}, with optional
+ (formal) \emph{type} and \emph{definiens} components.
+ \item Finally, \sTeX expressions are converted to \omdoc/\mmt terms, which use the
+ abstract syntax (and XML encoding) of \openmath \cite{BusCapCar:2oms04}.
+ \end{itemize}
+ \end{mmtbox}
+ \end{sfragment}
-\begin{sfragment}[id=sec.stexarchives]{\sTeX Archives}
- \input{packages/stex-mathhub}
-\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}
+ \begin{sfragment}[id=sec.decls]{Module, Symbol and Notation Declarations}
+ \input{packages/stex-modules}
+ \input{packages/stex-symbols}
+ \end{sfragment}
- \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}
+ \begin{sfragment}{Module Inheritance and Structures}
+ The \sTeX features for modular document management are inherited from the OMDoc/MMT
+ model that organizes knowledge into a graph, where the nodes are theories (called
+ modules in \sTeX) and the edges are truth-preserving mappings (called theory
+ morphismes in MMT). We have already seen modules/theories above.
+
+ Before we get into theory morphisms in \sTeX we will see a very simple application of
+ modules: managing multilinguality modularly.
+
+ \begin{sfragment}{Multilinguality and Translations}
+
+ If we load the \sTeX document class or package with the option |lang=<lang>|, \sTeX
+ will load the appropriate \pkg{babel} language for you -- e.g. |lang=de| will load
+ the babel language |ngerman|. Additionally, it makes \sTeX aware of the current
+ document being set in (in this example) \emph{german}. This matters for reasons
+ other than mere \pkg{babel}-purposes, though:
+
+ Every \emph{module} is assigned a language. If no \sTeX
+ package option is set that allows for inferring a language,
+ \sTeX will check whether the current file name ends in
+ e.g. |.en.tex| (or |.de.tex| or |.fr.tex|, or...) and
+ set the language accordingly. Alternatively, a language
+ can be explicitly assigned via
+ \stexcode"\begin{smodule}[lang=<language>]{Foo}".
+ \iffalse\end{smodule}\fi
- \input{packages/stex-symbols}
+ \begin{mmtbox}
+ Technically, each |smodule|-environment induces \emph{two}
+ \omdoc/\mmt theories:
+ \stexcode"\begin{smodule}[lang=<lang>]{Foo}"
+ \iffalse\end{smodule}\fi
+ generates a theory |some/namespace?Foo| that only contains
+ the ``formal'' part of the module -- i.e. exactly the
+ content that is exported when using \stexcode"\importmodule".
+
+ Additionally, \mmt generates a \emph{language theory}
+ |some/namespace/Foo?<lang>| that includes |some/namespace?Foo|
+ and contains all the other document content -- variable
+ declarations, includes for each \stexcode"\usemodule", etc.
+ \end{mmtbox}
+
+ Notably, the language suffix in a filename is ignored
+ for \stexcode"\usemodule", \stexcode"\importmodule"
+ and in generating/computing URIs for modules. This however
+ allows for providing \emph{translations} for modules
+ between languages without needing to duplicate content:
+
+ If a module |Foo| exists in e.g. english in a file |Foo.en.tex|,
+ we can provide a file |Foo.de.tex| right next to it, and write
+ \stexcode"\begin{smodule}[sig=en]{Foo}".
+ \iffalse\end{smodule}\fi
+ The |sig|-key then signifies, that the ``signature'' of the
+ module is contained in the \emph{english} version of the module,
+ which is immediately imported from there, just like
+ \stexcode"\importmodule" would.
+
+ Additionally to translating the informal content of a module
+ file to different languages, it also allows for customizing
+ notations between languages. For example,
+ the \emph{least common multiple} of two numbers is often
+ denoted as $\mathtt{lcm}(a,b)$ in english, but is
+ called \emph{kleinstes gemeinsames Vielfaches} in german
+ and consequently denoted as $\mathtt{kgV}(a,b)$ there.
+
+ We can therefore imagine a german version of an lcm-module
+ looking something like this:
+
+ \begin{latexcode}[gobble=8]
+ \begin{smodule}[sig=en]{lcm}
+ \notation*{lcm}[de]{\comp{\mathtt{kgV}}(#1,#2)}
+
+ Das \symref{lcm}{kleinste gemeinsame Vielfache}
+ $\lcm{a,b}$ von zwei Zahlen $a,b$ ist...
+ \end{smodule}
+ \end{latexcode}
+
+ If we now do \stexcode"\importmodule{lcm}"
+ (or \stexcode"\usemodule{lcm}") within a \emph{german} document,
+ it will also load the content of the german translation,
+ including the |de|-notation for \stexcode"\lcm".
- \input{packages/stex-inheritance}
+ \end{sfragment}
- \begin{sfragment}{Advanced Structuring Mechanisms}
+ \input{packages/stex-inheritance}
\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}
+\begin{sfragment}[id=sec.textsymbols]{Using \sTeX Symbols}
+ \input{packages/stex-terms}
+ \input{packages/stex-references}
+\end{sfragment}
+\begin{sfragment}{\sTeX Statements}
+ \input{packages/stex-statements}
\input{packages/stex-proofs}
\end{sfragment}
+\begin{sfragment}[id=sec.customhighlight]{Highlighting and Presentation Customizations}
+
+ The environments starting with |s| (i.e. \stexcode"smodule", \stexcode"sassertion",
+ \stexcode"sexample", \stexcode"sdefinition", \stexcode"sparagraph" and
+ \stexcode"sproof") by default produce no additional output whatsoever (except for the
+ environment content of course). Instead, the document that uses them (whether directly
+ or e.g. via \stexcode"\inputref") can decide how these environments are supposed to look
+ like.
+
+ The \pkg{stexthm} package defines some default customizations that can be used, but of
+ course many existing \LaTeX\xspace templates come with their own |definition|, |theorem|
+ and similar environments that authors are supposed (or even required) to use. Their
+ concrete syntax however is usually not compatible with all the additional arguments that
+ \sTeX allows for semantic information.
+
+ Therefore we introduced the separate environments \stexcode"sdefinition" etc. instead of
+ using \stexcode"definition" directly. We allow authors to specify how these environments
+ should be styled via the commands \stexcode"stexpatch*".
+
+ \begin{function}{\stexpatchmodule,\stexpatchdefinition,
+ \stexpatchassertion,\stexpatchexample,\stexpatchparagraph,
+ \stexpatchproof}
+ All of these commands take one optional and two proper arguments, i.e.\\
+ \stexcode"\stexpatch*[<type>]{<begin-code>}{<end-code>}".
+
+ After \stex reads and processes the optional arguments for these environments, (some
+ of) their values are stored in the macros \stexcode"\s*<field>"
+ (i.e. \stexcode"sexampleid", \stexcode"\sassertionname", etc.). It then checks for all
+ the values |<type>| in the |type=|-list, whether an \stexcode"\stexpatch*[<type>]" for
+ the current environment has been called. If it finds one, it uses the patches
+ |<begin-code>| and |<end-code>| to mark up the current environment. If no patch for
+ (any of) the type(s) is found, it checks whether and \stexcode"\stexpatch*" was called
+ without optional argument.
+ \end{function}
+
+ For example, if we want to use a predefined |theorem| environment for
+ \stexcode"sassertion"s with |type=theorem|, we can do
+\begin{latexcode}
+\stexpatchassertion[theorem]{\begin{theorem}}{\end{theorem}}
+\end{latexcode}
+ ...or, rather, since e.g. |theorem|-like environments defined using \pkg{amsthm} take an
+ optional title as argument, we can do:
+\begin{latexcode}
+\stexpatchassertion[theorem]
+ {\ifx\sassertiontitle\@empty
+ \begin{theorem}
+ \else
+ \begin{theorem}[\sassertiontitle]
+ \fi}
+ {\end{theorem}}
+\end{latexcode}
+
+ Or, if we want \emph{all kinds of} \stexcode"sdefinition"s to use a predefined
+ |definition|-environment irrespective of their |type=|, then we can issue the following
+ customization patch:
+\begin{latexcode}
+\stexpatchdefinition
+ {\ifx\sdefinitiontitle\@empty
+ \begin{definition}
+ \else
+ \begin{definition}[\sdefinitiontitle]
+ \fi}
+ {\end{definition}}
+\end{latexcode}
+
+ \begin{function}{\compemph,\varemph,\symrefemph,\defemph}
+ Apart from the environments, we can control how \sTeX highlights variables, notation
+ components, \stexcode"\symref"s and \stexcode"\definiendum"s, respectively.
+
+ To do so, we simply redefine these four macros. For example, to highlight notation
+ components (i.e. everything in a \stexcode"\comp") in blue, as in this document, we
+ can do \stexcode"\def\compemph#1{\textcolor{blue}{#1}}". By default, |\compemph| et
+ al do nothing.
+ \end{function}
+
+ \begin{function}{\compemph@uri,\varemph@uri,\symrefemph@uri,\defemph@uri}
+ For each of the four macros, there exists an additional macro that takes the full URI
+ of the relevant symbol currently being highlighted as a second argument. That allows
+ us to e.g. use pdf tooltips and links. For example, this document uses\Ednote{MK: why
+ |protected|, ... if we show that, then we should explain.}
+\begin{latexcode}
+\protected\def\symrefemph@uri#1#2{
+ \pdftooltip{
+ \srefsymuri{#2}{\symrefemph{#1}}
+ }{
+ URI:~\detokenize{#2}
+ }
+}
+\end{latexcode}
+ By default, |\compemph@uri| is simply defined as |\compemph{#1}| (analogously for the
+ other three commands).
+\end{function}
+\end{sfragment}
+
\begin{sfragment}{Additional Packages}
- \input{packages/stex-tikzinput}
+ \begin{sfragment}{Tikzinput: Treating TIKZ code as images}
+ \input{packages/stex-tikzinput}
+ \end{sfragment}
\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}
+ \begin{sfragment}{Representing Problems and Solutions}
\input{packages/stex-problem}
-
- \input{packages/stex-hwexam}
\end{sfragment}
-
+ \begin{sfragment}{Homeworks, Quizzes and Exams}
+ \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
+\newpage
+\printbibliography
+\end{document}
+\fi
-
-
-\csname if@infulldoc\endcsname\else\end{document}\fi
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+
+% LocalWords: stex-docheader infulldoctrue l@subsubsection toclevel@part ExplSyntaxOff
+% LocalWords: l_document_structure_section_level_int dangerbox mmtbox omdoc OBJref lmh
+% LocalWords: own:fifom MueRabRot:rslffml20 sec.stexarchives stex-mathhub ngerman a,b
+% LocalWords: Metatheory sec.customhighlight sproof stexthm xspace stexpatchmodule
+% LocalWords: stexpatchexample stexpatchparagraph sexampleid amsthm sassertiontitle
+% LocalWords: sdefinitiontitle compemph varemph srefsymuri stex-hwexam TeXLive:on tlmgr
+% LocalWords: stexls:on,stexls-vscode-plugin:on