summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/doc/stex-manual.tex
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2023-03-22 03:01:52 +0000
committerNorbert Preining <norbert@preining.info>2023-03-22 03:01:52 +0000
commitcbbc6dbdbf08b70a7e7d8d184ca51c57c835415a (patch)
tree97ded8ca7095c54f6ff9b661be6b93f80bf792c4 /macros/latex/contrib/stex/doc/stex-manual.tex
parentde9a0afa47c2ee09e1d4704821cad2b231d36b3f (diff)
CTAN sync 202303220301
Diffstat (limited to 'macros/latex/contrib/stex/doc/stex-manual.tex')
-rw-r--r--macros/latex/contrib/stex/doc/stex-manual.tex563
1 files changed, 0 insertions, 563 deletions
diff --git a/macros/latex/contrib/stex/doc/stex-manual.tex b/macros/latex/contrib/stex/doc/stex-manual.tex
deleted file mode 100644
index 547e238f54..0000000000
--- a/macros/latex/contrib/stex/doc/stex-manual.tex
+++ /dev/null
@@ -1,563 +0,0 @@
-
-\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