diff options
author | Norbert Preining <norbert@preining.info> | 2022-05-25 03:01:13 +0000 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2022-05-25 03:01:13 +0000 |
commit | f01a37f8311f33e32441d25bdadcda9dcdbd165d (patch) | |
tree | efb861dfafff09d4bef8024c85a11f8c8deaba76 /macros/latex/contrib/stex/doc/stex-manual.tex | |
parent | 0c7d079315627312627c83bc9ce6f5e4f1b436f6 (diff) |
CTAN sync 202205250301
Diffstat (limited to 'macros/latex/contrib/stex/doc/stex-manual.tex')
-rw-r--r-- | macros/latex/contrib/stex/doc/stex-manual.tex | 972 |
1 files changed, 365 insertions, 607 deletions
diff --git a/macros/latex/contrib/stex/doc/stex-manual.tex b/macros/latex/contrib/stex/doc/stex-manual.tex index 92834af1c5..31b9c4eaeb 100644 --- a/macros/latex/contrib/stex/doc/stex-manual.tex +++ b/macros/latex/contrib/stex/doc/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 |