diff options
author | Norbert Preining <norbert@preining.info> | 2023-03-22 03:01:52 +0000 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2023-03-22 03:01:52 +0000 |
commit | cbbc6dbdbf08b70a7e7d8d184ca51c57c835415a (patch) | |
tree | 97ded8ca7095c54f6ff9b661be6b93f80bf792c4 /macros/latex/contrib/stex/doc/stex-manual.tex | |
parent | de9a0afa47c2ee09e1d4704821cad2b231d36b3f (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.tex | 563 |
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 |