diff options
Diffstat (limited to 'Master/texmf-dist/doc/latex')
24 files changed, 3521 insertions, 933 deletions
diff --git a/Master/texmf-dist/doc/latex/stex/README.md b/Master/texmf-dist/doc/latex/stex/README.md index 13caa1f7342..b5eed1a41fa 100644 --- a/Master/texmf-dist/doc/latex/stex/README.md +++ b/Master/texmf-dist/doc/latex/stex/README.md @@ -3,8 +3,13 @@ sTeX: An Infrastructure for Semantic Preloading of LaTeX Documents ![CI Status](https://github.com/slatex/sTeX/workflows/CI/badge.svg) This repository contains the sTeX package collection, a version of TeX/LaTeX that allows -to markup TeX/LaTeX documents semantically without leaving the document format, -essentially turning it into a document format for mathematical knowledge management (MKM). +to markup TeX/LaTeX documents semantically without leaving the document format. + +Running `pdflatex` over sTeX-annotated documents formats them into normal-looking PDF. But +sTeX also comes with a [conversion pipeline](https://github.com/slatex/RusTeX) into +semantically annotated HTML5, which can host semantic added-value services that make the +documents active (i.e. interactive and user-adaptive) and essentially turning LaTeX into a +document format for (mathematical) knowledge management (MKM). ## Copyright & License @@ -12,12 +17,41 @@ Copyright (c) 2022 Michael Kohlhase The package is distributed under the terms of the LaTeX Project Public License (LPPL) ## Maintainers -Michael Kohlhase, Dennis Müller, FAU Erlangen-Nürnberg. +[Michael Kohlhase](https://kwarc.info/kohlhase), [Dennis Müller](https://kwarc.info/people/dmueller), FAU Erlangen-Nürnberg. ## Documentation -See the -[documentation of the sTeX package](https://github.com/slatex/sTeX/blob/main/doc/stex-doc.pdf) -for details. +The [sTeX manual ](https://github.com/slatex/sTeX/blob/main/doc/stex-manual.pdf) gives a +general introduction and motivation. The +[sTeX package documentation](https://github.com/slatex/sTeX/blob/main/doc/stex-doc.pdf) +gives the details of the implementation. A complete list of sTeX-related publications can +be found [here](https://kwarc.github.io/bibs/sTeX/). + +## sTeX Corpus & Best Practices + +sTeX comes with a large corpus of pre-annotated materials that act as evaluation grounds +and regression tests for the sTeX functionality and best practices that are publicly +available. +* [HelloWorld](https://gl.mathhub.info/HelloWorld) a collection of simple hello world + examples the show off the best practices of sTeX annotation. +* [SMGLoM](https://gl.mathhub.info/smglom), the Semantic, Multilingual Glossary of + Mathematics (and similar disciplines). SMGloM provides a large set of definitions and + well-designed semantic macros for core mathematical (and computation) concepts and + objects. This resource greatly facilitates "getting off the ground" in semantic + annotation. +* [MiKoMH](https://gl.mathhub.info/MiKoMH) a set of semantically annotated courses in + computer science and (symbolic) AI (ca. 5000 pages of slides and notes). Ca. 3000 + problem/solutions exist are only available upon request. +* [sTeX3 Labs](https://gl.mathhub.info/sTeX) a set of experimental re-formalizations of + (mostly) [SMGLoM](https://gl.mathhub.info/smglom) material to fully take advantage of + the sTeX3 functionality and the + [rusTeX](https://github.com/slatex/RusTeX)/[MMT](https://uniformal.github.io) pipeline + and knowledge managemen facilities. + +All of these are hosted on [MathHub](https://mathhub.info), an experimental portal for the +management of active mathematical documents and flexiformal mathematics. The organization +of the material into "mathematical archives" (GIT repositories with a particular +standardized structure on [a GitLab repository management server](https://gl.mathhub.info) +greatly enhances modularization and the provision of added value services. ## Setup @@ -31,10 +65,10 @@ Then update your `TEXINPUTS` environment variable, e.g. by placing the followin export TEXINPUTS="$(TEXINPUTS):<sTeXDIR>//: ``` -Similarly, set your `MATHHUB` environment variable to where you intend to keep your sTeX archives. For details, see the documentation linked above. +Similarly, set your `MATHHUB` environment variable to where you intend to keep your sTeX +archives. For details, see the documentation linked above. For a LaTeX IDE, update the directory path where `pdflatex` looks for paths. -For a LaTeX IDE, update the directory path where `pdflatex` looks for paths. -For larger documents it may be necessary to enlarge the internal memory allocation of the TEX/LATEX executables. This can be done by adding the following configurations in `texmf.cnf` (or changing them, if they already exist). +For larger documents it may (rarely) be necessary to enlarge the internal memory allocation of the TEX/LATEX executables. This can be done by adding the following configurations in `texmf.cnf` (or changing them, if they already exist). ``` param_size = 20000 % simultaneous macro parameters, also applies to MP nest_size = 1000 % simultaneous semantic levels (e.g., groups) diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-basics.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-basics.tex index daa6d6418d2..f766b9b22f1 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-basics.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-basics.tex @@ -1,3 +1,9 @@ +We can use \sTeX by simply including the package with |\usepackage{stex}|, +or -- primarily for individual fragments to be included in other +documents -- by using the \sTeX document class with |\documentclass{stex}| +which combines the \pkg{standalone} document class with the \pkg{stex} +package. + Both the \pkg{stex} package and document class offer the following options: @@ -5,12 +11,31 @@ options: \item[\texttt{lang}] (\meta{language}$\ast$) Languages to load with the \pkg{babel} package. \item[\texttt{mathhub}] (\meta{directory}) MathHub folder - to search for repositories. - \item[\texttt{sms}] (\meta{boolean}) use \emph{persisted} - mode (not yet implemented). + to search for repositories -- this is not necessary if the + |MATHHUB| system variable is set. + \item[\texttt{writesms}] (\meta{boolean}) with this package + option, \sTeX will write the contents of all external + modules imported via \stexcode"\importmodule" or \stexcode"\usemodule" + into a file \stexcode"\jobname.sms" (analogously to + the table of contents \stexcode".toc"-file). + \item[\texttt{usems}] (\meta{boolean}) subsequently tells + \sTeX to read the generated sms-file at the beginning of the + document. This allows for e.g. collaborating on documents + without all authors having to have all used archives and + modules available -- one author can load the modules + with \texttt{writesms}, and the rest can use the + the modules with \texttt{usesms}. Furthermore, the sms + file can be submitted alongside a \texttt{tex}-file, + effectively making it ``standalone''. \item[\texttt{image}] (\meta{boolean}) passed on to \pkg{tikzinput}. \item[\texttt{debug}] (\meta{log-prefix}$\ast$) Logs debugging information with the given prefixes to the terminal, - or all if |all| is given. -\end{description}
\ No newline at end of file + or all if |all| is given. Largely irrelevant for the + majority of users. +\end{description} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-document-structure.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-document-structure.tex index 1c8fe97dac2..f8d570ea5e0 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-document-structure.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-document-structure.tex @@ -1 +1,155 @@ -\textcolor{red}{TODO: document-structure documentation}
\ No newline at end of file +The \pkg{document-structure} package supplies an infrastructure for writing {\omdoc} documents in {\LaTeX}. +This includes a simple structure sharing mechanism for \sTeX that allows to to move from +a copy-and-paste document development model to a copy-and-reference model, which +conserves space and simplifies document management. The augmented structure can be used +by MKM systems for added-value services, either directly from the \sTeX sources, or +after translation. + + + The \pkg{document-structure} package supplies macros and environments that allow to label document + fragments and to reference them later in the same document or in other documents. In + essence, this enhances the document-as-trees model to + documents-as-directed-acyclic-graphs (DAG) model. This structure can be used by MKM + systems for added-value services, either directly from the \sTeX sources, or after + translation. Currently, trans-document referencing provided by this package can only be + used in the \sTeX collection. + + DAG models of documents allow to replace the ``Copy and Paste'' in the source document + with a label-and-reference model where document are shared in the document source and the + formatter does the copying during document formatting/presentation. + +The \pkg{document-structure} package accepts the following options: +\begin{center} + \begin{tabular}{|l|p{10cm}|}\hline + \texttt{class=\meta{name}} & load \meta{name}|.cls| instead of |article.cls|\\\hline + \texttt{topsect=\meta{sect}} & The top-level sectioning level; the default for + \meta{sect} is \texttt{section}\\\hline + \end{tabular} +\end{center} + +\begin{environment}{sfragment} + The structure of the document is given by nested |sfragment| environments. In the + {\LaTeX} route, the |sfragment| environment is flexibly mapped to sectioning commands, + inducing the proper sectioning level from the nesting of |sfragment| + environments. Correspondingly, the |sfragment| environment takes an optional key/value + argument for metadata followed by a regular argument for the (section) title of the + sfragment. The optional metadata argument has the keys |id| for an identifier, + |creators| and |contributors| for the Dublin Core metadata~\cite{DCMI:dmt03}. The option + |short| allows to give a short title for the generated section. If the title contains + semantic macros, they need to be protected by |\protect|\ednote{MK: still?}, and we need + to give the |loadmodules| key it needs no value. For instance we would have +\begin{latexcode} +\begin{smodule}{foo} + \symdef{bar}{B^a_r} + ... + \begin{sfragment}[id=sec.barderiv,loadmodules] + {Introducing $\protect\bar$ Derivations} +\end{latexcode} + +\sTeX automatically computes the sectioning level, from the nesting of |sfragment| +environments. +\end{environment} + +But sometimes, we want to skip levels (e.g. to use a |\subsection*| as an introduction for +a chapter). + +\begin{environment}{blindfragment} + Therefore the \pkg{document-structure} package provides a variant |blindfragment| that + does not produce markup, but increments the sectioning level and logically groups + document parts that belong together, but where traditional document markup relies on + convention rather than explicit markup. The |blindfragment| environment is useful + e.g. for creating frontmatter at the correct level. The example below shows a typical + setup for the outer document structure of a book with parts and chapters. + +\begin{latexcode} +\begin{document} +\begin{blindfragment} +\begin{blindfragment} +\begin{frontmatter} +\maketitle\newpage +\begin{sfragment}{Preface} +... <<preface>> ... +\end{sfragment} +\clearpage\setcounter{tocdepth}{4}\tableofcontents\clearpage +\end{frontmatter} +\end{blindfragment} +... <<introductory remarks>> ... +\end{blindfragment} +\begin{sfragment}{Introduction} +... <<intro>> ... +\end{sfragment} +... <<more chapters>> ... +\bibliographystyle{alpha}\bibliography{kwarc} +\end{document} +\end{latexcode} + +Here we use two levels of |blindfragment|: +\begin{itemize} +\item The outer one groups the introductory parts of the book (which we assume to have a + sectioning hierarchy topping at the part level). This |blindfragment| makes sure that + the introductory remarks become a ``chapter'' instead of a ``part''. +\item The inner one groups the frontmatter\footnote{We shied away from redefining the + |frontmatter| to induce a blindfragment, but this may be the ``right'' way to go in + the future.} and makes the preface of the book a section-level construct.\ednote{MK: + We need a substitute for the ``Note that here the |display=flow| on the |sfragment| + environment prevents numbering as is traditional for prefaces.''} +\end{itemize} +\end{environment} + +\begin{function}{\skipfragment} + The |\skipfragment| ``skips an |sfragment|'', i.e. it just steps the respective sectioning + counter. This macro is useful, when we want to keep two documents in sync structurally, + so that section numbers match up: Any section that is left out in one becomes a + |\skipfragment|. +\end{function} + +\begin{function}{\currentsectionlevel,\CurrentSectionLevel} + The |\currentsectionlevel| macro supplies the name of the current sectioning level, + e.g. ``chapter'', or ``subsection''. |\CurrentSectionLevel| is the capitalized + variant. They are useful to write something like ``In this |\currentsectionlevel|, we + will\ldots'' in an |sfragment| environment, where we do not know which sectioning level we + will end up. +\end{function} + +\begin{function}{\prematurestop,\afterprematurestop} + For prematurely stopping the formatting of a document, \sTeX provides the + |\prematurestop| macro. It can be used everywhere in a document and ignores all input + after that -- backing out of the |sfragment| environment as needed. After that -- and + before the implicit |\end{document}| it calls the internal |\afterprematurestop|, which + can be customized to do additional cleanup or e.g. print the bibliography. + + |\prematurestop| is useful when one has a driver file, e.g. for a course taught multiple + years and wants to generate course notes up to the current point in the lecture. Instead + of commenting out the remaining parts, one can just move the |\prematurestop| macro. + This is especially useful, if we need the rest of the file for processing, e.g. to + generate a theory graph of the whole course with the already-covered parts marked up as + an overview over the progress; see |import_graph.py| from the |lmhtools| + utilities~\cite{lmhtools:github:on}. +\end{function} + +Text fragments and modules can be made more re-usable by the use of global variables. For +instance, the admin section of a course can be made course-independent (and therefore +re-usable) by using variables (actually token registers) |courseAcronym| and |courseTitle| +instead of the text itself. The variables can then be set in the \sTeX preamble of the +course notes file. + +\begin{function}{\setSGvar,\useSGvar} + |\setSGvar{|\meta{vname}|}{|\meta{text}|}| to set the global variable \meta{vname} to + \meta{text} and |\useSGvar{|\meta{vname}|}| to reference it. +\end{function} + +\begin{function}{\ifSGvar} + With|\ifSGvar| we can test for the contents of a global variable: the macro call + |\ifSGvar{|\meta{vname}|}{|\meta{val}|}{|\meta{ctext}|}| tests the content of the global + variable \meta{vname}, only if (after expansion) it is equal to \meta{val}, the + conditional text \meta{ctext} is formatted. +\end{function} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: article.cls topsect DCMI:dmt03 loadmodules lmhtools +% LocalWords: prematurestop afterprematurestop import_graph.py STRlabel STRcopy vname +% LocalWords: STRsemantics setSGvar ifSGvar ctext diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-features.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-features.tex index e70bbaa0e84..b5ce5906d15 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-features.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-features.tex @@ -1,18 +1,173 @@ +\begin{sfragment}{The \texttt{mathstructure} Environment} +\begin{smodule}[ns=https://github.com/slatex/sTeX/doc]{MathStructures} + A common occurence in mathematics is bundling several + interrelated ``declarations'' together into \emph{structures}. + For example: + \begin{itemize} + \item A \emph{monoid} is a structure $\mathstruct{M,\circ,e}$ + with $\circ:M\times M\to M$ and $e\in M$ such that... + \item A \emph{topological space} is a structure + $\mathstruct{X,\mathcal T}$ where $X$ is a set and + $\mathcal T$ is a topology on $X$ + \item A \emph{partial order} is a structure $\mathstruct{S,\leq}$ + where $\leq$ is a binary relation on $S$ such that... + \end{itemize} + + This phenomenon is important and common enough to warrant special + support, in particular because it requires being able + to \emph{instantiate} such structures (or, rather, + structure \emph{signatures}) in order to talk about (concrete + or variable) \emph{particular} monoids, topological spaces, + partial orders etc. + + \begin{environment}{mathstructure} + The \stexcode"mathstructure" environment allows us to do + exactly that. It behaves exactly like the + \stexcode"smodule" environment, but is itself only allowed + inside an \stexcode"smodule" environment, and allows + for instantiation later on. + \end{environment} + + How this works is again best demonstrated by example: + \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2} + \symdef{fun}[args=bi]{#1 \comp\mapsto #2} + \symdef{set}{\comp{\texttt{Set}}} + + \stexexample{% +\begin{mathstructure}{monoid} + \symdef{universe}[type=\set]{\comp{U}} + \symdef{op}[ + args=2, + type=\funtype{\universe,\universe}{\universe}, + op=\circ + ]{#1 \comp{\circ} #2} + \symdef{unit}[type=\universe]{\comp{e}} +\end{mathstructure} + +A \symname{monoid} is... + } + Note that the \stexcode"\symname{monoid}" is appropriately + highlighted and (depending on your pdf viewer) + shows a URI on hovering -- implying that the \stexcode"mathstructure" + environment has generated a \emph{symbol} |monoid| for us. + It has not generated a semantic macro though, since + we can not use the |monoid|-symbol \emph{directly}. Instead, + we can instantiate it, for example for integers: + + \stexexample{% +\symdef{Int}[type=\set]{\comp{\mathbb Z}} +\symdef{addition}[ + type=\funtype{\Int,\Int}{\Int}, + args=2, + op=+ +]{##1 \comp{+} ##2} +\symdef{zero}[type=\Int]{\comp{0}} + +$\mathstruct{\Int,\addition!,\zero}$ is a \symname{monoid}. + } + + So far, we have not actually instantiated |monoid|, but now + that we have all the symbols to do so, we can: + + \stexexample{% +\instantiate{intmonoid}{monoid}{\mathbb{Z}_{+,0}}[ + universe = Int , + op = addition , + unit = zero +] + +$\intmonoid{universe}$, $\intmonoid{unit}$ and $\intmonoid{op}{a}{b}$. + +Also: $\intmonoid!$ + } + \begin{function}{\instantiate} + So summarizing: + \stexcode"\instantiate" takes four arguments: The + (macro-)name of the instance, a key-value pair assigning + declarations in the corresponding \stexcode"mathstructure" + to symbols currently in scope, the name of the \stexcode"mathstructure" + to instantiate, and lastly a notation for the instance itself. + + It then generates a semantic macro that takes as argument + the name of a declaration in the instantiated \stexcode"mathstructure" + and resolves it to the corresponding instance of that particular declaration. + \end{function} + + \begin{mmtbox} + \stexcode"\instantiate" and \stexcode"mathstructure" make use of the + \emph{Theories-as-Types} paradigm (see \cite{MueRabKoh:tat18}): + + \stexcode"mathstructure{<name>}" simply creates a nested theory with name + |<name>-structure|. The \emph{constant} |<name>| is defined as + |Mod(<name>-structure)| -- a \emph{dependent record type with manifest fields}, + the fields of which are generated from (and correspond to) the constants in + |<name>-structure|. + + \stexcode"\instantiate" generates a constant whose definiens is a record term of + type |Mod(<name>-structure)|, with the fields assigned based on the respective + key-value-list. + \end{mmtbox} + + Notably, \stexcode"\instantiate" throws an error if not \emph{every} + declaration in the instantiated \stexcode"mathstructure" is being assigned. + + You might consequently ask what the usefulness of \stexcode"mathstructure" + even is. + + \begin{function}{\varinstantiate} + The answer is that we can also instantiate a + \stexcode"mathstructure" with a \emph{variable}. + The syntax of \stexcode"\varianstantiate" is equivalent + to that of \stexcode"\instantiate", but all of the key-value-pairs + are optional, and if not explicitly assigned (to a symbol \emph{or} + a variable declared with \stexcode"\vardef") inherit their notation + from the one in the \stexcode"mathstructure" environment. + \end{function} + + This allows us to do things like: + + \stexexample{% +\varinstantiate{varM}{monoid}{M} + +A \symname{monoid} is a structure +$\varM!:=\mathstruct{\varM{universe},\varM{op}!,\varM{unit}}$ +such that +$\varM{op}!:\funtype{\varM{universe},\varM{universe}}{\varM{universe}}$ ... +} + +and + +\stexexample{% + \varinstantiate{varMb}{monoid}{M_2}[universe = Int] + + Let $\varMb!:=\mathstruct{\varMb{universe},\varMb{op}!,\varMb{unit}}$ +be a \symname{monoid} on $\Int$ ... + } + + We will return to these two example later, when we also know + how to handle the \emph{axioms} of a monoid. +\end{smodule} +\end{sfragment} + +\begin{sfragment}{The \texttt{copymodule} Environment} + + \textcolor{red}{TODO: explain} + Given modules: -\stexexample{ - \begin{smodule}{magma} - \symdef{universe}{\comp{\mathcal U}} - \symdef{operation}[args=2,op=\circ]{#1 \comp\circ #2} - \end{smodule} - \begin{smodule}{monoid} - \importmodule{magma} - \symdef{unit}{\comp e} - \end{smodule} - \begin{smodule}{group} - \importmodule{monoid} - \symdef{inverse}[args=1]{{#1}^{\comp{-1}}} - \end{smodule} +\stexexample{% +\begin{smodule}{magma} + \symdef{universe}{\comp{\mathcal U}} + \symdef{operation}[args=2,op=\circ]{#1 \comp\circ #2} +\end{smodule} +\begin{smodule}{monoid} + \importmodule{magma} + \symdef{unit}{\comp e} +\end{smodule} +\begin{smodule}{group} + \importmodule{monoid} + \symdef{inverse}[args=1]{{#1}^{\comp{-1}}} +\end{smodule} } We can form a module for \emph{rings} by ``cloning'' @@ -20,48 +175,64 @@ an instance of |group| (for addition) and |monoid| (for multiplication), respectively, and ``glueing them together'' to ensure they share the same universe: -\stexexample{ - \begin{smodule}{ring} - \begin{copymodule}{group}{addition} - \renamedecl[name=universe]{universe}{runiverse} - \renamedecl[name=plus]{operation}{rplus} - \renamedecl[name=zero]{unit}{rzero} - \renamedecl[name=uminus]{inverse}{ruminus} - \end{copymodule} - \notation*{rplus}[plus,op=+,prec=60]{#1 \comp+ #2} - %\setnotation{rplus}{plus} - \notation*{rzero}[zero]{\comp0} - %\setnotation{rzero}{zero} - \notation*{ruminus}[uminus,op=-]{\comp- #1} - %\setnotation{ruminus}{uminus} - \begin{copymodule}{monoid}{multiplication} - \assign{universe}{\runiverse} - \renamedecl[name=times]{operation}{rtimes} - \renamedecl[name=one]{unit}{rone} - \end{copymodule} - \notation*{rtimes}[cdot,op=\cdot,prec=50]{#1 \comp\cdot #2} - %\setnotation{rtimes}{cdot} - \notation*{rone}[one]{\comp1} - %\setnotation{rone}{one} - Test: $\rtimes a{\rplus c{\rtimes de}}$ - \end{smodule} +\stexexample{% +\begin{smodule}{ring} + \begin{copymodule}{group}{addition} + \renamedecl[name=universe]{universe}{runiverse} + \renamedecl[name=plus]{operation}{rplus} + \renamedecl[name=zero]{unit}{rzero} + \renamedecl[name=uminus]{inverse}{ruminus} + \end{copymodule} + \notation*{rplus}[plus,op=+,prec=60]{#1 \comp+ #2} +%\setnotation{rplus}{plus} + \notation*{rzero}[zero]{\comp0} +%\setnotation{rzero}{zero} + \notation*{ruminus}[uminus,op=-]{\comp- #1} +%\setnotation{ruminus}{uminus} + \begin{copymodule}{monoid}{multiplication} + \assign{universe}{\runiverse} + \renamedecl[name=times]{operation}{rtimes} + \renamedecl[name=one]{unit}{rone} + \end{copymodule} + \notation*{rtimes}[cdot,op=\cdot,prec=50]{#1 \comp\cdot #2} +%\setnotation{rtimes}{cdot} + \notation*{rone}[one]{\comp1} +%\setnotation{rone}{one} + Test: $\rtimes a{\rplus c{\rtimes de}}$ +\end{smodule} } \textcolor{red}{TODO: explain donotclone} + +\end{sfragment} + +\begin{sfragment}{The \texttt{interpretmodule} Environment} + + \textcolor{red}{TODO: explain} + +\stexexample{% +\begin{smodule}{int} + \symdef{Integers}{\comp{\mathbb Z}} + \symdef{plus}[args=2,op=+]{#1 \comp+ #2} + \symdef{zero}{\comp0} + \symdef{uminus}[args=1,op=-]{\comp-#1} + + \begin{interpretmodule}{group}{intisgroup} + \assign{universe}{\Integers} + \assign{operation}{\plus!} + \assign{unit}{\zero} + \assign{inverse}{\uminus!} + \end{interpretmodule} +\end{smodule} +} + +\end{sfragment} +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: -\stexexample{ - \begin{smodule}{int} - \symdef{Integers}{\comp{\mathbb Z}} - \symdef{plus}[args=2,op=+]{#1 \comp+ #2} - \symdef{zero}{\comp0} - \symdef{uminus}[args=1,op=-]{\comp-#1} - - \begin{interpretmodule}{group}{intisgroup} - \assign{universe}{\Integers} - \assign{operation}{\plus!} - \assign{unit}{\zero} - \assign{inverse}{\uminus!} - \end{interpretmodule} - \end{smodule} -}
\ No newline at end of file +% LocalWords: circ,e intmonoid MueRabKoh:tat18 varinstantiate 2,op runiverse rplus prec +% LocalWords: rzero uminus ruminus plus,op uminus,op rtimes cdot,op cdot,prec 1,op +% LocalWords: donotclone intisgroup diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-hwexam.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-hwexam.tex index 5f1758b0150..5aced96e664 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-hwexam.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-hwexam.tex @@ -1 +1,84 @@ -\textcolor{red}{TODO: hwexam documentation}
\ No newline at end of file + +The \pkg{hwexam} package and class supplies an infrastructure that allows to format +nice-looking assignment sheets by simply including problems from problem files marked up +with the \pkg{roblem} package. It is designed to be compatible with |problems.sty|, and +inherits some of the functionality. + +\begin{variable}{solutions,notes,hints,gnotes,pts,min} + The \pkg{wexam} package and class take the options |solutions|, |notes|, |hints|, + |gnotes|, |pts|, |min|, and |boxed| that are just passed on to the \pkg{problems} + package (cf. its documentation for a description of the intended behavior). +\end{variable} + +This package supplies the \DescribeEnv{assignment}|assignment| environment that groups +problems into assignment sheets. It takes an optional KeyVal argument with the keys +\DescribeMacro{number}|number| (for the assignment number; if none is given, 1 is +assumed as the default or --- in multi-assignment documents --- the ordinal of the +|assignment| environment), \DescribeMacro{title}|title| (for the assignment title; this +is referenced in the title of the assignment sheet), \DescribeMacro{type}|type| (for the +assignment type; e.g. ``quiz'', or ``homework''), \DescribeMacro{given}|given| (for the +date the assignment was given), and \DescribeMacro{due}|due| (for the date the +assignment is due). + +Furthermore, the \pkg{hwexam} package takes the option +\DescribeMacro{multiple}|multiple| that allows to combine multiple assignment sheets +into a compound document (the assignment sheets are treated as section, there is a table +of contents, etc.). + +Finally, there is the option \DescribeMacro{test}|test| that modifies the behavior to +facilitate formatting tests. Only in |test| mode, the macros |\testspace|, +|\testnewpage|, and |\testemptypage| have an effect: they generate space for the +students to solve the given problems. Thus they can be left in the {\LaTeX} source. + +\DescribeMacro{\testspace}|\testspace| takes an argument that expands to a dimension, +and leaves vertical space accordingly. \DescribeMacro{\testnewpage}|\testnewpage| makes +a new page in |test| mode, and \DescribeMacro{\testemptypage}|\testemptypage| generates +an empty page with the cautionary message that this page was intentionally left empty. + +Finally, the \DescribeEnv{testheading}|\testheading| takes an optional keyword argument +where the keys \DescribeMacro{duration}|duration| specifies a string that specifies the +duration of the test, \DescribeMacro{min}|min| specifies the equivalent in number of +minutes, and \DescribeMacro{reqpts}|reqpts| the points that are required for a perfect +grade. + +\begin{latexcode} +\title{320101 General Computer Science (Fall 2010)} +\begin{testheading}[duration=one hour,min=60,reqpts=27] + Good luck to all students! +\end{testheading} +\end{latexcode} + +Will result in +\begin{center} + \begin{minipage}{.9\textwidth} +\makeatletter +\@problem{1.1}{4}{10} +\@problem{2.1}{4}{8} +\@problem{2.2}{6}{10} +\@problem{2.3}{6}{10} +\@problem{3.1}{4}{8} +\@problem{3.2}{4}{8} +\@problem{3.3}{2}{4} +\makeatother +\title{320101 General Computer Science (Fall 2010)} +\begin{testheading}[duration=one hour,min=60,reqpts=27] + good luck +\end{testheading} +\end{minipage} +\end{center} +\ednote{MK: The first three ``problems'' come from the stex examples above, how do we get rid + of this?} + +\begin{function}{\inputassignment} + The |\inputassignment| macro can be used to input an assignment from another file. It + takes an optional KeyVal argument and a second argument which is a path to the file + containing the problem (the macro assumes that there is only one |assignment| + environment in the included file). The keys |number|, |title|, |type|, |given|, and + |due| are just as for the |assignment| environment and (if given) overwrite the ones + specified in the |assignment| environment in the included file. +\end{function} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-inheritance.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-inheritance.tex index 41631f94d27..be7c4e68ec0 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-inheritance.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-inheritance.tex @@ -1 +1,131 @@ -\textcolor{red}{TODO: inheritance documentation}
\ No newline at end of file +\begin{sfragment}{Simple Inheritance and Namespaces} + + \begin{function}{\importmodule,\usemodule} + \stexcode"\importmodule[Some/Archive]{path?ModuleName}" is only allowed within an + \stexcode"smodule"-environment and makes the symbols declared in |ModuleName| + available therein. Additionally the symbols of |ModuleName| will be exported if the + current module is imported somewhere else via \stexcode"\importmodule". + + \stexcode"\usemodule" behaves the same way, but without exporting the content of the + used module. + \end{function} + + It is worth going into some detail how exactly \stexcode"\importmodule" + and \stexcode"\usemodule" resolve their arguments to find + the desired module -- which is closely related to the + \emph{namespace} generated for a module, that is used to generate + its URI. + + \begin{dangerbox} + 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 \stexcode"\begin{smodule}{Foo}" + \iffalse\end{smodule}\fi 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. + + 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. +\end{dangerbox} + +\begin{dangerbox} + Conversely, here is how namespaces/URIs and file paths are computed + in import statements, examplary \stexcode"\importmodule": + + \begin{itemize} + \item \stexcode"\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 \stexcode"\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, \stexcode"\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, \stexcode"\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 strongly discouraged, unless the module is delared in + the current file directly. + \end{itemize} + + \end{dangerbox} + + \begin{function}{\STEXexport} + \stexcode"\importmodule" and \stexcode"\usemodule" import all symbols, notations, + semantic macros and (recursively) \stexcode"\importmodule"s. If you want to + additionally export e.g. convenience macros and other (\sTeX) code from a module, you + can use the command \stexcode"\STEXexport{<code>}" in your module. Then |<code>| is + executed (both immediately and) every time the current module is opened via + \stexcode"\importmodule" or \stexcode"\usemodule". + \end{function} + + \begin{dangerbox} + For persistency reasons, everything in an \stexcode"\STEXexport" + is digested by \TeX in the \LaTeX3-category code scheme. + This means that the characters \stexcode"_" and \stexcode":" + are considered \emph{letters} and valid parts of + control sequence names, and space characters are ignored entirely. + For spaces, use the character \stexcode"~" instead, and + keep in mind, that if you want to use subscripts, you + should use \stexcode"\c_math_subscript_token" instead + of \stexcode"_"! + + + Also note, that \stexcode"\newcommand" defines macros \emph{globally} + and throws an error if the macro already exists, + potentially leading to low-level \LaTeX\xspace errors if + we put a \stexcode"\newcommand" in an \stexcode"\STEXexport" + and the |<code>| is executed more than once in a document + -- which can happen easily. + + A safer alternative is to use macro definition principles, + that are safe to use even if the macro being defined already + exists, and ideally are local to the current \TeX\xspace group, + such as \stexcode"\def" or \stexcode"\let". + \end{dangerbox} + +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-mathhub.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-mathhub.tex index 4b05134e70d..fb872acfbad 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-mathhub.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-mathhub.tex @@ -1,5 +1,6 @@ \begin{sfragment}{The Local MathHub-Directory} - |\usemodule|, |\importmodule|, |\inputref| etc. allow for + \stexcode"\usemodule", \stexcode"\importmodule", + \stexcode"\inputref" etc. allow for including content modularly without having to specify absolute paths, which would differ between users and machines. Instead, \sTeX uses \emph{archives} that determine the global @@ -7,30 +8,30 @@ for \sTeX to find content referenced via such URIs. All \sTeX archives need to exist in the local |MathHub|-directory. - \sTeX knows where this folder is via one of three means: + \sTeX knows where this folder is via one of four means: \begin{enumerate} - \item If the \sTeX package is loaded with the option - |mathhub=/path/to/mathhub|, then \sTeX will consider - |/path/to/mathhub| as the local |MathHub|-directory. - \item If the |mathhub| package option is \emph{not} - set, but the macro |\mathhub| exists when the - \sTeX-package is loaded, then this macro is - assumed to point to the local |MathHub|-directory; i.e. - |\def\mathhub{/path/to/mathhub}\usepackage{stex}| - will set the |MathHub|-directory as |path/to/mathhub|. - \item Otherwise, \sTeX will attempt to retrieve the - system variable |MATHHUB|, assuming it will - point to the local |MathHub|-directory. Since this - variant needs setting up only \emph{once} and is - machine-specific (rather than defined in tex code), - it is compatible with collaborating and sharing tex - content, and hence recommended. + \item If the \sTeX package is loaded with the option |mathhub=/path/to/mathhub|, then + \sTeX will consider |/path/to/mathhub| as the local |MathHub|-directory. + \item If the |mathhub| package option is \emph{not} set, but the macro |\mathhub| + exists when the \sTeX-package is loaded, then this macro is assumed to point to the + local |MathHub|-directory; i.e. + \stexcode"\def\mathhub{/path/to/mathhub}\usepackage{stex}" will set the + |MathHub|-directory as |path/to/mathhub|. + \item Otherwise, \sTeX will attempt to retrieve the system variable |MATHHUB|, + assuming it will point to the local |MathHub|-directory. Since this variant needs + setting up only \emph{once} and is machine-specific (rather than defined in tex + code), it is compatible with collaborating and sharing tex content, and hence + recommended. + \item Finally, if all else fails, \sTeX will look for a file + |~/.stex/mathhub.path|. If this file exists, \sTeX will assume that it contains the + path to the local |MathHub|-directory. This method is recommended on systems where + it is difficult to set environment variables. \end{enumerate} \end{sfragment} \begin{sfragment}{The Structure of \sTeX Archives} - An \sTeX archive |group/name| needs to be stored in the + An \sTeX archive |group/name| is stored in the directory |/path/to/mathhub/group/name|; e.g. assuming your local |MathHub|-directory is set as |/user/foo/MathHub|, then in order for the |smglom/calculus|-archive to be found by the @@ -43,19 +44,41 @@ |MANIFEST.MF|, the content of which we will consider shortly \end{itemize} An additional |lib|-directory is optional, and is where \sTeX will - look for files included via |\libinput|. + look for files included via \stexcode"\libinput". Additionally a \emph{group} of archives |group/name| may have an additional archive |group/meta-inf|. If this |meta-inf|-archive - has a |/lib|-subdirectory, it too will be searched by |\libinput| + has a |/lib|-subdirectory, it too will be searched by \stexcode"\libinput" from all tex files in any archive in the |group/*|-group. + + \paragraph{} We recommend the following additional directory structure in the + |source|-folder of an \sTeX archive: + \begin{itemize} + \item |/source/mod/| -- individual \sTeX modules, containing + symbol declarations, notations, and + \stexcode"\begin{sparagraph}[type=symdoc,for=...]" + environments for ``encyclopaedic'' symbol documentations + \iffalse\end{sparagraph}\fi + \item |/source/def/| -- definitions + \item |/source/ex/| -- examples + \item |/source/thm/| -- theorems, lemmata and proofs; preferably + proofs in separate files to allow for multiple proofs for the + same statement + \item |/source/snip/| -- individual text snippets such as remarks, + explanations etc. + \item |/source/frag/| -- individual document fragments, + ideally only \stexcode"\inputref"ing snippets, definitions, + examples etc. in some desirable order + \item |/source/tikz/| -- tikz images, as individual |.tex|-files + \item |/source/PIC/| -- image files. + \end{itemize} + \end{sfragment} \begin{sfragment}{MANIFEST.MF-Files} - The |MANIFEST.MF| in the |META-INF|-directory consists of - key-value-pairs, instructing \sTeX (and associated software) - of various properties of an archive. For example, - the |MANIFEST.MF| of the |smglom/calculus|-archive looks like this: + The |MANIFEST.MF| in the |META-INF|-directory consists of key-value-pairs, informing + \sTeX (and associated software) of various properties of an archive. For example, the + |MANIFEST.MF| of the |smglom/calculus|-archive looks like this: \begin{framed} \begin{verbatim} @@ -86,4 +109,95 @@ e.g. for |lmh install|. \end{itemize} -\end{sfragment}
\ No newline at end of file +\end{sfragment} + +\begin{sfragment}{Using Files in \sTeX Archives Directly} + Several macros provided by \sTeX allow for directly including + files in repositories. These are: + \begin{function}{\mhinput} + \stexcode"\mhinput[Some/Archive]{some/file}" directly + inputs the file |some/file| in the |source|-folder of + |Some/Archive|. + \end{function} + \begin{function}{\inputref} + \stexcode"\inputref[Some/Archive]{some/file}" behaves like \stexcode"\mhinput", but + wraps the input in a |\begingroup ... \endgroup|. When converting to |xhtml|, the + file is not input at all, and instead an |html|-annotation is inserted that + references the file, e.g. for lazy loading. + + In the majority of practical cases \stexcode"\inputref" is likely to be preferred + over \stexcode"\mhinput" because it leads to less duplication in the generated + |xhtml|. + \end{function} + \begin{function}{\ifinput} + Both \stexcode"\mhinput" and \stexcode"\inputref" + set \stexcode"\ifinput" to ``true'' during input. This allows + for selectively including e.g. bibliographies only if the + current file is not being currently included in a larger document. + \end{function} + \begin{function}{\addmhbibresource} + \stexcode"\addmhbibresource[Some/Archive]{some/file}" searches for a file like + \stexcode"\mhinput" does, but calls |\addbibresource| to the result and looks for + the file in the archive root directory directly, rather than the |source| + directory. Typical invocations are + \begin{itemize} + \item |\addmhbibresource{lib/refs.bib}|, which specifies a bibliography in the |lib| + folder in the local archive or + \item |\addmhbibresource[HW/meta-inf]{lib/refs.bib}| in another. + \end{itemize} + \end{function} + \begin{function}{\libinput} + \stexcode"\libinput{some/file}" + searches for a file |some/file| in + \begin{itemize} + \item the |lib|-directory of the current archive, and + \item the |lib|-directory of a |meta-inf|-archive in + (any of) the archive groups containing the current archive + \end{itemize} + and include all found files in reverse order; + e.g. \stexcode"\libinput{preamble}" in a |.tex|-file in + |smglom/calculus| will \emph{first} input |.../smglom/meta-inf/lib/preamble.tex| + and then |../smglom/calculus/lib/preamble.tex|. + + \stexcode|\libinput| will throw an error if \emph{no} candidate for |some/file| + is found. + \end{function} + \begin{function}{\libusepackage} + \stexcode"\libusepackage[package-options]{some/file}" searches for a file + |some/file.sty| in the same way that \stexcode"\libinput" does, but will + call\\ + |\usepackage[package-options]{path/to/some/file}| instead of |\input|. + + \stexcode|\libusepackage| throws an error if not \emph{exactly one} candidate for + |some/file| is found. + \end{function} + + \begin{remark} + A good practice is to have individual \sTeX fragments + follow basically this document frame: + \begin{latexcode}[gobble=12] + \documentclass{stex} + \libinput{preamble} + \begin{document} + ... + \ifinputref \else \libinput{postamble} \fi + \end{document} + \end{latexcode} + Then the |preamble.tex| files can take care of loading the generally required + packages, setting presentation customizations etc. (per archive or archive group + or both), and |postamble.tex| can e.g. print the bibliography, index etc. + + \stexcode|\libusepackage| is particularly useful in |preamble.tex| when we want to + use custom packages that are not part of {\TeX}Live. In this case we commit the + respective packages in one of the |lib| folders and use \stexcode|\libusepackage| + to load them. + \end{remark} +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +%%% LocalWords: mathhub symdoc,for lmh subdirs arithmetics,smglom sets,smglom mv,smglom +%%% LocalWords: linear-algebra,smglom diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex index 1585ba504c8..4feb646eb9f 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex @@ -1 +1,30 @@ -\textcolor{red}{TODO: metatheory documentation}
\ No newline at end of file +The \pkg{stex-metatheory} package contains \sTeX symbols so ubiquitous, that it is +virtually impossible to describe any flexiformal content without them, or that are +required to annotate even the most primitive symbols with meaningful +(foundation-independent) ``type''-annotations, or required for basic structuring +principles (theorems, definitions). As such, it serves as the default meta theory for any +\sTeX module. + +We can also see the \pkg{stex-metatheory} as a foundation of mathematics in the sense of +\cite{rabe:future:15}, albeit an informal one (the ones discussed there are all formal +foundations). The state of the \pkg{stex-metatheory} is necessarily incomplete, and will +stay so for a long while: It arises as a collection of empirically useful symbols that are +collected as more and more mathematics are encoded in \sTeX and are classified as +foundational. + +Formal foundations should ideally instantiate these symbols with their formal counterparts, +e.g. |isa| corresponds to a typing operation in typed setting, or the $\in$-operator in +set-theoretic contexts; |bind| corresponds to a universal quantifier in ($n$th-order) +logic, or a $\Pi$ in dependent type theories. + +We make this theory part of the \sTeX collection due to the obiquity +of the symbols involved. Note however, that the metatheory is +for all practical purposes a ``normal'' \sTeX module, and the +symbols contained ``normal'' \sTeX symbols. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: stex-metatheory th-order diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-modules.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-modules.tex index c067f28a1c3..424c2200e85 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-modules.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-modules.tex @@ -1 +1,73 @@ -\textcolor{red}{TODO: modules documentation}
\ No newline at end of file +\begin{sfragment}{The \texttt{smodule}-Environment} + \begin{environment}{smodule} + A new module is declared using the basic syntax + \begin{center} + \stexcode"\begin{smodule}[options]{ModuleName}...\end{smodule}". + \end{center} + A module is required to declare any new formal content such as symbols or + notations (but not variables, which may be introduced anywhere). + + The |smodule|-environment takes several keyword arguments, all of which are + optional: + + \begin{itemize} + \item[|title|] (\meta{token list}) to display in customizations. + \item[|type|] (\meta{string}$\ast$) for use in customizations. + \item[|deprecate|] (\meta{module}) if set, will throw a warning + when loaded, urging to use \meta{module} instead. + \item[|id|] (\meta{string}) for cross-referencing. + \item[|ns|] (\meta{URI}) the namespace to use. \emph{Should not be used, + unless you know precisely what you're doing}. If not explicitly set, is + computed using \cs{stex_modules_current_namespace:}. + \item[|lang|] (\meta{language}) if not set, computed from the current file name (e.g. |foo.en.tex|). + \item[|sig|] (\meta{language}) if the current file is a translation of a file with the same base name + but a different language suffix, setting |sig=<lang>| will preload the module + from that language file. This helps ensuring that the (formal) content of both modules + is (almost) identical across languages and avoids duplication. + \item[|creators|] (\meta{string}$\ast$) names of the creators. + \item[|contributors|] (\meta{string}$\ast$) names of contributors. + \item[|srccite|] (\meta{string}) a source citation for the content of this module. + \end{itemize} + \end{environment} + + \begin{mmtbox} + An \sTeX module corresponds to an \mmt/\omdoc \emph{theory}. + As such it gets assigned a module URI (\emph{universal resource identifier}) + of the form |<namespace>?<module-name>|. + \end{mmtbox} + + By default, opening a module will produce no output whatsoever, + e.g.: + \stexexample{% +\begin{smodule}[title={This is Some Module}]{SomeModule} + Hello World +\end{smodule} + } + + \begin{function}{\stexpatchmodule} + We can customize this behavior either for all modules or + only for modules with a specific |type| using the command + \stexcode"\stexpatchmodule[optional-type]{begin-code}{end-code}". + Some optional parameters are then available in |\smodule*|-macros, + specifically |\smoduletitle|, |\smoduletype| and |\smoduleid|. + \end{function} + For example: + + \stexexample{% +\stexpatchmodule[display] + {\textbf{Module (\smoduletitle)}\par} + {\par\noindent\textbf{End of Module (\smoduletitle)}} + +\begin{smodule}[type=display,title={Some New Module}]{SomeModule2} + Hello World +\end{smodule} + } +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: srccite mmtbox stexexample stexpatchmodule smoduletitle smoduleid +% LocalWords: display,title diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-problem.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-problem.tex index 1ce5aaa3a23..a90c36412d0 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-problem.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-problem.tex @@ -1 +1,151 @@ -\textcolor{red}{TODO: problem documentation}
\ No newline at end of file +The \pkg{problem} package supplies an infrastructure that allows specify problem. Problems +are text fragments that come with auxiliary functions: hints, notes, and +solutions\footnote{for the moment multiple choice problems are not supported, but may + well be in a future version}. Furthermore, we can specify how long the solution to a +given problem is estimated to take and how many points will be awarded for a perfect +solution. + +Finally, the \pkg{problem} package facilitates the management of problems in small files, +so that problems can be re-used in multiple environment. + +\begin{function}{solutions,notes,hints,gnotes,pts,min,boxed,test} + The \pkg{problem} package takes the options |solutions| (should solutions be output?), + |notes| (should the problem notes be presented?), |hints| (do we give the hints?), + |gnotes| (do we show grading notes?), |pts| (do we display the points awarded for + solving the problem?), |min| (do we display the estimated minutes for problem + soling). If theses are specified, then the corresponding auxiliary parts of the problems + are output, otherwise, they remain invisible. + + The |boxed| option specifies that problems should be formatted in framed boxes so that + they are more visible in the text. Finally, the |test| option signifies that we are in a + test situation, so this option does not show the solutions (of course), but leaves space + for the students to solve them. +\end{function} + +\begin{environment}{problem} + The main environment provided by the \pkg{problem}package is (surprise surprise) the + |problem| environment. It is used to mark up problems and exercises. The environment + takes an optional KeyVal argument with the keys |id| as an identifier that can be + reference later, |pts| for the points to be gained from this exercise in homework or + quiz situations, |min| for the estimated minutes needed to solve the problem, and + finally |title| for an informative title of the problem. +\end{environment} + +\stexexample{% +\documentclass{article} +\usepackage[solutions,hints,pts,min]{problem} +\begin{document} + \begin{sproblem}[id=elefants,pts=10,min=2,title=Fitting Elefants] + How many Elefants can you fit into a Volkswagen beetle? + \begin{hint} + Think positively, this is simple! + \end{hint} + \begin{exnote} + Justify your answer + \end{exnote} +\begin{solution}[for=elefants,height=3cm] + Four, two in the front seats, and two in the back. + \begin{gnote} + if they do not give the justification deduct 5 pts + \end{gnote} +\end{solution} +\end{sproblem} +\end{document} +} + +\begin{environment}{solution} + The |solution| environment can be to specify a solution to a problem. If the package + option |solutions| is set or |\solutionstrue| is set in the text, then the solution will + be presented in the output. The |solution| environment takes an optional KeyVal argument + with the keys |id| for an identifier that can be reference |for| to specify which + problem this is a solution for, and |height| that allows to specify the amount of space + to be left in test situations (i.e. if the |test| option is set in the |\usepackage| + statement). +\end{environment} + +\begin{environment}{hint,exnote,gnote} + The |hint| and |exnote| environments can be used in a |problem| environment to give + hints and to make notes that elaborate certain aspects of the problem. The |gnote| + (grading notes) environment can be used to document situtations that may arise in + grading. +\end{environment} + +\begin{function}{\startsolutions,\stopsolutions} + Sometimes we would like to locally override the |solutions| option we have given to the + package. To turn on solutions we use the |\startsolutions|, to turn them off, + |\stopsolutions|. These two can be used at any point in the documents. +\end{function} + +\begin{function}{\ifsolutions} + Also, sometimes, we want content (e.g. in an exam with master solutions) conditional on + whether solutions are shown. This can be done with the |\ifsolutions| conditional. +\end{function} + +\begin{environment}{mcb} + Multiple choice blocks can be formatted using the |mcb| environment, in which single + choices are marked up with |\mcc| macro. +\end{environment} + +\begin{function}{\mcc} + |\mcc[|\meta{keyvals}|]{|\meta{text}|}| takes an optional key/value argument + \meta{keyvals} for choice metadata and a required argument \meta{text} for the proposed + answer text. The following keys are supported + \begin{itemize} + \item |T| for true answers, |F| for false ones, + \item |Ttext| the verdict for true answers, |Ftext| for false ones, and + \item |feedback| for a short feedback text given to the student. + \end{itemize} +\end{function} + +If we start the solutions, then we get + +\stexexample{% +\startsolutions +\begin{sproblem}[title=Functions,name=functions1] + What is the keyword to introduce a function definition in python? + \begin{mcb} + \mcc[T]{def} + \mcc[F,feedback=that is for C and C++]{function} + \mcc[F,feedback=that is for Standard ML]{fun} + \mcc[F,Ftext=Nooooooooo,feedback=that is for Java]{public static void} + \end{mcb} +\end{sproblem} +} +without solutions (that is what the students see during the exam/quiz)\ednote{MK: that did +not work!} +\stexexample{% +\stopsolutions +\begin{sproblem}[title=Functions,name=functions1] + What is the keyword to introduce a function definition in python? + \begin{mcb} + \mcc[T]{def} + \mcc[F,feedback=that is for C and C++]{function} + \mcc[F,feedback=that is for Standard ML]{fun} + \mcc[F,Ftext=Nooooooooo,feedback=that is for Java]{public static void} + \end{mcb} +\end{sproblem} +} + +\begin{function}{\includeproblem} + The |\includeproblem| macro can be used to include a problem from another file. It takes + an optional KeyVal argument and a second argument which is a path to the file containing + the problem (the macro assumes that there is only one problem in the include file). The + keys |title|, |min|, and |pts| specify the problem title, the estimated minutes for + solving the problem and the points to be gained, and their values (if given) overwrite + the ones specified in the |problem| environment in the included file. +\end{function} + +The sum of the points and estimated minutes (that we specified in the |pts| and |min| keys +to the |problem| environment or the |\includeproblem| macro) to the log file and the +screen after each run. This is useful in preparing exams, where we want to make sure that +the students can indeed solve the problems in an allotted time period. + +The |\min| and |\pts| macros allow to specify (i.e. to print to the margin) the +distribution of time and reward to parts of a problem, if the |pts| and |pts| options are +set. This allows to give students hints about the estimated time and the points to be +awarded. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-proofs.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-proofs.tex index 0523c65948d..d06db1282f5 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-proofs.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-proofs.tex @@ -1 +1,214 @@ -\textcolor{red}{TODO: sproofs documentation}
\ No newline at end of file +The \pkg{stex-proof} package supplies macros and environment that allow to annotate the +structure of mathematical proofs in \sTeX document. This structure can be used by MKM +systems for added-value services, either directly from the \sTeX sources, or after +translation. + +We will go over the general intuition by way of a running example: + +\begin{latexcode} +\begin{sproof}[id=simple-proof] + {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} + \begin{spfcases}{For the induction we have to consider three cases:} + \begin{spfcase}{$n=1$} + \begin{spfstep}[type=inline] then we compute $1=1^2$\end{spfstep} + \end{spfcase} + \begin{spfcase}{$n=2$} + \begin{spfcomment}[type=inline] + This case is not really necessary, but we do it for the + fun of it (and to get more intuition). + \end{spfcomment} + \begin{spfstep}[type=inline] We compute $1+3=2^{2}=4$.\end{spfstep} + \end{spfcase} + \begin{spfcase}{$n>1$} + \begin{spfstep}[type=assumption,id=ind-hyp] + Now, we assume that the assertion is true for a certain $k\geq 1$, + i.e. $\sum_{i=1}^k{(2i-1)}=k^{2}$. + \end{spfstep} + \begin{spfcomment} + We have to show that we can derive the assertion for $n=k+1$ from + this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. + \end{spfcomment} + \begin{spfstep} + We obtain $\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1$ + \spfjust[method=arith:split-sum]{by splitting the sum}. + \end{spfstep} + \begin{spfstep} + Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$ + \spfjust[method=fertilize]{by inductive hypothesis}. + \end{spfstep} + \begin{spfstep}[type=conclusion] + We can \spfjust[method=simplify]{simplify} the right-hand side to + ${k+1}^2$, which proves the assertion. + \end{spfstep} + \end{spfcase} + \begin{spfstep}[type=conclusion] + We have considered all the cases, so we have proven the assertion. + \end{spfstep} + \end{spfcases} +\end{sproof} +\end{latexcode} + +This yields the following result: + +\begin{mdframed} + \begin{sproof}[id=simple-proof] + {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} + \begin{spfcases}{For the induction we have to consider the following cases:} + \begin{spfcase}{$n=1$} + \begin{spfstep}[type=inline] then we compute $1=1^2$\end{spfstep} + \end{spfcase} + \begin{spfcase}{$n=2$} + \begin{spfcomment}[type=inline] + This case is not really necessary, but we do it for the fun + of it (and to get more intuition). + \end{spfcomment} + \begin{spfstep}[type=inline] + We compute $1+3=2^{2}=4$ + \end{spfstep} + \end{spfcase} + \begin{spfcase}{$n>1$} + \begin{spfstep}[type=hypothesis,id=ind-hyp] + Now, we assume that the assertion is true for a certain $k\geq 1$, i.e. + $\sum_{i=1}^k{(2i-1)}=k^{2}$. + \end{spfstep} + \begin{spfcomment} + We have to show that we can derive the assertion for $n=k+1$ from this + assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. + \end{spfcomment} + \begin{spfstep}[id=splitit] + We obtain $\sum_{i=1}^{k+1}{(2i-1)}=\sum_{i=1}^k{(2i-1)}+2(k+1)-1$ + \spfjust[method=arith:split-sum]{by splitting the sum}. + \end{spfstep} + \begin{spfstep}[id=byindhyp] + Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$ + \spfjust[method=fertilize]{by \premise[ind-hyp]{inductive hypothesis}}. + \end{spfstep} + \begin{spfstep}[type=conclusion] + We can \spfjust[method=simplify-eq]{simplify the \justarg[rhs]{right-hand side}} to + $(k+1)^2$, which proves the assertion. + \end{spfstep} + \end{spfcase} + \begin{spfstep}[type=conclusion] + We have considered all the cases, so we have proven the assertion. + \end{spfstep} + \end{spfcases} +\end{sproof} +\end{mdframed} + +\begin{environment}{sproof} + The |sproof| environment is the main container for proofs. It takes an optional |KeyVal| + argument that allows to specify the |id| (identifier) and |for| (for which assertion is + this a proof) keys. The regular argument of the |proof| environment contains an + introductory comment, that may be used to announce the proof style. The |proof| + environment contains a sequence of |spfstep|, |spfcomment|, and |spfcases| environments + that are used to markup the proof steps. +\end{environment} + +\begin{function}{\spfidea} + The |\spfidea| macro allows to give a one-paragraph description of the proof idea. +\end{function} + +\begin{function}{\spfsketch} + For one-line proof sketches, we use the |\spfsketch| macro, which takes the same + optional argument as |sproof| and another one: a natural language text that sketches + the proof. +\end{function} + +\begin{environment}{spfstep} + Regular proof steps are marked up with the |step| environment, which takes an optional + |KeyVal| argument for annotations. A proof step usually contains a local assertion + (the text of the step) together with some kind of evidence that this can be derived + from already established assertions. +\end{environment} + +\begin{function}{\spfjust} + This evidence is marked up with the |\spfjust| macro in the \pkg{stex-proofs} + package. This environment totally invisible to the formatted result; it wraps the text + in the proof step that corresponds to the evidence. The environment takes an optional + |KeyVal| argument, which can have the |method| key, whose value is the name of a proof + method (this will only need to mean something to the application that consumes the + semantic annotations). Furthermore, the justification can contain ``premises'' + (specifications to assertions that were used justify the step) and ``arguments'' + (other information taken into account by the proof method). +\end{function} + +\begin{function}{\premise} + The |\premise| macro allows to mark up part of the text as reference to an assertion + that is used in the argumentation. In the running example we have used the |\premise| + macro to identify the inductive hypothesis. +\end{function} + +\begin{function}{\justarg} + The |\justarg| macro is very similar to |\premise| with the difference that it is used + to mark up arguments to the proof method. Therefore the content of the first argument + is interpreted as a mathematical object rather than as an identifier as in the case of + |\premise|. In our example, we specified that the simplification should take place on + the right hand side of the equation. Other examples include proof methods that + instantiate. Here we would indicate the substituted object in a |\justarg| macro. +\end{function} + +Note that both |\premise| and |\justarg| can be used with an empty second argument to +mark up premises and arguments that are not explicitly mentioned in the text. + +\begin{environment}{subproof} + The |spfcases| environment is used to mark up a subproof. This environment takes an + optional |KeyVal| argument for semantic annotations and a second argument that allows + to specify an introductory comment (just like in the |proof| environment). The + |method| key can be used to give the name of the proof method + executed to make this subproof. +\end{environment} + +\begin{environment}{spfcases} + The |spfcases| environment is used to mark up a proof by cases. Technically it is a + variant of the |subproof| where the |method| is |by-cases|. Its contents are |spfcase| + environments that mark up the cases one by one. +\end{environment} + +\begin{environment}{spfcase} + The content of a |spfcases| environment are a sequence of case proofs marked up in the + |spfcase| environment, which takes an optional |KeyVal| argument for semantic + annotations. The second argument is used to specify the the description of the case + under consideration. The content of a |spfcase| environment is the same as that of a + |sproof|, i.e. |spfstep|s, |spfcomment|s, and |spfcases| environments. +\end{environment} + +\begin{function}{\spfcasesketch} + |\spfcasesketch| is a variant of the |spfcase| environment that takes the same + arguments, but instead of the |spfstep|s in the body uses a third argument for a proof + sketch. +\end{function} + +\begin{environment}{spfcomment} + The |spfcomment| environment is much like a |step|, only that it does not have an + object-level assertion of its own. Rather than asserting some fact that is relevant + for the proof, it is used to explain where the proof is going, what we are attempting + to to, or what we have achieved so far. As such, it cannot be the target of a + |\premise|. +\end{environment} + +\begin{function}{\sproofend} + Traditionally, the end of a mathematical proof is marked with a little box at the end of + the last line of the proof (if there is space and on the end of the next line if there + isn't), like so:\sproofend + + The \pkg{stex-proofs} package provides the |\sproofend| macro for this. +\end{function} + +\begin{variable}{\sProofEndSymbol} + If a different symbol for the proof end is to be used (e.g. {\sl{q.e.d}}), then this can + be obtained by specifying it using the |\sProofEndSymbol| configuration macro (e.g. by + specifying |\sProofEndSymbol{q.e.d}|). +\end{variable} + +Some of the proof structuring macros above will insert proof end symbols for sub-proofs, +in most cases, this is desirable to make the proof structure explicit, but sometimes this +wastes space (especially, if a proof ends in a case analysis which will supply its own +proof end marker). To suppress it locally, just set |proofend={}| in them or use use +|\sProofEndSymbol{}|. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: hypothesis,id geq splitit arith:split-sum byindhyp rhs proofend diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-references.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-references.tex index bf8a8ed66c0..11de003e9be 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-references.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-references.tex @@ -1 +1,8 @@ -\textcolor{red}{TODO: references documentation}
\ No newline at end of file +\begin{sfragment}[id=sec.references]{Referencing Symbols and Statements} +\textcolor{red}{TODO: references documentation} +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-slides.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-slides.tex index 1f9d0c989d6..a900c1fcbb8 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-slides.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-slides.tex @@ -1 +1,212 @@ -\textcolor{red}{TODO: notesslides documentation}
\ No newline at end of file +The \pkg{notesslides} document class is derived from |beamer.cls|~\cite{beamerclass:on}, +it adds a ``notes version'' for course notes that is more suited to printing than the one +supplied by |beamer.cls|. + +The \pkg{notesslides} class takes the notion of a slide frame from Till Tantau's excellent +\pkg{beamer} class and adapts its notion of frames for use in the \sTeX and \omdoc. To +support semantic course notes, it extends the notion of mixing frames and explanatory +text, but rather than treating the frames as images (or integrating their contents into +the flowing text), the \pkg{notesslides} package displays the slides as such in the course +notes to give students a visual anchor into the slide presentation in the course (and to +distinguish the different writing styles in slides and course notes). + +In practice we want to generate two documents from the same source: the slides for +presentation in the lecture and the course notes as a narrative document for home +study. To achieve this, the \pkg{notesslides} class has two modes: \emph{slides mode} and +\emph{notes mode} which are determined by the package option. + + +\begin{variable}{slides,notes,sectocframes,frameimages,fiboxed} + The \pkg{notesslides} class takes a variety of class options: + \begin{itemize} + \item The options |slides| and |notes| switch between slides mode and notes mode (see + Section~\ref{sec:user:notesslides}). + \item If the option |sectocframes| is given, then for the |sfragment|s, special frames + with the |sfragment| title (and number) are generated. + \item If the option |frameimages| is set, then slide mode also shows the + |\frameimage|-generated frames (see section~\ref{sec:user:frameimage}). If also the + |fiboxed| option is given, the slides are surrounded by a box. + \end{itemize} +\end{variable} + +\begin{environment}{frame,note} + Slides are represented with the |frame| environment just like in the \pkg{beamer} class, + see~\cite{Tantau:ugbc} for details. The \pkg{notesslides} class adds the |note| + environment for encapsulating the course note fragments.\footnote{MK: it would be very + nice, if we did not need this environment, and this should be possible in principle, + but not without intensive LaTeX trickery. Hints to the author are welcome.} +\end{environment} + +\begin{dangerbox} + Note that it is essential to start and end the |notes| environment at the start of the + line -- in particular, there may not be leading blanks -- else {\LaTeX} becomes confused + and throws error messages that are difficult to decipher. +\end{dangerbox} + +By interleaving the |frame| and |note| environments, we can build course notes as shown +here: + +\begin{latexcode} +\ifnotes\maketitle\else +\frame[noframenumbering]\maketitle\fi + +\begin{note} + We start this course with ... +\end{note} + +\begin{frame} + \frametitle{The first slide} + ... +\end{frame} +\begin{note} + ... and more explanatory text +\end{note} + +\begin{frame} + \frametitle{The second slide} + ... +\end{frame} +... +\end{latexcode} + +\begin{function}{\ifnotes} + Note the use of the |\ifnotes| conditional, which allows different treatment between + |notes| and |slides| mode -- manually setting |\notestrue| or |\notesfalse| is strongly + discouraged however. +\end{function} + +\begin{dangerbox} + We need to give the title frame the |noframenumbering| option so that the frame + numbering is kept in sync between the slides and the course notes. +\end{dangerbox} + +\begin{dangerbox} + The \pkg{beamer} class recommends not to use the |allowframebreaks| option on frames + (even though it is very convenient). This holds even more in the |notesslides| case: At + least in conjunction with |\newpage|, frame numbering behaves funnily (we have tried to + fix this, but who knows). +\end{dangerbox} + +\begin{function}{\inputref*} + If we want to transclude a the contents of a file as a note, we can use a new variant + |\inputref*| of the |\inputref| macro: |\inputref*{foo}| is equivalent to + |\begin{note}\inputref{foo}\end{note}|. +\end{function} + +\begin{environment}{nparagraph, nparagraph, ndefinition, nexample, nsproof, nassertion} + There are some environments that tend to occur at the top-level of |note| + environments. We make convenience versions of these: e.g. the |nparagraph| environment + is just an |sparagraph| inside a |note| environment (but looks nicer in the source, + since it avoids one level of source indenting). Similarly, we have the |nfragment|, + |ndefinition|, |nexample|, |nsproof|, and |nassertion| environments. +\end{environment} + +\begin{function} {\setslidelogo} + The default logo provided by the \pkg{notesslides} package is the {\sTeX} logo it can be + customized using |\setslidelogo{|\meta{logo name}|}|. +\end{function} + +\begin{function}{\setsource} + The default footer line of the \pkg{notesslides} package mentions copyright and + licensing. In the \pkg{beamer} class, |\source| stores the author's name as the + copyright holder . By default it is \emph{Michael Kohlhase} in the \pkg{notesslides} + package since he is the main user and designer of this + package. |\setsource{|\meta{name}|}| can change the writer's name. +\end{function} + +\begin{function}{\setlicensing} + For licensing, we use the Creative Commons Attribuition-ShareAlike license by default to + strengthen the public domain. If package |hyperref| is loaded, then we can attach a + hyperlink to the license logo. |\setlicensing[|\meta{url}|]{|\meta{logo name}|}| is used + for customization, where \meta{url} is optional. +\end{function} + +Sometimes, we want to integrate slides as images after all -- e.g. because we already +have a PowerPoint presentation, to which we want to add \sTeX notes. + +\begin{function}{\frameimage,\mhframeimage} + In this case we can use |\frameimage[|\meta{opt}|]{|\meta{path}|}|, where \meta{opt} are + the options of |\includegraphics| from the \pkg{graphicx} package~\cite{CarRah:tpp99} + and \meta{path} is the file path (extension can be left off like in + |\includegraphics|). We have added the |label| key that allows to give a frame label + that can be referenced like a regular |beamer| frame. + +The |\mhframeimage| macro is a variant of |\frameimage| with repository support. Instead +of writing +\begin{latexcode} +\frameimage{\MathHub{fooMH/bar/source/baz/foobar}} +\end{latexcode} + we can simply write (assuming that |\MathHub| is defined as above) +\begin{latexcode} +\mhframeimage[fooMH/bar]{baz/foobar} +\end{latexcode} + Note that the |\mhframeimage| form is more semantic, which allows more advanced document +management features in \textsf{MathHub}. +\end{function} + +If |baz/foobar| is the ``current module'', i.e. if we are on the \textsf{MathHub} path +\ldots|MathHub/fooMH/bar|\ldots, then stating the repository in the first optional +argument is redundant, so we can just use +\begin{latexcode} +\mhframeimage{baz/foobar} +\end{latexcode} + +\begin{function}{\textwarning} + The |\textwarning| macro generates a warning sign: \textwarning +\end{function} + +In course notes, we sometimes want to point to an ``excursion'' -- material that is either +presupposed or tangential to the course at the moment -- e.g. in an appendix. The typical +setup is the following: + +\begin{latexcode} +\excursion{founif}{../ex/founif}{We will cover first-order unification in} +... +\begin{appendix}\printexcursions\end{appendix} +\end{latexcode} + +\begin{function}{\excursion} + The |\excursion{|\meta{ref}|}{|\meta{path}|}{|\meta{text}|}| is syntactic sugar for + +\begin{latexcode} +\begin{nparagraph}[title=Excursion] + \activateexcursion{founif}{../ex/founif} + We will cover first-order unification in \sref{founif}. +\end{nparagraph} +\end{latexcode} +\end{function} + +\begin{function}{\activateexcursion,\printexcursion,\excursionref} + Here |\activateexcursion{|\meta{path}|}| augments the |\printexcursions| macro by a call + |\inputref{|\meta{path}|}|. In this way, the |\printexcursions| macro (usually in the + appendix) will collect up all excursions that are specified in the main text. + + Sometimes, we want to reference -- in an excursion -- part of another. We can use + |\excursionref{|\meta{label}|}| for that. +\end{function} + +\begin{function}{\excursiongroup} + Finally, we usually want to put the excursions into an |sfragment| environment and add + an introduction, therefore we provide the a variant of the |\printexcursions| macro: + |\excursiongroup[id=|\meta{id}|,intro=|\meta{path}|]| is equivalent to +\begin{latexcode} +\begin{note} +\begin{sfragment}[id=<id>]{Excursions} + \inputref{<path>} + \printexcursions +\end{sfragment} +\end{note} +\end{latexcode} +\end{function} + +\begin{dangerbox} + When option |book| which uses |\pagestyle{headings}| is given and semantic macros are + given in the |sfragment| titles, then they sometimes are not defined by the time the + heading is formatted. Need to look into how the headings are made. This is a problem of + the underlying \pkg{document-structure} package. +\end{dangerbox} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex index aa9f5f76abf..6a2478fa7d1 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex @@ -1 +1,145 @@ -\textcolor{red}{TODO: statements documentation}
\ No newline at end of file +\begin{sfragment}{Definitions, Theorems, Examples, Paragraphs} +\begin{smodule}{Statements} + As mentioned earlier, we can semantically mark-up + \emph{statements} such as definitions, theorems, lemmata, examples, etc. + + The corresponding environments for that are: + \begin{itemize} + \item \stexcode"sdefinition" for definitions, + \item \stexcode"sassertion" for assertions, i.e. + propositions that are declared to be \emph{true}, + such as theorems, lemmata, axioms, + \item \stexcode"sexample" for examples and counterexamples, and + \item \stexcode"sparagraph" for ``other'' semantic paragraphs, + such as comments, remarks, conjectures, etc. + \end{itemize} + + The \emph{presentation} of these environments can be customized + to use e.g. predefined |theorem|-environments, see \sref{sec.customhighlight} + for details. + + All of these environments take optional arguments in the form of + |key=value|-pairs. Common to all of them are the keys |id=| (for cross-referencing, + see \sref{sec.references}), |type=| for customization (see \sref{sec.customhighlight}) + and additional information (e.g. definition principles, ``difficulty'' etc), as well + as |title=| (for giving the paragraph a title), and finally |for=|. + + The |for=| key expects a comma-separated list of existing + symbols, allowing for e.g. things like + \symdef{addition}[args=a,prec=100]{#1}{##1 \comp+ ##2} + \symdef{multiplication}[args=a,prec=50]{#1}{##1 \comp\cdot ##2} + \stexexample{% +\begin{sexample}[ + id=additionandmultiplication.ex, + for={addition,multiplication}, + type={trivial,boring}, + title={An Example} +] + $\addition{2,3}$ is $5$, $\multiplication{2,3}$ is $6$. +\end{sexample} + } + + \begin{function}{\definiendum,\definame,\Definame} + \stexcode"sdefinition" (and \stexcode"sparagraph" with + |type=symdoc|) introduce three new macros: + \stexcode"definiendum" behaves like \stexcode"symref" + (and \stexcode"definame"/\stexcode"Definame" + like \stexcode"symname"/\stexcode"Symname", respectively), + but highlights the referenced symbol as \emph{being defined} + in the current definition. + \end{function} + + \begin{mmtbox} + The special |type=symdoc| for \stexcode"sparagraph" is intended to be used for + ``informal definitions'', or encyclopedia-style descriptions for symbols. + + The \mmt system can use those (in lieu of an actual \stexcode"sdefinition" in scope) + to present to users, e.g. when hovering over symbols. + \end{mmtbox} + + \begin{function}{\definiens} + Additionally, \stexcode"sdefinition" (and \stexcode"sparagraph" with + |type=symdoc|) introduces \stexcode"\definiens[<optional symbolname>]{<code>}" + which marks up |<code>| as being the explicit \emph{definiens} + of |<optional symbolname>| (in case |for=| has multiple symbols). + \end{function} + + All four statement environments -- i.e. \stexcode|sdefinition|, + \stexcode|sassertion|, \stexcode|sexample|, and \stexcode|sparagraph| -- also take an + optional parameter |name=| -- if this one is given a value, the environment will + generate a \emph{symbol} by that name (but with no semantic macro). Not only does this + allow for \stexcode"\symref" et al, it allows us to resume our earlier example for + monoids much more nicely:\ednote{MK: we should reference the example explicitly here.} + + \symdef{set}{\comp{\texttt{Set}}} + \symdef{equal}[args=2]{#1 \comp= #2} + \symdef{inset}[args=2]{#1 \comp\in #2} + \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2} + + \stexexample{% +\begin{mathstructure}{monoid} + \symdef{universe}[type=\set]{\comp{U}} + \symdef{op}[ + args=2, + type=\funtype{\universe,\universe}{\universe}, + op=\circ + ]{#1 \comp{\circ} #2} + \symdef{unit}[type=\universe]{\comp{e}} + + \begin{sparagraph}[type=symdoc,for=monoid] + A \definame{monoid} is a structure + $\mathstruct{\universe,\op!,\unit}$ + where $\op!:\funtype{\universe}{\universe}$ and + $\inset{\unit}{\universe}$ such that + + \begin{sassertion}[name=associative, + type=axiom, + title=Associativity] + $\op!$ is associative + \end{sassertion} + \begin{sassertion}[name=isunit, + type=axiom, + title=Unit] + $\equal{\op{\svar{x}}{\unit}}{\svar{x}}$ + for all $\inset{\svar{x}}{\universe}$ + \end{sassertion} + \end{sparagraph} +\end{mathstructure} + +An example for a \symname{monoid} is... + } + + The main difference to before\ednote{MK: reference} is that the two + \stexcode|sassertion|s now have |name=| attributes. Thus the \stexcode"mathstructure" + \symname{monoid} now contains two additional symbols, namely the axioms for + associativity and that $e$ is a unit. Note that both symbols do not represent the mere + \emph{propositions} that e.g. $\circ$ is associative, but \emph{the assertion that it + is actually true} that $\circ$ is associative. + + If we now want to instantiate |monoid| (unless with a variable, + of course), we also need to assign |associative| and |neutral| + to analogous assertions. So the earlier example + \begin{latexcode}[gobble=8] + \instantiate{intmonoid}{monoid}{\mathbb{Z}_{+,0}}[ + universe = Int , + op = addition , + unit = zero + ] + \end{latexcode} + ...will not work anymore. We now need to give assertions that + |addition| is associative and that |zero| is a unit with respect + to addition.\footnote{Of course, \sTeX can not check that + the assertions are the ``correct'' ones -- but if + the assertions (both in |monoid| as well as those for addition and + zero) are properly marked up, \mmt can. \textcolor{red}{TODO: should}} + +\end{smodule} +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: sec.customhighlight a,prec additionandmultiplication.ex trivial,boring +% LocalWords: addition,multiplication symdoc symdoc,for isunit diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-symbols.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-symbols.tex index 50b450a248f..e7bafeda6b6 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-symbols.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-symbols.tex @@ -1 +1,587 @@ -\textcolor{red}{TODO: symbols documentation}
\ No newline at end of file +\begin{smodule}[ns=https://github.com/slatex/sTeX/doc]{SymbolsAndNotations} +\begin{sfragment}{Declaring New Symbols and Notations} + Inside an \stexcode"smodule" environment, we can declare new \sTeX symbols. + +\begin{function}{\symdecl} + The most basic command for doing so is using \stexcode"\symdecl{symbolname}". This + introduces a new symbol with name |symbolname|, arity $0$ and semantic macro + \stexcode"\symbolname". + + The starred variant \stexcode"\symdecl*{symbolname}" will declare a symbol, but not + introduce a semantic macro. If we don't want to supply a notation (for example to + introduce concepts like ``abelian'', which is not something that has a notation), the + starred variant is likely to be what we want. +\end{function} +\begin{mmtbox} + \stexcode"\symdecl" introduces a new \omdoc/\mmt constant in the current module + (=\omdoc/\mmt theory). Correspondingly, they get assigned the URI + |<module-URI>?<constant-name>|. +\end{mmtbox} + +Without a semantic macro or a notation, the only meaningful way to reference a symbol is +via \stexcode"\symref",\stexcode"\symname" etc. + +\stexexample{% +\symdecl*{foo} +Given a \symname{foo}, we can... +} + +Obviously, most semantic macros should take actual \emph{arguments}, implying that the +symbol we introduce is an \emph{operator} or \emph{function}. We can let +\stexcode"\symdecl" know the \emph{arity} (i.e. number of arguments) of a symbol like +this: + +\stexexample{% +\symdecl{binarysymbol}[args=2] +\symref{binarysymbol}{this} is a symbol taking two arguments. +} + +So far we have gained exactly \ldots nothing by adding the arity information: we cannot do +anything with the arguments in the text. + +We will now see what we can gain with more machinery. + +\begin{function}{\notation} + We probably want to supply a notation as well, in which case we can finally actually use + the semantic macro in math mode. We can do so using the \stexcode"\notation" command, + like this: + +\stexexample{% +\notation{binarysymbol}{\text{First: }#1\text{; Second: }#2} +$\binarysymbol{a}{b}$ } +\end{function} + +\begin{mmtbox} + Applications of semantic macros, such as \stexcode"\binarysymbol{a}{b}" are translated + to \mmt/\omdoc as |OMA|-terms with head |<OMS name="...?binarysymbol"/>|. + + Semantic macros with no arguments correspond to |OMS| directly. +\end{mmtbox} + +\begin{function}{\comp} + For many semantic services e.g. semantic highlighting or \defemph{wikification} (linking + user-visible notation components to the definition of the respective symbol they come + from), we need to specify the notation components. Unfortunately, there is currently no + way the \sTeX engine can infer this by itself, so we have to specify it manually in the + notation specification. We can do so with the \stexcode"\comp" command. +\end{function} + +We can introduce a new notation |highlight| for \stexcode"\binarysymbol" that fixes this +flaw, which we can subsequently use with \stexcode"\binarysymbol[highlight]": + +\stexexample{% +\notation{binarysymbol}[highlight] + {\comp{\text{First: }}#1\comp{\text{; Second: }}#2} +$\binarysymbol[highlight]{a}{b}$ +} + +\begin{dangerbox} + Ideally, \stexcode"\comp" would not be necessary: Everything in a notation that is + \emph{not} an argument should be a notation component. Unfortunately, it is + computationally expensive to determine where an argument begins and ends, and the + argument markers |#n| may themselves be nested in other macro applications or + \TeX\xspace groups, making it ultimately almost impossible to determine them + automatically while also remaining compatible with arbitrary highlighting customizations + (such as tooltips, hyperlinks, colors) that users might employ, and that are ultimately + invoked by \stexcode"\comp". +\end{dangerbox} + +\begin{dangerbox} + Note that it is required that + \begin{enumerate} + \item the argument markers |#n| never occur inside a \stexcode"\comp", and + \item no semantic arguments may ever occur inside a notation. + \end{enumerate} + Both criteria are not just required for technical reasons, but conceptionally + meaningful: + + The underlying principle is that the arguments to a semantic macro represent + \emph{arguments to the mathematical operation} represented by a symbol. For example, a + semantic macro \stexcode"\addition{a}{b}" taking two arguments would represent \emph{the + actual addition of (mathematical objects) $a$ and $b$}. It should therefore be + impossible for $a$ or $b$ to be part of a notation component of \stexcode"\addition". + + Similarly, a semantic macro can not conceptually be part of the notation of + \stexcode"\addition", since a semantic macro represents a \emph{distinct mathematical + concept} with \emph{its own semantics}, whereas notations are syntactic + representations of the very symbol to which the notation belongs. + + If you want an argument to a semantic macro to be a purely syntactic parameter, then you + are likely somewhat confused with respect to the distinction between the precise + \emph{syntax} and \emph{semantics} of the symbol you are trying to declare (which + happens quite often even to experienced \sTeX users), and might want to give those + another thought - quite likely, the macro you aim to implement does not actually + represent a semantically meaningful mathematical concept, and you will want to use + \stexcode"\def" and similar native \LaTeX\xspace macro definitions rather than semantic + macros. +\end{dangerbox} + +\begin{function}{\symdef} + In the vast majority of cases where a symbol declaration should come with a semantic + macro, we will want to supply a notation immediately. For that reason, the + \stexcode"\symdef" command combines the functionality of both \stexcode"\symdecl" and + \stexcode"\notation" with the optional arguments of both: +\end{function} + +\stexexample{% +\symdef{newbinarysymbol}[hl,args=2] + {\comp{\text{1.: }}#1\comp{\text{; 2.: }}#2} +$\newbinarysymbol{a}{b}$ +} + +We just declared a new symbol |newbinarysymbol| with |args=2| and immediately provided it +with a notation with identifier |hl|. Since |hl| is the \emph{first} (and so far, only) +notation supplied for |newbinarysymbol|, using \stexcode"\newbinarysymbol" without +optional argument defaults to this notation.\bigskip + +But one man's meat is another man's poison: it is very subjective what the ``default +notation'' of an operator should be. Different communities have different practices. For +instance, the complex unit is written as $i$ in Mathematics and as $j$ in electrical +engineering. So to allow modular specification and facilitate re-use of document fragments +\sTeX allows to re-set notation defaults. + +\begin{function}{\setnotation} + The first notation provided will stay the default notation unless explicitly changed -- + this is enabled by the \stexcode"\setnotation" command: + \stexcode"\setnotation{symbolname}{notation-id}" sets the default notation of + \stexcode"\symbolname" to |notation-id|, i.e. henceforth, \stexcode"\symbolname" behaves + like \stexcode"\symbolname[notation-id]" from now on. +\end{function} + +Often, a default notation is set right after the corresponding notation is introduced -- +the starred version \stexcode"\notation*" for that reason introduces a new notation and +immediately sets it to be the new default notation. So expressed differently, the +\emph{first} \stexcode"\notation" for a symbol behaves exactly like \stexcode"\notation*", +and \stexcode"\notation*{foo}[bar]{...}" behaves exactly like +\stexcode"\notation{foo}[bar]{...}\setnotation{foo}{bar}". + +\begin{function}{\textsymdecl} + In the less mathematical settings where we want a symbol and + semantic macro for some concept with a notation \emph{beyond} + its mere name, but which should also be available in \TeX's text + mode, the command \stexcode"\textsymdecl" is useful. + For example, we can declare a symbol \stexcode"openmath" + with the notation \stexcode"\textsc{OpenMath}" using + \textsymdecl{openmath}[name=OpenMath]{\textsc{OpenMath}} + \stexcode"\textsymdecl{openmath}[name=OpenMath]{\textsc{OpenMath}}". + The \stexcode"\openmath" yields \openmath both in text and math + mode. +\end{function} + +\begin{sfragment}{Operator Notations} + Once we have a semantic macro with arguments, such as \stexcode"\newbinarysymbol", the + semantic macro represents the \emph{application} of the symbol to a list of + arguments. What if we want to refer to the operator \emph{itself}, though? + + We can do so by supplying the \stexcode"\notation" (or \stexcode"\symdef") with an + \emph{operator notation}, indicated with the optional argument |op=|. We can then + invoke the operator notation using \stexcode"\symbolname![notation-identifier]". Since + operator notations never take arguments, we do not need to use \stexcode"\comp" in it, + the whole notation is wrapped in a \stexcode"\comp" automatically: + + \stexexample{% + \notation{newbinarysymbol}[ab, op={\text{a:}\cdot\text{; b:}\cdot}] + {\comp{\text{a:}}#1\comp{\text{; b:}}#2} \symname{newbinarysymbol} is also + occasionally written $\newbinarysymbol![ab]$ + } + + \begin{mmtbox} + \stexcode"\symbolname!" is translated to \omdoc/\mmt as |<OMS name="...?symbolname"/>| + directly. + \end{mmtbox} + +\end{sfragment} +\end{sfragment} + +\begin{sfragment}{Argument Modes} + The notations so far used \emph{simple} arguments which we call \emph{mode}-|i| + arguments. Declaring a new symbol with \stexcode"\symdecl{foo}[args=3]" is equivalent to + writing \stexcode"\symdecl{foo}[args=iii]", indicating that the semantic macro takes + three mode-|i| arguments. However, there are three more argument modes which we will + investigate now, namely mode-|b|, mode-|a| and mode-|B| arguments. + +\begin{sfragment}{Mode-\texttt b Arguments} + +A mode-|b| argument represents a \emph{variable} that is \emph{bound} by the symbol in +its application, making the symbol a \emph{binding operator}. Typical examples of +binding operators are e.g. sums $\sum$, products $\prod$, integrals $\int$, quantifiers +like $\forall$ and $\exists$, that $\lambda$-operator, etc. + +\begin{mmtbox} + Mode-|b| arguments behave exactly like mode-|i| arguments within \TeX, but applications + of binding operators, i.e. symbols with mode-|b| arguments, are translated to + |OMBIND|-terms in \omdoc/\mmt, rather than |OMA|. +\end{mmtbox} + +For example, we can implement a summation operator binding an index variable and taking +lower and upper index bounds and the expression to sum over like this: + +\stexexample{% +\symdef{summation}[args=biii] + {\mathop{\comp{\sum}}_{#1\comp{=}#2}^{#3}#4} + $\summation{\svar{x}}{1}{\svar{n}}{\svar{x}}^2$ +} + +where the variable $\svar{x}$ is now \emph{bound} by the \stexcode"\summation"-symbol in +the expression. +\end{sfragment} + +\begin{sfragment}{Mode-\texttt a Arguments} + Mode-|a| arguments represent a \emph{flexary argument sequence}, i.e. a sequence of + arguments of arbitrary length. Formally, operators that take arbitrarily many arguments + don't ``exist'', but in informal mathematics, they are ubiquitous. Mode-|a| arguments + allow us to write e.g. \stexcode"\addition{a,b,c,d,e}" rather than having to write + something like \stexcode"\addition{a}{\addition{b}{\addition{c}{\addition{d}{e}}}}"! + + \stexcode"\notation" (and consequently \stexcode"\symdef", too) take one additional + argument for each mode-|a| argument that indicates how to ``accumulate'' a + comma-separated sequence of arguments. This is best demonstrated on an example. + + Let's say we want an operator representing quantification over an ascending chain of + elements in some set, i.e. \stexcode"\ascendingchain{S}{a,b,c,d,e}{t}" should yield + $\forall a{<_S}b{<_S}c{<_S}d{<_S}e.\,t$. The ``base''-notation for this operator is + simply\\ \stexcode"{\comp{\forall} #2\comp{.\,}#3}", where |#2| represents the full + notation fragment \emph{accumulated} from |{a,b,c,d,e}|. + + The \emph{additional} argument to \stexcode"\notation" (or \stexcode"\symdef") takes the + same arguments as the base notation and two \emph{additional} arguments |##1| and |##2| + representing successive pairs in the mode-|a| argument, and accumulates them into |#2|, + i.e. to produce $a<_Sb<_Sc<_Sd<_Se$, we do \stexcode"{##1 \comp{<}_{#1} ##2}": + + \stexexample{% +\symdef{ascendingchain}[args=iai] + {\comp{\forall} #2\comp{.\,}#3} + {##1 \comp{<}_{#1} ##2} + +Tadaa: $\ascendingchain{S}{a,b,c,d,e}{t}$ +} + +If this seems overkill, keep in mind that you will rarely need the single-hash arguments +|#1|,|#2| etc. in the |a|-notation-argument. For a much more representative and simpler +example, we can introduce flexary addition via: +\stexexample{% + \symdef{addition}[args=a]{#1}{##1 \comp{+} ##2} + +Tadaa: $\addition{a,b,c,d,e}$ +} + +\begin{sfragment}{The \texttt{assoc}-key} + We mentioned earlier that ``formally'', flexary arguments don't really + ``exist''. Indeed, formally, addition is usually defined as a binary operation, + quantifiers bind a single variable etc. + + Consequently, we can tell \sTeX (or, rather, \mmt/\omdoc) how to ``resolve'' flexary + arguments by providing \stexcode"\symdecl" or \stexcode"\symdef" with an optional + |assoc|-argument, as in \stexcode"\symdecl{addition}[args=a,assoc=bin]". The possible + values for the |assoc|-key are: + \begin{itemize} + \item[|bin|:] A binary, associative argument, e.g. as in \stexcode"\addition" + \item[|binl|:] A binary, left-associative argument, e.g. + $a^{\scriptstyle b^{\scriptstyle c^d}}$, which stands for $((a^b)^c)^d$ + \item[|binr|:] A binary, right-associative argument, e.g. as in $A\to B\to C\to D$, + which stands for $A \to (B \to (C \to D))$ + \item[|pre|:] Successively prefixed, e.g. as in $\forall x,y,z.\,P$, which stands for + $\forall x.\, \forall y.\, \forall z.\,P$ + \item[|conj|:] Conjunctive, e.g. as in $a=b=c=d$ or $a,b,c,d\in A$, which stand for + $a=d\wedge b=d\wedge c=d$ and $a\in A\wedge b\in A \wedge c\in A\wedge d\in A$, + respectively + \item[|pwconj|:] Pairwise conjunctive, e.g. as in $a\neq b\neq c\neq d$, which stands + for $a\neq b\wedge a\neq c\wedge a\neq d\wedge b\neq c\wedge b\neq d\wedge c\neq d$ + \end{itemize} + As before, at the PDF level, this annotation is invisible (and without effect), but at + the level of the generated OMDoc/MMT this leads to more semantical expressions. +\end{sfragment} +\end{sfragment} + +\begin{sfragment}{Mode-\texttt B Arguments} + Finally, mode-|B| arguments simply combine the functionality of both |a| and |b| - + i.e. they represent an arbitrarily long sequence of variables to be bound, e.g. for + implementing quantifiers: + + \stexexample{% +\symdef{quantforall}[args=Bi] + {\comp{\forall}#1\comp{.}#2} + {##1\comp,##2} + +$\quantforall{\svar{x},\svar{y},\svar{z}}{P}$ +} +\end{sfragment} +\end{sfragment} + +\begin{sfragment}{Type and Definiens Components} + \stexcode"\symdecl" and \stexcode"\symdef" take two more optional arguments. \TeX\xspace + largely ignores them (except for special situations we will talk about later), but \mmt + can pick up on them for additional services. These are the |type| and |def| keys, which + expect expressions in math-mode (ideally using semantic macros, of course!) + + \begin{mmtbox} + The |type| and |def| keys correspond to the |type| and |definiens| components of + \omdoc/\mmt constants. + + Correspondingly, the name ``type'' should be taken with a grain of salt, since + \omdoc/\mmt -- being foundation-independent -- does not a priori implement a fixed + typing system. + \end{mmtbox} + + \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2} + \symdef{fun}[args=bi]{#1 \comp\mapsto #2} + \symdef{set}{\comp{\texttt{Set}}} + + The |type|-key allows us to provide additional information + (given the necessary \sTeX symbols), e.g. for + addition on natural numbers: + + \stexexample{% +\symdef{Nat}[type=\set]{\comp{\mathbb N}} +\symdef{addition}[ + type=\funtype{\Nat,\Nat}{\Nat}, + op=+, + args=a +]{#1}{##1 \comp+ ##2} + +\symname{addition} is an operation $\funtype{\Nat,\Nat}{\Nat}$ +} + +The |def|-key allows for declaring symbols as abbreviations: +\stexexample{% +\symdef{successor}[ + type=\funtype{\Nat}{\Nat}, + def=\fun{\svar{x}}{\addition{\svar{x},1}}, + op=\mathtt{succ}, + args=1 +]{\comp{\mathtt{succ(}#1\comp{)}}} + +The \symname{successor} operation $\funtype{\Nat}{\Nat}$ +is defined as $\fun{\svar{x}}{\addition{\svar{x},1}}$ +} +\end{sfragment} + +\begin{sfragment}{Precedences and Automated Bracketing} + Having done \stexcode"\addition", the obvious next thing to implement is + \stexcode"\multiplication". This is straight-forward in theory: + + \stexexample{% +\symdef{multiplication}[ + type=\funtype{\Nat,\Nat}{\Nat}, + op=\cdot, + args=a +]{#1}{##1 \comp\cdot ##2} + +\symname{multiplication} is an operation $\funtype{\Nat,\Nat}{\Nat}$ +} + +However, if we \emph{combine} \stexcode"\addition" and \stexcode"\multiplication", we +notice a problem: + +\stexexample{% +$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ +} + +We all know that $\multiplication!$ binds stronger than $\addition!$, so the output +$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ does not actually +reflect the term we wrote. We can of course insert parentheses manually + +\stexexample{% +$\addition{a,\multiplication{b,(\addition{c,\multiplication{d,e}})}}$ +} +but we can also do better by supplying \emph{precedences} and +have \sTeX insert parentheses automatically. + +For that purpose, \stexcode"\notation" (and hence \stexcode"\symdef") take an optional +argument |prec=<opprec>;<argprec1>x...x<argprec n>|. + +We will investigate the precise meaning of |<opprec>| and the |<argprec>|s shortly -- in +the vast majority of cases, it is perfectly sufficient to think of |prec=| taking a single +number and having that be \emph{the} precedence of the notation, where lower precedences +(somewhat counterintuitively) bind stronger than higher precedences. So fixing our +notations for \stexcode"\addition" and \stexcode"\multiplication", we get: + +\stexexample{% +\notation{multiplication}[ + op=\cdot, + prec=50 +]{#1}{##1 \comp\cdot ##2} +\notation{addition}[ + op=+, + prec=100 +]{#1}{##1 \comp+ ##2} + +$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ +} + +Note that the precise numbers used for precedences are pretty arbitrary - what matters is +which precedences are higher than which other precedences when used in conjunction. +\begin{variable}{\infprec,\neginfprec} + It is occasionally useful to have ``infinitely'' high or low precedences to enforce or + forbid automated bracketing entirely -- for those purposes, \stexcode"\infprec" and + \stexcode"\neginfprec" exist (which are implemented as the maximal and minimal integer + values accordingly). +\end{variable} + +\begin{dangerbox} + More precisely, each notation takes + \begin{enumerate} + \item One \emph{operator precedence} and + \item one \emph{argument precedence} for each argument. + \end{enumerate} + By default, all precedences are $0$, unless the symbol takes no argument, in which case + the operator precedence is \stexcode"\neginfprec" (negative infinity). If we only + provide a single number, this is taken as both the operator precedence and all argument + precedences. + + \sTeX decides whether to insert parentheses by comparing operator precedences to a + \emph{downward precedence} $p_d$ with initial value \stexcode"\infprec". When + encountering a semantic macro, \sTeX takes the operator precedence $p_{op}$ of the + notation used and checks whether $p_{op}>p_d$. If so, \sTeX insert parentheses. + + When \sTeX steps into an argument of a semantic macro, it sets $p_d$ to the respective + argument precedence of the notation used. + + In the example above: + \begin{enumerate} + \item \sTeX starts out with $p_d=$\stexcode"\infprec". + \item \sTeX encounters \stexcode"\addition" with $p_{op}=100$. Since + $100\not>$\stexcode"\infprec", it inserts no parentheses. + \item Next, \sTeX encounters the two arguments for \stexcode"\addition". Both have no + specifically provided argument precedence, so \sTeX uses $p_d=p_{op}=100$ for both and + recurses. + \item Next, \sTeX encounters \stexcode"\multiplication{b,...}", whose notation has + $p_{op}=50$. + \item We compare to the current downward precedence $p_d$ set by \stexcode"\addition", + arriving at $p_{op}=50\not>100=p_d$, so \sTeX again inserts no parentheses. + \item Since the notation of \stexcode"\multiplication" has no explicitly set argument + precedences, \sTeX uses the operator precedence for all arguments of + \stexcode"\multiplication", hence sets $p_d=p_{op}=50$ and recurses. + \item Next, \sTeX encounters the inner \stexcode"\addition{c,...}" whose notation has + $p_{op}=100$. + \item We compare to the current downward precedence $p_d$ set by + \stexcode"\multiplication", arriving at $p_{op}=100>50=p_d$ -- which finally prompts + \sTeX to insert parentheses, and we proceed as before. + \end{enumerate} +\end{dangerbox} +\end{sfragment} + +\begin{sfragment}{Variables} + All symbol and notation declarations require a module with which they are associated, + hence the commands \stexcode"\symdecl", \stexcode"\notation", \stexcode"\symdef" + etc. are disabled outside of |smodule|-environments. + + Variables are different -- variables are allowed everywhere, are not exported when the + current module (if one exists) is imported (via \stexcode"\importmodule" or + \stexcode"\usemodule") and (also unlike symbol declarations) ``disappear'' at the end of + the current \TeX\xspace group. + + \begin{function}{\svar} + So far, we have always used variables using \stexcode"\svar{n}", which marks-up $n$ as + a variable with name |n|. More generally, \stexcode"\svar[foo]{<texcode>}" marks-up + the arbitrary |<texcode>| as representing a variable with name |foo|. + \end{function} + + Of course, this makes it difficult to reuse variables, or introduce ``functional'' + variables with arities $>0$, or provide them with a type or definiens. + + \begin{function}{\vardef} + For that, we can use the \stexcode"\vardef" command. Its syntax is largely the same as + that of \stexcode"\symdef", but unlike symbols, variables have only one notation + (\textcolor{red}{TODO: so far?}), hence there is only \stexcode"\vardef" and no + \stexcode"\vardecl". + \end{function} + +\stexexample{% +\vardef{varf}[ + name=f, + type=\funtype{\Nat}{\Nat}, + op=f, + args=1, + prec=0;\neginfprec +]{\comp{f}#1} +\vardef{varn}[name=n,type=\Nat]{\comp{n}} +\vardef{varx}[name=x,type=\Nat]{\comp{x}} + +Given a function $\varf!:\funtype{\Nat}{\Nat}$, +by $\addition{\varf!,\varn}$ we mean the function +$\fun{\varx}{\varf{\addition{\varx,\varn}}}$ +} + +(of course, ``lifting'' addition in the way described in the previous example is an +operation that deserves its own symbol rather than abusing \stexcode"\addition", +but... well.) + +\textcolor{red}{TODO: bind=forall/exists} +\end{sfragment} + +\begin{sfragment}{Variable Sequences} + Variable \emph{sequences} occur quite frequently in informal mathematics, hence they + deserve special support. Variable sequences behave like variables in that they disappear + at the end of the current \TeX\xspace group and are not exported from modules, but their + declaration is quite different. + + \begin{function}{\varseq} + A variable sequence is introduced via the command \stexcode"\varseq", which takes the + usual optional arguments |name| and |type|. It then takes a starting index, an end + index and a \emph{notation} for the individual elements of the sequence parametric in + an index. Note that both the starting as well as the ending index may be variables. + \end{function} + + This is best shown by example: + \stexexample{% +\vardef{varn}[name=n,type=\Nat]{\comp{n}} +\varseq{seqa}[name=a,type=\Nat]{1}{\varn}{\comp{a}_{#1}} + +The $i$th index of $\seqa!$ is $\seqa{i}$. +} + +Note that the syntax |\seqa!| now automatically generates a presentation based on the +starting and ending index. + +\textcolor{red}{TODO: more notations for invoking sequences}. + +\vardef{varn}[name=n,type=\Nat]{\comp{n}} +\varseq{seqa}[name=a]{1}{\varn}{\comp{a}_{#1}} + +Notably, variable sequences are nicely compatible with |a|-type arguments, so we can do +the following: + +\stexexample{% +$\addition{\seqa}$ +} + +Sequences can be \emph{multidimensional} using the |args|-key, in which case the +notation's arity increases and starting and ending indices have to be provided as a +comma-separated list: + +\stexexample{% +\vardef{varm}[name=m,type=\Nat]{\comp{m}} +\varseq{seqa}[ + name=a, + args=2, + type=\Nat, +]{1,1}{\varn,\varm}{\comp{a}_{#1}^{#2}} + +$\seqa!$ and $\addition{\seqa}$ +} +\vardef{varm}[name=m,type=\Nat]{\comp{m}} + +We can also explicitly provide a ``middle'' segment to be used, like such: + +\stexexample{% +\varseq{seqa}[ + name=a, + type=\Nat, + args=2, + mid={\comp{a}_{\varn}^1,\comp{a}_1^2,\ellipses,\comp{a}_{1}^{\varm}} +]{1,1}{\varn,\varm}{\comp{a}_{#1}^{#2}} + +$\seqa!$ and $\addition{\seqa}$ +} +\end{sfragment} +\end{smodule} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: binarysymbol newbinarysymbol hl,args a,b,c,d,e ascendingchain assoc binl +% LocalWords: a,assoc binr x,y,z conj a,b,c,d pwconj funtype succ prec opprec argprec1 +% LocalWords: argprec texcode varf varn n,type varx x,type varseq seqa a,type th m,type diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-terms.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-terms.tex index cc67ce0c7fc..759b3f5fdd8 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-terms.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-terms.tex @@ -1 +1,177 @@ -\textcolor{red}{TODO: terms documentation}
\ No newline at end of file +\begin{smodule}{SymbolsInText} + \symdef{set}{\comp{\texttt{Set}}} + + Given a symbol declaration \stexcode"\symdecl{symbolname}", + we obtain a semantic macro \stexcode"\symbolname". + We can use this semantic macro in math mode to use its notation(s), + and we can use \stexcode"\symbolname!" + in math mode to use its operator notation(s). + What else can we do? + +\begin{sfragment}{\texttt{\textbackslash symref} and its variants} + + \begin{function}{\symref,\symname} + We have already seen \stexcode"\symname" and + \stexcode"\symref", the latter being the more general. + + \stexcode"\symref{<symbolname>}{<code>}" marks-up |<code>| + as referencing |<symbolname>|. Since quite often, the |<code>| + should be (a variant of) the name of the symbol anyway, + we also have \stexcode"\symname{<symbolname>}". + \end{function} + + Note that \stexcode"\symname" uses the \emph{name} + of a symbol, not its macroname. More precisely, + \stexcode"\symname" will insert the name of the symbol + with ``|-|'' replaced by spaces. + If a symbol does not have + an explicit |name=| given, the two are equal -- but + for \stexcode"\symname" it often makes sense to make the + two explicitly distinct. For example: + \stexexample{% +\symdef{Nat}[ + name=natural-number, + type=\set +]{\comp{\mathbb{N}}} + +A \symname{Nat} is... + } + + \stexcode"\symname" takes two additional optional + arguments, |pre=| and |post=| that get prepended or appended + respectively to the symbol name. + + \begin{function}{\Symname} + Additionally, \stexcode"\Symname" behaves exactly + like \stexcode"\symname", but will capitalize the first + letter of the name: + \end{function} + \stexexample{% +\Symname[post=s]{Nat} are... + } + + \begin{dangerbox} + This is as good a place as any other to explain how + \sTeX resolves a string |symbolname| to an actual symbol. + + If \stexcode"\symbolname" is a semantic macro, then + \sTeX has no trouble resolving |symbolname| to the full + URI of the symbol that is being invoked. + + However, especially in \stexcode"\symname" (or if a symbol + was introduced using \stexcode"\symdecl*" without + generating a semantic macro), we might + prefer to use the \emph{name} of a symbol directly for + readability -- e.g. we would want to write + \stexcode"A \symname{natural-number} is..." rather than + \stexcode"A \symname{Nat} is...". \sTeX attempts to handle + this case thusly: + + If |string| does \emph{not} correspond to a semantic + macro \stexcode"\string" and does \emph{not} + contain a |?|, then \sTeX checks + all symbols currently in scope until it finds one, + whose name is |string|. If |string| is of the + form |pre?name|, \sTeX first looks through all modules + currently in scope, whose full URI ends with |pre|, + and then looks for a symbol with name |name| in those. + This allows + for disambiguating more precisely, e.g. by + saying \stexcode"\symname{Integers?addition}" + or \stexcode"\symname{RealNumbers?addition}" in the + case where several |addition|s are in scope. + \end{dangerbox} +\end{sfragment} + +\symdef{addition}[op=+,prec=100,args=2]{#1 \comp+ #2} +\symdef{multiplication}[op=\cdot,prec=50,args=a]{#1}{##1 \comp\cdot ##2} + +\begin{sfragment}{Marking Up Text and On-the-Fly Notations} + We can also use semantic macros outside of text mode though, + which allows us to annotate arbitrary text fragments. + + Let us assume again, that we have + \stexcode"\symdef{addition}[args=2]{#1 \comp+ #2}". Then we + can do + \stexexample{% +\addition{\comp{The sum of} \arg{$\svar{n}$} \comp{ and }\arg{$\svar{m}$}} +is... + } + ...which marks up the text fragment as representing + an \emph{application} of the |addition|-symbol to two + argument $\svar{n}$ and $\svar{m}$. + + \begin{mmtbox} + As expected, the above example is translated to \omdoc/\mmt + as an |OMA| with |<OMS name="...?addition"/>| as head and + |<OMV name="n"/>| and |<OMV name="m"/>| as arguments. + \end{mmtbox} + + \begin{dangerbox} + Note the difference in treating ``arguments'' between math mode and text mode. In + math mode the (in this case two) tokens/groups following the \stexcode|\addition| + macro are treated as arguments to the addition function, whereas in text mode the + group following \stexcode|\addition| is taken to be the ad-hoc presentation. We + drill in on this now. + \end{dangerbox} + + \begin{function}{\arg} + In text mode, every semantic macro takes exactly one + argument, namely the text-fragment to be annotated. + The \stexcode"\arg" command is only valid within the + argument to a semantic macro and marks up the + \emph{individual arguments} for the symbol. + \end{function} + + We can also use semantic macros in text mode to invoke + an operator itself instead of its application, with the + usual syntax using |!|: + \stexexample{% +\addition!{Addition} is... + } + + Indeed, \stexcode"\symbolname!{<code>}" is exactly equivalent to + \stexcode"\symref{symbolname}{<code>}" (the latter is in fact implemented in terms of + the former). + + \stexcode"\arg" also allows us to switch the order of arguments + around and ``hide'' arguments: For example, \stexcode"\arg[3]{<code>}" + signifies that |<code>| represents the \emph{third} + argument to the current operator, and \stexcode"\arg*[i]{<code>}" + signifies that |<code>| represents the $i$th argument, but it + should not produce any output (it is exported in the |xhtml| + however, so that \mmt and other systems can pick up on it).\ednote{MK: I do not + understand why we have to/want to give the second arg*; I think this must be + elaborated on.} + \stexexample{% +\addition{\comp{adding} + \arg[2]{$\svar{k}$} + \arg*{$\addition{\svar{n}}{\svar{m}}$}} yields... + } + Note that since the second \stexcode"\arg" has no explicit argument + number, it automatically represents the first not-yet-given + argument -- i.e. in this case the first one.\ednote{MK: I do not understand this at + all. } + + \paragraph{} The same syntax can be used in math mod as well. This allows us to + spontaneously introduce new notations on the fly. We can activate it using the starred + variants of semantic macros: + + \stexexample{% +Given $\addition{\svar{n}}{\svar{m}}$, then +$\addition*{ + \arg*{\addition{\svar{n}}{\svar{m}}} + \comp{+} + \arg{\svar{k}} +}$ yields... + } + +\end{sfragment} +\end{smodule} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: + +% LocalWords: prec cdot,prec 50,args th diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-tikzinput.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-tikzinput.tex index fb7d0c1e5b2..ac321f129cd 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-tikzinput.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-tikzinput.tex @@ -1 +1,61 @@ -\textcolor{red}{TODO: tikzinput documentation}
\ No newline at end of file +\begin{function}{image} + The behavior of the \pkg{ikzinput} package is determined by whether the |image| option + is given. If it is not, then the \pkg{tikz} package is loaded, all other options are + passed on to it and |\tikzinput{|\meta{file}|}| inputs the TIKZ file \meta{file}|.tex|; + if not, only the \pkg{graphicx} package is loaded and |\tikzinput{|\meta{file}|}| loads + an image file \meta{file}|.|\meta{ext} generated from \meta{file}|.tex|. +\end{function} + +The selective input functionality of the \pkg{tikzinput} package assumes that the TIKZ +pictures are externalized into a standalone picture file, such as the following one + +\begin{latexcode} +\documentclass{standalone} +\usepackage{tikz} +\usetikzpackage{...} +\begin{document} + \begin{tikzpicture} + ... + \end{tikzpicture} +\end{document} +\end{latexcode} + + The \pkg{standalone} class is a minimal {\LaTeX} class that when loaded in a document + that uses the \pkg{standalone} package: the preamble and the |documenat| environment + are disregarded during loading, so they do not pose any problems. In effect, an + |\input| of the file above only sees the |tikzpicture| environment, but the file itself + is standalone in the sense that we can run {\LaTeX} over it separately, e.g. for + generating an image file from it. + +\begin{function}{\tikzinput,\ctikzinput} + This is exactly where the \pkg{tikzinput} package comes in: it supplies the |\tikzinput| + macro, which -- depending on the |image| option -- either directly inputs the TIKZ + picture (source) or tries to load an image file generated from it. + + Concretely, if the |image| option is not set for the \pkg{tikzinput} package, then + |\tikzinput[|\meta{opt}|]{|\meta{file}|}| disregards the optional argument \meta{opt} + and inputs \meta{file}|.tex| via |\input| and resizes it to as specified in the |width| + and |height| keys. If it is, |\tikzinput[|\meta{opt}|]{|\meta{file}|}| expands to + |\includegraphics[|\meta{opt}|]{|\meta{file}|}|. + + |\ctizkinput| is a version of |\tikzinput| that is centered. +\end{function} + +\begin{function}{\mhtikzinput,\cmhtikzinput} + |\mhtizkinput| is a variant of |\tikzinput| that treats its file path argument as a + relative path in a math archive in analogy to \stexcode|\inputref|. To give the archive + path, we use the |mhrepos=| key. Again, |\cmhtizkinput| is a version of |\mhtikzinput| + that is centered. +\end{function} + +\begin{function}{\libusetikzlibrary} + Sometimes, we want to supply archive-specific TIKZ libraries in the |lib| folder of the + archive or the |meta-inf/lib| of the archive group. Then we need an analogon to + \stexcode|\libinput| for \stexcode|\usetikzlibrary|. The \pkg{stex-tikzinput} package + provides the \stexcode|libusetikzlibrary| for this purpose. +\end{function} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../stex-manual" +%%% End: diff --git a/Master/texmf-dist/doc/latex/stex/stex-abstract.tex b/Master/texmf-dist/doc/latex/stex/stex-abstract.tex index 445bbf064aa..f342bbf9075 100644 --- a/Master/texmf-dist/doc/latex/stex/stex-abstract.tex +++ b/Master/texmf-dist/doc/latex/stex/stex-abstract.tex @@ -1,10 +1,26 @@ \begin{abstract} - \sTeX is a collection of {\LaTeX} package that allow to markup documents semantically without leaving the document format, essentially turning {\LaTeX} into a document format for mathematical knowledge management (MKM). + \sTeX is a collection of {\LaTeX} packages that allow to markup documents semantically + without leaving the document format. + + Running `pdflatex` over sTeX-annotated documents formats them into normal-looking + PDF. But sTeX also comes with a conversion pipeline into semantically annotated HTML5, + which can host semantic added-value services that make the documents active + (i.e. interactive and user-adaptive) and essentially turning {\LaTeX} into a document + format for (mathematical) knowledge management (MKM). \sTeX augments {\LaTeX} with \begin{itemize} - \item \emph{Semantic macros} that denote and distinguish between mathematical concepts, operators, etc. independent of their notational presentation, - \item A powerful \emph{module system} that allows for authoring and importing individual fragments containing document text and/or semantic macros, independent of -- and without hard coding -- directory paths relative to the current document, - \item A mechanism for exporting \sTeX documents to (modular) XHTML, preserving all the semantic information for semantically informed knowledge management services. + \item \emph{semantic macros} that denote and distinguish between mathematical concepts, + operators, etc. independent of their notational presentation, + \item a powerful \emph{module system} that allows for authoring and importing individual + fragments containing document text and/or semantic macros, independent of -- and + without hard coding -- directory paths relative to the current document, and + \item a mechanism for exporting \sTeX documents to (modular) XHTML, preserving all the + semantic information for semantically informed knowledge management services. \end{itemize} \end{abstract} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "stex-manual" +%%% End: diff --git a/Master/texmf-dist/doc/latex/stex/stex-doc.pdf b/Master/texmf-dist/doc/latex/stex/stex-doc.pdf Binary files differindex 7499111fa86..0d0a36720cb 100644 --- a/Master/texmf-dist/doc/latex/stex/stex-doc.pdf +++ b/Master/texmf-dist/doc/latex/stex/stex-doc.pdf diff --git a/Master/texmf-dist/doc/latex/stex/stex-doc.tex b/Master/texmf-dist/doc/latex/stex/stex-doc.tex index d2e82390837..7a98ff49c2b 100644 --- a/Master/texmf-dist/doc/latex/stex/stex-doc.tex +++ b/Master/texmf-dist/doc/latex/stex/stex-doc.tex @@ -1,4 +1,4 @@ -\def\bibfolder{../lib/bib} +\def\bibfolder#1{../lib/bib/#1} \input{stex-docheader} \infulldoctrue @@ -7,14 +7,13 @@ \clist_gput_right:Nn \g_docinput_clist { #1 } } -\bool_set_true:N \stex_dtx_tests_bool \ExplSyntaxOff \expandafter\newif\csname if@infulldoc\expandafter\endcsname\csname @infulldoctrue\endcsname \begin{document} \title{ - The {\stex{3}} Package + The {\stex{3}} Package Collection \thanks{Version {\fileversion} (last revised {\filedate})} } \author{Michael Kohlhase, Dennis Müller\\ @@ -207,4 +206,12 @@ \DocInputAgain +\begin{sfragment}{References}\ednote{we need an un-numbered version {sfragment*}} + \printbibliography[heading=none] +\end{sfragment} \end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/Master/texmf-dist/doc/latex/stex/stex-docheader.tex b/Master/texmf-dist/doc/latex/stex/stex-docheader.tex index d0f13e90b33..d16b19703bd 100644 --- a/Master/texmf-dist/doc/latex/stex/stex-docheader.tex +++ b/Master/texmf-dist/doc/latex/stex/stex-docheader.tex @@ -7,14 +7,15 @@ \RequirePackage{tikzinput} \usetikzlibrary{fit} -\usepackage[debug=all,lang=en, mathhub=./tests]{stex} +% \usepackage[debug=all,lang=en, mathhub=./tests]{stex} +\usepackage[lang=en, mathhub=./tests]{stex} \usepackage{url,array,float,textcomp} \usepackage[show]{ed} \usepackage[hyperref=auto,style=alphabetic]{biblatex} -\addbibresource{\bibfolder/kwarcpubs.bib} -\addbibresource{\bibfolder/extpubs.bib} -\addbibresource{\bibfolder/kwarccrossrefs.bib} -\addbibresource{\bibfolder/extcrossrefs.bib} +\addbibresource{\bibfolder{kwarcpubs.bib}} +\addbibresource{\bibfolder{extpubs.bib}} +\addbibresource{\bibfolder{kwarccrossrefs.bib}} +\addbibresource{\bibfolder{extcrossrefs.bib}} \usepackage{amssymb} \usepackage{amsfonts} \usepackage{xspace} @@ -26,73 +27,121 @@ \floatname{exfig}{Example} \usepackage{listings} - -\ExplSyntaxOn - -\keys_define:nn { stex-tests } { - do .bool_set:N = \stex_dtx_tests_bool -} - -\ProcessKeysOptions { stex-tests } - -\prg_new_conditional:Nnn \stex_indtx: { T } { - \bool_if:NTF \stex_dtx_tests_bool - \prg_return_true: \prg_return_false: +\usepackage{lststex} + +\lstdefinelanguage{sTeX}{ + sensitive=true, + numbers=left, + numbersep=3pt, + xleftmargin=3pt, + alsodigit={\$}, + %gobble=4, + alsoletter={\\}, + %moredelim = [s][\itshape]{$}{$}, + %moredelim = [s][\itshape\bfseries]{\\[}{\\]}, + classoffset=0,keywordstyle=\bfseries,morekeywords={ + \\begin,\\end,\\ExplSyntaxOn,\\ExplSyntaxOff,\\documentclass, + \\usepackage,\\def,\\[,\\],\\else,\\fi,$\iffalse$\fi, + \\newcommand, \\renewcommand, \\let + }, + classoffset=1,keywordstyle=\itshape\color{OliveGreen},morekeywords={ + \\defeq,\\geometricSeries,\\infinitesum,\\realdivide, + \\realpower, + \\symbolname,\\binarysymbol,\\newbinarysymbol,\\addition, + \\summation,\\ascendingchain,\\quantforall,\\set,\\funtype, + \\Nat,\\successor,\\multiplication,\\Int,\\zero,\\uminus, + \\intmonoid + }, + classoffset=2,keywordstyle=\color{blue},morekeywords={ + \\symdecl,\\symdef,\\notation,\\vardef,\\varseq,\\instantiate, + \\varinstantiate, \\renamedecl, \\assign, \\setnotation, + \\STEXexport + }, + classoffset=3,keywordstyle=\color{BurntOrange},morekeywords={ + \\importmodule,\\usemodule,\\libinput,\\inputref,\\mhinput, + \\libusepackage,\\addmhbibresource,\\ifinputref + }, + classoffset=4,keywordstyle=\color{Purple},morekeywords={ + \\definiendum,\\definame,\\symref,\\symname,\\comp, + \\compemph,\\definiens,\\svar,\\infprec,\\neginfprec,\\ellipses, + \\Symname,\\arg + }, + classoffset=5,keywordstyle=\color{magenta},morekeywords={ + smodule,sdefinition,sassertion,sparagraph,sexample, + sproof,subproof,spfcases,spfcase,spfstep,spfcomment, + \\spfidea,\\spfsketch,\\spfcasesketch,\\sproofend, + \\spfjust,\\premise,\\justarg, + copymodule,interpretmodule,mathstructure,sexample + }, + classoffset=6,keywordstyle=\color{cyan},morekeywords={ + sfragment,blindfragment,\\skipfragment, + \\currentsectionlevel,\\Currentsectionlevel + \\prematurestop,\\afterprematurestop, + \\setSGvar,\\useSGvar,\\ifSGvar + }, + classoffset=7,keywordstyle=\color{brown},morekeywords={ + frame,note,\\ifnotes,\\setslidelogo,\\setsource,\\setlicensing + slides,notes,sectocframes,frameimages,fiboxed, + nparagraph, nparagraph, ndefinition, nexample, nsproof, nassertion, + \\frameimage,\\mhframeimage,\\textwarning, + \\activateexcursion,\\printexcursion,\\excursionref,\\excursiongroup + }, + classoffset=8,keywordstyle=\color{red},morekeywords={ + frame,note + } } -\ExplSyntaxOff - -\lstdefinestyle{mylatex}{ - keywordstyle=\color{BurntOrange} -} -\lstdefinelanguage{mylatex}{ - emphstyle=\underbar, - alsodigit={:}, - %alsoletter={_}, - alsoletter={\\} - sensitive=true, - classoffset=0,keywordstyle=\bfseries, - morekeywords={\\begin,\\end,\\ExplSyntaxOn,\\ExplSyntaxOff}, - classoffset=1,keywordstyle=\color{blue}, - morekeywords={ - \\symdecl, - \\symdef, - \\notation, - \\abbrdef, - \\importmodule, - \\usemodule, - \\STEXwithbrackets, - \\symref - }, - classoffset=2,keywordstyle=\color{Purple}, - morekeywords={ - \\stex_path_from_string:Nn, - \\stex_path_to_string:NN, - \\stex_path_to_string:N, - \\stex_require_repository:n, - \\stex_modules_current_namespace:, - \\stex_debug:n, - \\stex_set_current_repository:n, - \\stex_file_in_smsmode:nn, - \\stex_get_symbol:n, - }, - classoffset=3,keywordstyle=\color{SkyBlue}, - morekeywords={ - \\l_stex_modules_ns_str, - \\g_stex_currentfile_seq, - \\l_stex_current_module_prop, - \\l_stex_get_symbol_uri_str, - } - classoffset=0, -%^^A morecomment=[l][\color{Gray}]{//}, -%^^A morecomment=[s][\color{Gray}]{/*}{*/}, - morecomment=[s][\color{Green}]{$}{$},, - morecomment=[s][\color{OliveGreen}]{\\[}{\\]}, +%\lstdefinestyle{mylatex}{ +% keywordstyle=\color{BurntOrange} +%} +%\lstdefinelanguage{mylatex}{ +% emphstyle=\underbar, +% alsodigit={:}, +% %alsoletter={_}, +% alsoletter={\\} +% sensitive=true, +% classoffset=0,keywordstyle=\bfseries, +% morekeywords={\\begin,\\end,\\ExplSyntaxOn,\\ExplSyntaxOff}, +% classoffset=1,keywordstyle=\color{blue}, +% morekeywords={ +% \\symdecl, +% \\symdef, +% \\notation, +% \\abbrdef, +% \\importmodule, +% \\usemodule, +% \\STEXwithbrackets, +% \\symref +% }, +% classoffset=2,keywordstyle=\color{Purple}, +% morekeywords={ +% \\stex_path_from_string:Nn, +% \\stex_path_to_string:NN, +% \\stex_path_to_string:N, +% \\stex_require_repository:n, +% \\stex_modules_current_namespace:, +% \\stex_debug:n, +% \\stex_set_current_repository:n, +% \\stex_file_in_smsmode:nn, +% \\stex_get_symbol:n, +% }, +% classoffset=3,keywordstyle=\color{SkyBlue}, +% morekeywords={ +% \\l_stex_module_ns_str, +% \\g_stex_currentfile_seq, +% \\l_stex_current_module_prop, +% \\l_stex_get_symbol_uri_str, +% } +% classoffset=0, +%%^^A morecomment=[l][\color{Gray}]{//}, +%%^^A morecomment=[s][\color{Gray}]{/*}{*/}, +% morecomment=[s][\color{Green}]{$}{$},, +% morecomment=[s][\color{OliveGreen}]{\\[}{\\]}, %^^A morestring=[b][\color{Purple}]\$, -} -\lstnewenvironment{latexcode}[1][language=mylatex]{\lstset{language=mylatex,basicstyle=\tiny,inputencoding=utf8,#1,alsoletter={\\,*},alsoother={\$}}}{} - +%} +\lstnewenvironment{latexcode}[1][]{\lstset{language=sTeX,#1}}{} +\def\stexcode{\lstinline[language=sTeX]} \usepackage{mdframed,realboxes} \usepackage[most]{tcolorbox} @@ -103,13 +152,13 @@ \newenvironment{stextest@output} { - \begin{mdframed}[linewidth=1pt,backgroundcolor=white]\tiny + \begin{mdframed}[linewidth=1pt,backgroundcolor=white]\small } {\end{mdframed}} \newenvironment{stextest@input} { - \begin{mdframed}[linewidth=1pt,backgroundcolor=lightgray]\tiny + \begin{mdframed}[linewidth=1pt,backgroundcolor=white]\small } {\end{mdframed}} @@ -118,47 +167,49 @@ \newcount\test@counter\test@counter=0 \newcount\example@counter\example@counter=0 -\newenvironment{stextest@border} -{ - \global\advance\test@counter by 1 - \newtcolorbox{stextestborderbox}{ - empty, - title={Test \the\test@counter}, - attach boxed title to top left, - minipage boxed title, - boxed title style={empty,size=minimal,toprule=0pt,top=4pt,left=3mm,overlay={}}, - coltitle=red,fonttitle=\bfseries, - before=\par\medskip\noindent,parbox=false,boxsep=0pt,left=3mm,right=0mm,top=2pt,breakable,pad at break=0mm, - before upper=\csname @totalleftmargin\endcsname0pt, - overlay unbroken={\draw[red,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); }, - overlay first={\draw[red,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); }, - overlay middle={\draw[red,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); }, - overlay last={\draw[red,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); }, - } -%^^A\refstepcounter{remark} -\begin{stextestborderbox}\small +\newtcolorbox{exampleborderbox}{ + empty, + title={Example \the\example@counter}, + attach boxed title to top left, + minipage boxed title, + boxed title style={empty,size=minimal,toprule=0pt,top=1pt,left=3mm,overlay={}}, + coltitle=blue,fonttitle=\bfseries, + parbox=false,boxsep=0pt,left=3mm,right=0mm,top=2pt,breakable,pad at break=0mm, + before upper=\csname @totalleftmargin\endcsname0pt, + overlay unbroken={\draw[blue,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); }, + overlay first={\draw[blue,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); }, + overlay middle={\draw[blue,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); }, + overlay last={\draw[blue,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); }, + outer arc=4pt } -{\end{stextestborderbox}} + + +%\newtcolorbox{exampleborderbox}{ +% enhanced, +% left=0pt, +% title={Example \the\example@counter}, +% right=0pt, +% top=8pt, +% bottom=8pt, +% colback=white, +% colframe=blue, +% width=\textwidth, +% enlarge left by=0mm, +% boxsep=5pt, +% fontupper=\small, +% arc=4pt, +% outer arc=4pt, +% leftupper=1.5cm, +% fonttitle=\bfseries, +% coltitle=blue, +% boxed title style={empty,size=minimal,toprule=0pt,top=1pt,left=3mm,overlay={}}, +%} \newenvironment{example@border} { \global\advance\example@counter by 1 - \newtcolorbox{exampleborderbox}{ - empty, - title={Example \the\example@counter}, - attach boxed title to top left, - minipage boxed title, - boxed title style={empty,size=minimal,toprule=0pt,top=1pt,left=3mm,overlay={}}, - coltitle=blue,fonttitle=\bfseries, - parbox=false,boxsep=0pt,left=3mm,right=0mm,top=2pt,breakable,pad at break=0mm, - before upper=\csname @totalleftmargin\endcsname0pt, - overlay unbroken={\draw[blue,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); }, - overlay first={\draw[blue,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); }, - overlay middle={\draw[blue,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); }, - overlay last={\draw[blue,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); }, - } %^^A\refstepcounter{remark} -\begin{exampleborderbox}\small +\begin{exampleborderbox} } {\end{exampleborderbox}} @@ -172,97 +223,134 @@ \ExplSyntaxOn -\AddToHook{begindocument}{ - \stex_indtx:T { - \newwrite\alltestsoutfile - \immediate\openout\alltestsoutfile=alltests.tst - } -} - - \def\stextest{ - \begingroup - \catcode`\\=12\relax - \catcode`\#=12\relax - \catcode`\&=12\relax - \catcode`\$=12\relax - \catcode`\^=12\relax - \catcode`\_=12\relax - \catcode`^^J=12\relax - \endlinechar=`^^J - \newlinechar=-1 +\def\stexexample{ + \begingroup + \catcode`\\=12\relax + \catcode`\#=12\relax + \catcode`\&=12\relax + \catcode`\$=12\relax + \catcode`\^=12\relax + \catcode`\_=12\relax + \catcode`\ =12\relax + \catcode`^^J=12\relax + \endlinechar=`^^J + \newlinechar=-1 %^^A \everyeof{\noexpand} - \test_a:n - } - \long\def \test_a:n #1 { - \endgroup - \stex_indtx:T { - \immediate\write\alltestsoutfile{% - ^^J\c_backslash_str stextest{\detokenize{^^J^^J#1^^J}}^^J - } + \example_a:n +} +\long\def\example_a:n #1 { + \endgroup + \begin{example@border} + \immediate\openout\testoutfile=stextest.tex + \immediate\write\testoutfile{ + \c_backslash_str begin{latexcode} + \detokenize{^^J}#1 + \c_backslash_str end{latexcode} } - \begin{stextest@border} - \immediate\openout\testoutfile=stextest.tst - \immediate\write\testoutfile{ - \c_backslash_str begin{latexcode} - \detokenize{^^J^^J#1^^J} - \c_backslash_str end{latexcode} - } - \immediate\closeout\testoutfile - \begin{stextest@input} - \catcode`\#=12\relax - \input{stextest.tst} - \end{stextest@input} - \immediate\openout\testoutfile=stextest.tst - \immediate\write\testoutfile{\detokenize{#1}} - \immediate\closeout\testoutfile - \stex_indtx:T { - \begin{stextest@output} - \input{stextest.tst} - \end{stextest@output} - } - \end{stextest@border} - } + \immediate\closeout\testoutfile + + Input: + + \begin{stextest@input} + \catcode`\#=12\relax + \input{stextest.tex} + \end{stextest@input} + \immediate\openout\testoutfile=stextest.tex + \immediate\write\testoutfile{#1} + \immediate\closeout\testoutfile + + Output: + + \begin{stextest@output} + \input{stextest.tex} + \end{stextest@output} + \end{example@border} +} - \def\stexexample{ - \begingroup - \catcode`\\=12\relax - \catcode`\#=12\relax - \catcode`\&=12\relax - \catcode`\$=12\relax - \catcode`\^=12\relax - \catcode`\_=12\relax - \catcode`^^J=12\relax - \endlinechar=`^^J - \newlinechar=-1 -%^^A \everyeof{\noexpand} - \example_a:n - } - \long\def \example_a:n #1 { - \endgroup - \begin{example@border} - \immediate\openout\testoutfile=stextest.tst - \immediate\write\testoutfile{ - \c_backslash_str begin{latexcode} - \detokenize{^^J}#1 - \c_backslash_str end{latexcode} - } - \immediate\closeout\testoutfile - \begin{stextest@input} - \catcode`\#=12\relax - \input{stextest.tst} - \end{stextest@input} - \immediate\openout\testoutfile=stextest.tst - \immediate\write\testoutfile{#1} - \immediate\closeout\testoutfile - \begin{stextest@output} - \input{stextest.tst} - \end{stextest@output} - \end{example@border} - } +\ExplSyntaxOff - \long\def\test#1{} +\def\textwarning{\includegraphics[width=1.2em]{stex-dangerous-bend}\xspace} +\newtcolorbox{dangerbox}{ + breakable, + enhanced, + left=0pt, + right=0pt, + top=8pt, + bottom=8pt, + colback=white, + colframe=red, + width=\textwidth, + enlarge left by=0mm, + boxsep=5pt, + fontupper=\small, + arc=4pt, + outer arc=4pt, + leftupper=1.5cm, + overlay={ + \node[anchor=west] at ([xshift=10pt]$(frame.north west)!0.5!(frame.south west)$) + {\includegraphics[width=1cm,height=1cm]{stex-dangerous-bend}};} +} -\ExplSyntaxOff +\usetikzlibrary{decorations.pathmorphing,shapes,arrows,calc} +% Taken from pgflibrarytikzmmt.code.tex +\newcommand{\mmtarrowtip}{angle 45} +\newcommand{\mmtarrowtipmonoright}{right hook} + +\tikzstyle{include}=[\mmtarrowtipmonoright-\mmtarrowtip,thick] +\tikzstyle{morph}=[-\mmtarrowtip,thick] +\tikzstyle{preview}=[decorate, decoration={coil,aspect=0,amplitude=1pt, + segment length=6pt, + pre=lineto,pre length=3pt, + post=lineto,post length=5pt}, thick] +\tikzstyle{view}=[preview,-\mmtarrowtip] + +% TIKZ RULES +\def\mmtlogo{ +\begin{tikzpicture} + + % White Background (Margins are eyeballed) + % This is necessary because we paste white over arrows later. + % If somebody want's to do the full song and dance with + % interrupted arrows to get transparent background, be my guest. + + \fill[white!] (-0.01,0.15) rectangle (1.11,-0.95); + + % Arrows + \draw [blue, include] (0,0) -- (1.1,0); + \draw [green, morph] (0,-0.4) -- (1.1,-0.4); + \draw [red, view] (-0,-0.8) -- (1.1,-0.8); + + % Cutout for letters + \fill[white] (0.33,0.1) rectangle (0.66,-0.9); + + % Letters + \node at (0.18,0) (nodeM1) {\large M}; + \node at (0.18,-0.4) (nodeM2) {\large M}; + \node at (0.21,-0.8) (nodeT) {\large T}; + +\end{tikzpicture} +} + +\newtcolorbox{mmtbox}{ + breakable, + enhanced, + left=0pt, + right=0pt, + top=8pt, + bottom=8pt, + colback=white, + colframe=green, + width=\textwidth, + enlarge left by=0mm, + boxsep=5pt, + fontupper=\small, + arc=4pt, + outer arc=4pt, + leftupper=1.5cm, + overlay={ + \node[anchor=west] at ([xshift=10pt]$(frame.north west)!0.5!(frame.south west)$) + {\mmtlogo};} +} \MakeShortVerb{\|} @@ -283,7 +371,7 @@ \def\atwintoo#1#2#3{{#1 #2 #3}\atwin{#1}{#2}{#3}} \def\cT{\mathcal{T}}\def\cD{\mathcal{D}} -\def\fileversion{3.0} +\def\fileversion{3.1} \def\filedate{\today} \RequirePackage{pdfcomment} @@ -322,7 +410,7 @@ \newif\ifinfulldoc\infulldocfalse \makeatother -\def\basedocurl{https://github.com/slatex/sTeX/blob/latex3/doc} +\def\basedocurl{https://github.com/slatex/sTeX/blob/main/doc} \newcounter{module} \NewDocumentEnvironment {module}{}{ @@ -331,25 +419,31 @@ }{ } -\stexpatchmodule{\begin{module}}{\end{module}} - -\def\compemph#1{\textcolor{blue}{#1}} -\def\symrefemph#1{\textcolor{green}{#1}} - -\RequirePackage{pdfcomment} -\makeatletter -\protected\def\compemph@uri#1#2{% - \pdftooltip{% - \srefsymuri{#2}{\compemph{#1}}% - }{% - URI: \detokenize{#2}% - }% +\stexpatchmodule[visible]{\begin{module}}{\end{module}} + +\usepackage{stexthm} + + +\newtcolorbox{remarkbox}[1][]{ + empty, + title={Remark \theremark: #1}, + attach boxed title to top left, + minipage boxed title, + boxed title style={empty,size=minimal,toprule=0pt,top=4pt,left=3mm,overlay={}}, + fonttitle=\bfseries,coltitle=black, + before=\par\medskip\noindent,parbox=false,boxsep=0pt,left=3mm,right=0mm,top=2pt,breakable,pad at break=0mm, + before upper=\csname @totalleftmargin\endcsname0pt, + overlay unbroken={\draw[black,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); }, + overlay first={\draw[black,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); }, + overlay middle={\draw[black,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); }, + overlay last={\draw[black,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); }, } -\protected\def\symrefemph@uri#1#2{% - \pdftooltip{% - \srefsymuri{#2}{\symrefemph{#1}}% - }{% - URI: \detokenize{#2}% - }% + +\renewenvironment{remark}[1][]{ + \refstepcounter{remark}\begin{remarkbox}[#1] + \begin{mdframed}[linewidth=1pt,backgroundcolor=lightgray!33!white] +}{ +\end{mdframed}\end{remarkbox}\endlist } -\makeatother
\ No newline at end of file + +\usepackage{rustex} diff --git a/Master/texmf-dist/doc/latex/stex/stex-manual.pdf b/Master/texmf-dist/doc/latex/stex/stex-manual.pdf Binary files differindex 80b4154b9af..32c1e047ca5 100644 --- a/Master/texmf-dist/doc/latex/stex/stex-manual.pdf +++ b/Master/texmf-dist/doc/latex/stex/stex-manual.pdf diff --git a/Master/texmf-dist/doc/latex/stex/stex-manual.tex b/Master/texmf-dist/doc/latex/stex/stex-manual.tex index 92834af1c5e..31b9c4eaeb2 100644 --- a/Master/texmf-dist/doc/latex/stex/stex-manual.tex +++ b/Master/texmf-dist/doc/latex/stex/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 diff --git a/Master/texmf-dist/doc/latex/stex/stex-tutorial.tex b/Master/texmf-dist/doc/latex/stex/stex-tutorial.tex new file mode 100644 index 00000000000..dcd4c442e00 --- /dev/null +++ b/Master/texmf-dist/doc/latex/stex/stex-tutorial.tex @@ -0,0 +1,354 @@ + \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, + and write a small fragment defining the \emph{geometric series}: + + % \textcolor{red}{TODO: use some sTeX-archive instead of smglom, + % use a convergence-notion that includes the limit, + % mark-up the theorem properly} + + \begin{framed}\begin{latexcode}[gobble=8] + \documentclass{article} + \usepackage{stex,xcolor,stexthm} + + \begin{document} + \begin{smodule}{GeometricSeries} + \importmodule[smglom/calculus]{series} + \importmodule[smglom/arithmetics]{realarith} + + \symdef{geometricSeries}[name=geometric-series]{\comp{S}} + + \begin{sdefinition}[for=geometricSeries] + The \definame{geometricSeries} is the \symname{?series} + \[\defeq{\geometricSeries}{\definiens{ + \infinitesum{\svar{n}}{1}{ + \realdivide[frac]{1}{ + \realpower{2}{\svar{n}} + }} + }}.\] + \end{sdefinition} + + \begin{sassertion}[name=geometricSeriesConverges,type=theorem] + The \symname{geometricSeries} \symname{converges} towards $1$. + \end{sassertion} + \end{smodule} + \end{document} + \end{latexcode}\end{framed} + + Compiling this document with |pdflatex| should yield + the output + + \begin{mdframed} + \noindent\textbf{Definition 0.1. }\ The + \pdftooltip{\textcolor{blue}{\textbf{geometric series}}}{URI: file://your/file/name/here?GeometricSeries?geometric-series} + is the + \pdftooltip{\textcolor{blue}{series}}{URI: http://mathhub.info/smglom/calculus?series?series} + \[ + \pdftooltip{\textcolor{blue}S}{URI: file://your/file/name/here?GeometricSeries?geometric-series} + \pdftooltip{\textcolor{blue}{:=}}{URI: http://mathhub.info/smglom/mv?defeq?definitional-equation} + \mathop{\pdftooltip{\textcolor{blue}{\sum}}{URI: http://mathhub.info/smglom/calculus?series?infinitesum} + }_{ + \pdftooltip{\textcolor{gray}{n}}{Variable var://n}=1 + }^{ + \pdftooltip{\textcolor{blue}\infty}{URI: http://mathhub.info/smglom/calculus?series?infinitesum} + } \frac{1}{2^{\pdftooltip{\textcolor{gray}{n}}{Variable var://n}}} + .\] + \noindent\textbf{Theorem 0.2. }\ The + \pdftooltip{\textcolor{blue}{geometric series}}{URI: file://your/file/name/here?GeometricSeries?geometric-series} + \pdftooltip{\textcolor{blue}{converges}}{URI: http://mathhub.info/smglom/calculus?sequenceConvergence?converges} towards $1$. + \end{mdframed} + + Move your cursor over the various highlighted parts of the document -- depending on + your pdf viewer, this should yield some interesting (but possibly for now cryptic) + information. + + \begin{sparagraph}[type=remark] + Note that all of the highlighting, tooltips, coloring and the environment headers + come from \pkg{stexthm} -- by default, the amount of additional packages loaded + is kept to a minimum and all the presentations can be customized, + see \sref{sec.customhighlight}. + \end{sparagraph} + + Let's investigate this document in detail to understand the respective parts of the + \sTeX markup infrastructure:\bigskip + + \begin{environment}{smodule} + \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=8] + \begin{smodule}{GeometricSeries} + ... + \end{smodule} + \end{latexcode} + First, we open a new \emph{module} called |GeometricSeries|. The main purpose of + the |smodule| environment is to group the contents and associate it with a + \emph{globally unique} identifier (URI), which is computed from the name + |GeometricSeries| and the document context. + + (Depending on your pdf viewer), the URI should pop up in a tooltip if you hover over + the word \pdftooltip{\textcolor{blue}{\textbf{geometric series}}}{URI: + file://your/file/name/here?GeometricSeries?geometric-series}. + \end{environment}\bigskip + + \begin{function}{\importmodule} + \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=8] + \importmodule[smglom/calculus]{series} + \importmodule[smglom/arithmetics]{realarith} + \end{latexcode} + Next, we \emph{import} two modules -- |series| from the \sTeX archive + |smglom/calculus|, and |realarith| from the \sTeX archive |smglom/arithmetics|. If + we investigate these archives, we find the files |series.en.tex| and + |realarith.en.tex| (respectively) in their respective |source|-folders, which + contain the statements \stexcode"\begin{smodule}{series}" and + \stexcode"\begin{smodule}{realarith}" (respectively). + \iffalse\end{smodule}\end{smodule}\fi + + The \stexcode"\importmodule"-statements make all \stex symbols and associated + semantic macros (e.g. \stexcode"\infinitesum", \stexcode"\realdivide", + \stexcode"\realpower") in the imported module available to the current module + |GeometricSeries|. The module |GeometricSeries| ``exports'' all of these symbols to + all modules imports it via an \stexcode"\importmodule{GeometricSeries}" + instruction. Additionally it exports the local symbol \stexcode"\geometricSeries". + \end{function} + + \begin{function}{\usemodule} + If we only want to \emph{use} the content of some module |Foo|, + e.g. in remarks or examples, but none + of the symbols in our current module actually \emph{depend} on + the content of |Foo|, we can use \stexcode"\usemodule" instead -- like + \stexcode"\importmodule", this will make the module content available, + but will \emph{not} export it to other modules. + \end{function}\bigskip + + \begin{function}{\symdef} + \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=6] + \symdef{GeometricSeries}[name=geometric-series]{\comp{S}} + \end{latexcode} + Next, we introduce a new \emph{symbol} with name + |geometric-series| and assign it the semantic macro + \stexcode"\geometricSeries". + \stexcode"\symdef" also immediately assigns this symbol a \emph{notation}, + namely $S$. + \end{function} + + \begin{function}{\comp} + The macro \stexcode"\comp" marks the $S$ in the notation as a + \emph{notational component}, as opposed to e.g. arguments + to \stexcode"\geometricSeries". + It is the notational components that get highlighted + and associated with the corresponding symbol (i.e. in this + case |geometricSeries|). Since \stexcode"\geometricSeries" takes + no arguments, we can wrap the whole notation in a \stexcode"\comp". + \end{function}\bigskip + + \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=8] + \begin{sdefinition}[for=geometricSeries] + ... + \end{sdefinition} + \begin{sassertion}[name=geometricSeriesConverges,type=theorem] + ... + \end{sassertion} + \end{latexcode} + What follows are two \sTeX-\emph{statements} (e.g. definitions, + theorems, examples, proofs, ...). These are semantically marked-up + variants of the usual environments, which take additional optional + arguments (e.g. |for=|, |type=|, |name=|). Since many \LaTeX\xspace templates + predefine environments like |definition| or |theorem| with + different syntax, we use \stexcode"sdefinition", + \stexcode"sassertion", \stexcode"sexample" + etc. instead. You can customize these environments to e.g. + simply wrap around some predefined |theorem|-environment. + That way, we can still use \stexcode"sassertion" to provide semantic + information, while being fully compatible with (and using + the document presentation of) predefined environments. + + In our case, the \pkg{stexthm}-package patches + e.g. \stexcode"\begin{sassertion}[type=theorem]" to use + a |theorem|-environment defined (as usual) using the \pkg{amsthm} package. + \bigskip \iffalse \end{sassertion}\fi + + \begin{function}{\symname} + \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=6] + ... is the \symname{?series} + \end{latexcode} + The \stexcode"\symname"-command prints the name of a symbol, + highlights it (based on customizable settings) + and associates the text printed with the corresponding + symbol. + + Note that the argument of \stexcode"\symref" can be + an imported symbol + (here the |series| symbol is imported from the |series| module). \sTeX tries to + determine the full symbol URI from the argument. If there are name clashes in or + with the imported symbols, the name of the exporting module can be prepended to the + symbol name before the |?| character. + + If you hover over the word + \pdftooltip{\textcolor{blue}{series}}{URI: http://mathhub.info/smglom/calculus?series?series} + in the pdf output, you should see a tooltip showing the full URI + of the symbol used. + \end{function} + \begin{function}{\symref} + The \stexcode"\symname"-command is a special case of the more general + \stexcode"\symref"-command, which allows customizing the precise text associated + with a symbol. \stexcode"\symref" takes two arguments: the first ist the symbol + name (or macro name), and the second a variant verbalization of the symbol, e.g. an inflection + variant, a different language or a synonym. In our example + \stexcode"\symname{?series}" abbreviates \stexcode|\symref{?series}{series}|. + + \end{function} + \begin{function}{\definame,\definiendum} + \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=6] + The \definame{geometricSeries} ... + \end{latexcode} + The \stexcode"sdefinition"-environment provides two additional + macros, \stexcode"\definame" and \stexcode"\definiendum" which behave + similarly to \stexcode"\symname" and \stexcode"\symref", but explicitly mark + the symbols as \emph{being defined} in this environment, + to allow for special highlighting. + \end{function}\bigskip + + \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=8] + \[\defeq{\geometricSeries}{\definiens{ + \infinitesum{\svar{n}}{1}{ + \realdivide[frac]{1}{ + \realpower{2}{\svar{n}} + }} + }}.\] + \end{latexcode} + The next snippet -- set in a math environment -- uses + several semantic macros imported from (or recursively via) + |series| and |realarithmetics|, such as \stexcode"\defeq", + \stexcode"\infinitesum", + etc. In math mode, using a semantic macro inserts its (default) + definition. A semantic macro can have several notations -- in + that case, we can explicitly choose a specific notation by + providing its identifier as an optional argument; e.g. + \stexcode"\realdivide[frac]{a}{b}" will use the explicit notation named |frac| + of the semantic macro \stexcode"\realdivide", which yields $\frac ab$ + instead of $a/b$. + \begin{function}{\svar} + The \stexcode"\svar{n}" command marks up the |n| as a variable + with name |n| and notation |n|. + \end{function} + \begin{function}{\definiens} + The \stexcode"sdefinition"-environment additionally provides the + \stexcode"\definiens"-command, which allows for explicitly + marking up its argument as the \emph{definiens} of the + symbol currently being defined. + \end{function} + + \begin{sfragment}{\omdoc/xhtml Conversion} + So, if we run |pdflatex| on our document, then \sTeX yields pretty colors and + tooltips\footnote{...and hyperlinks for symbols, and indices, and allows reusing + document fragments modularly, and...}. But \sTeX becomes a lot more powerful if + we additionally convert our document to |xhtml| while preserving all the \sTeX + markup in the result. + + \textcolor{red}{TODO VSCode Plugin} + + Using \rustex \cite{RusTeX:on}, we can convert the document to |xhtml| + using the command |rustex -i /path/to/file.tex -o /path/to/outfile.xhtml|. + Investigating the resulting file, we notice additional semantic + information resulting from our usage of semantic macros, + \stexcode"\symref" etc. Below is the (abbreviated) snippet inside + our \stexcode"\definiens" block: + +\begin{lstlisting}[escapechar=!, +morekeywords={property,resource,stex:comp,stex:arg,stex:OMA,stex:OMV}] +<mrow resource="" property="stex:definiens"> + <mrow resource="...?series?infinitesum" property="stex:OMBIND"> + <munderover displaystyle="true"> + <mo resource="...?series?infinitesum" property="stex:comp">!$\Sigma$!</mo> + <mrow> + <mrow resource="1" property="stex:arg"> + <mi resource="var://n" property="stex:OMV">n</mi> + </mrow> + <mo resource="...?series?infinitesum" property="stex:comp">=</mo> + <mi resource="2" property="stex:arg">1</mi> + </mrow> + <mi resource="...?series?infinitesum" property="stex:comp">!$\infty$!</mi> + </munderover> + <mrow resource="3" property="stex:arg"> + <mfrac resource="...?realarith?division#frac#" property="stex:OMA"> + <mi resource="1" property="stex:arg">1</mi> + <mrow resource="2" property="stex:arg"> + <msup resource="...realarith?exponentiation" property="stex:OMA"> + <mi resource="1" property="stex:arg">2</mi> + <mrow resource="2" property="stex:arg"> + <mi resource="var://n" property="stex:OMV">n</mi> + </mrow> + </msup> + </mrow> + </mfrac> + </mrow> + </mrow> +</mrow> + \end{lstlisting} + ...containing all the semantic information. The \mmt system + can extract from this the following \openmath snippet: + + \begin{lstlisting}[escapechar=!] +<OMBIND> + <OMID name="...?series?infinitesum"/> + <OMV name="n"/> + <OMLIT name="1"/> + <OMA> + <OMS name="...?realarith?division"/> + <OMLIT name="1"/> + <OMA> + <OMS name="...realarith?exponentiation"/> + <OMLIT name="2"/> + <OMV name="n"/> + </OMA> + </OMA> +</OMBIND> + \end{lstlisting} + ...giving us the full semantics of the snippet, allowing for + a plurality of knowledge management services -- in particular + when serving the |xhtml|. + + \begin{remark} + Note that the |html| when opened in a browser will + look slightly different than the |pdf| when it comes + to highlighting semantic content -- that is because + naturally |html| allows for much more powerful + features than |pdf| does. Consequently, the |html| + is intended to be served by a system like \mmt, + which can pick up on the semantic information and + offer much more powerful highlighting, linking + and similar features, and being customizable by + \emph{readers} rather than being prescribed by an author. + + Additionally, not all browsers (most notably Chrome) + support \mathml natively, and might require + additional external JavaScript libraries such as + MathJax to render mathematical formulas properly. + \end{remark} + \end{sfragment} + + + \begin{sfragment}{\mmt/\omdoc Conversion} + Another way to convert our document to \emph{actual} + \mmt/\omdoc is to put it in an \sTeX \textbf{archive} + (see \sref{sec.stexarchives}) and have \mmt take care of + everything. + + Assuming the above file is |source/demo.tex| in + an \sTeX archive |MyTest|, you can run \mmt and + do + |build MyTest stex-omdoc demo.tex| to convert the + document to both |xhtml| (which you will find in + |xhtml/demo.xhtml| in the archive) and formal + \mmt/\omdoc, which you can subsequently view in + the \mmt browser (see \url{https://uniformal.github.io//doc/applications/server.html#the-mmt-web-site} + for details). + \end{sfragment} +\end{sfragment} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "stex-manual" +%%% End: + +% LocalWords: coloring sec.customhighlight realarith infinitesum realarithmetics |