
\ifcsname ifinfulldoc\endcsname\else
    \expandafter\newif\csname ifinfulldoc\endcsname\infulldocfalse
\fi
\ifcsname ifinidedoc\endcsname\else
    \expandafter\newif\csname ifinidedoc\endcsname\inidedocfalse
\fi

\ifinfulldoc\else
  \input{stex-docheader}

\begin{document}
	\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}{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
    toolchain of knowledge management systems. 
    
    Luckily, the \sTeX-IDE will take care of much of the setup required
    for the full toolchain, if you are willing to use it.

    \input{packages/stex-setup}

    \input{packages/stex-idesetup}

    \begin{sfragment}{Manual Setup}

      In lieu of using the \sTeX IDE, we can do the following:

    \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}{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 <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}
\end{sfragment}

\begin{sfragment}[id=sec.sTeX-IDE]{The \sTeX IDE}
  \input{stex-ide}
\end{sfragment}

\input{stex-tutorial}


\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=<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

      \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".

    \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}

\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{
    \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}
\end{sfragment}
\begin{sfragment}[id=sec.references]{Cross References}
  \input{packages/stex-references}
\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-notesslides}
  \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}

\ifinfulldoc\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
