\makeatletter \ifcsname if@infulldoc\endcsname\else \expandafter\newif\csname if@infulldoc\endcsname\@infulldocfalse \fi \makeatother \csname if@infulldoc\endcsname\else \def\bibfolder#1{../lib/bib/#1} \input{stex-docheader} \infulldoctrue \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-doc.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{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) 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 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} \end{sfragment} \begin{sfragment}{Quickstart} \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 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)://:" \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||. Every \sTeX archive as an \textbf{archive path} \lstinline|| and a name \lstinline||. We can clone the \sTeX archive by the following command-line instructions: \begin{lstlisting}[language=bash] cd / git clone https://gl.mathhub.info/smglom/.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="'' \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 \mmt System} available \href{https://github.com/uniformal/MMT/tree/sTeX}{here}. 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 \textbf{\sTeX Archives} If we only care about {\LaTeX} and generating |pdf|s, we do not technically need \mmt at all; however, we still need the |MATHHUB| system variable to be set. Furthermore, \mmt can make downloading content archives we might want to use significantly easier, since it makes sure that all dependencies of (often highly interrelated) \sTeX archives are cloned as well. Once set up, we can run |mmt| in a shell and download an archive along with all of its dependencies like this: |lmh install |, or a whole \emph{group} of archives; for example, |lmh install smglom| will download all smglom archives. \item \textbf{\RusTeX} The \mmt system will also set up \RusTeX for you, which is used to generate (semantically annotated) |xhtml| from tex sources. In lieu of using \mmt, you can also download and use \RusTeX directly \href{https://github.com/slatex/RusTeX}{here}. \end{itemize} \end{sfragment} \end{sfragment} \input{stex-tutorial} \end{sfragment} \begin{sfragment}{Creating \sTeX Content} \input{packages/stex-basics} \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.decls]{Module, Symbol and Notation Declarations} \input{packages/stex-modules} \input{packages/stex-symbols} \end{sfragment} \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=|, \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=]{Foo}". \iffalse\end{smodule}\fi \begin{mmtbox} Technically, each |smodule|-environment induces \emph{two} \omdoc/\mmt theories: \stexcode"\begin{smodule}[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?| 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". \end{sfragment} \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}[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*[]{}{}". After \stex reads and processes the optional arguments for these environments, (some of) their values are stored in the macros \stexcode"\s*" (i.e. \stexcode"sexampleid", \stexcode"\sassertionname", etc.). It then checks for all the values || in the |type=|-list, whether an \stexcode"\stexpatch*[]" for the current environment has been called. If it finds one, it uses the patches || and || 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} \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}{Representing Problems and Solutions} \input{packages/stex-problem} \end{sfragment} \begin{sfragment}{Homeworks, Quizzes and Exams} \input{packages/stex-hwexam} \end{sfragment} \end{sfragment} \csname if@infulldoc\endcsname\else \newpage \printbibliography \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