summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/doc/stex-manual.tex
blob: 92834af1c5e2f3ebe0779207cbd7af34327de5d8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
\makeatletter
\ifcsname if@infulldoc\endcsname\else
    \expandafter\newif\csname if@infulldoc\endcsname\@infulldocfalse
\fi
\makeatother

\csname if@infulldoc\endcsname\else

\def\bibfolder{../lib/bib}

\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{
		The {\stex{3}} Manual
		\thanks{Version {\fileversion} (last revised {\filedate})}
 	}
	\author{Michael Kohlhase, Dennis Müller\\
		FAU Erlangen-Nürnberg\\
		\url{http://kwarc.info/}
	}
	\pagenumbering{roman}
	\maketitle
	
	\input{stex-abstract}\bigskip

  This is the user manual for the \sTeX package and 
  associated software. It is primarily directed at end-users 
  who want to use \sTeX to author semantically
  enriched documents. For the full documentation, see
  \href{\basedocurl/stex.pdf}{the \sTeX documentation}
	
	\makeatletter
		\renewcommand\part{%
    		\clearpage
  			\thispagestyle{plain}%
  			\@tempswafalse
  			\null\vfil
  			\secdef\@part\@spart%
  		}
		\newcounter{chapter}
		\numberwithin{section}{chapter}
		\renewcommand\thechapter{\@arabic\c@chapter}
		\renewcommand\thesection{\thechapter.\@arabic\c@section}
		\newcommand*\chaptermark[1]{}
		\setcounter{secnumdepth}{2}
		\newcommand\@chapapp{\chaptername}
		%\newcommand\chaptername{Chapter}
  		\def\ps@headings{%
    		\let\@oddfoot\@empty
    		\def\@oddhead{{\slshape\rightmark}\hfil\thepage}%
    		\let\@mkboth\markboth
    		\def\chaptermark##1{%
      			\markright{\MakeUppercase{%
        			\ifnum \c@secnumdepth >\m@ne
            			\@chapapp\ \thechapter. \ %
        			\fi
        		##1}}%
        	}%
        }
		\newcommand\chapter{\clearpage
			\thispagestyle{plain}%
			\global\@topnum\z@
			\@afterindentfalse
			\secdef\@chapter\@schapter%
		}
		\def\@chapter[#1]#2{\refstepcounter{chapter}%
			\typeout{\@chapapp\space\thechapter.}%
			\addcontentsline{toc}{chapter}%
				{\protect\numberline{\thechapter}#1}%
			\chaptermark{#1}%
			\addtocontents{lof}{\protect\addvspace{10\p@}}%
			\addtocontents{lot}{\protect\addvspace{10\p@}}%
			\@makechapterhead{#2}%
			\@afterheading%
		}
		\def\@makechapterhead#1{%
			\vspace*{50\p@}%
			{\parindent \z@ \raggedright \normalfont
				\huge\bfseries \@chapapp\space \thechapter
				\par\nobreak
				\vskip 20\p@
				\interlinepenalty\@M
				\Huge \bfseries #1\par\nobreak
				\vskip 40\p@
			}%
		}
\newcommand*\l@chapter[2]{%
  \ifnum \c@tocdepth >\m@ne
    \addpenalty{-\@highpenalty}%
    \vskip 1.0em \@plus\p@
    \setlength\@tempdima{1.5em}%
    \begingroup
      \parindent \z@ \rightskip \@pnumwidth
      \parfillskip -\@pnumwidth
      \leavevmode \bfseries
      \advance\leftskip\@tempdima
      \hskip -\leftskip
      #1\nobreak\hfil
      \nobreak\hb@xt@\@pnumwidth{\hss #2%
                                 \kern-\p@\kern\p@}\par
      \penalty\@highpenalty
    \endgroup
  \fi}
\renewcommand*\l@section{\@dottedtocline{1}{1.5em}{2.8em}}
\renewcommand*\l@subsection{\@dottedtocline{2}{3.8em}{3.2em}}
\renewcommand*\l@subsubsection{\@dottedtocline{3}{7.0em}{4.1em}}
\def\partname{Part}
\def\toclevel@part{-1}
\def\maketitle{\chapter{\@title}}
\let\thanks\@gobble
\let\DelayPrintIndex\PrintIndex
\let\PrintIndex\@empty
\providecommand*{\hexnum}[1]{\text{\texttt{\char`\"}#1}}
\makeatother

\ExplSyntaxOn
\int_set:Nn \l_document_structure_section_level_int {1}
\ExplSyntaxOff

\clearpage

{%
  \def\\{:}% fix "newlines" in the ToC
  \tableofcontents
}

\clearpage
\pagenumbering{arabic}
	
\fi

\long\def\ignore#1{}

\begin{sfragment}{What is \sTeX?}
  
Formal systems for mathematics (such as interactive theorem provers)
have the potential to significantly increase both the accessibility
of published knowledge, as well as the confidence in its veracity,
by rendering the precise semantics of statements machine actionable.
This allows for a plurality of added-value services, from semantic
search up to verification and automated theorem proving.
Unfortunately, their usefulness is hidden behind severe barriers
to accessibility; primarily related to their surface languages
reminiscent of programming languages and very unlike informal
standards of presentation.

\sTeX minimizes this gap between informal and formal 
mathematics by integrating formal methods into established
and widespread authoring workflows, primarily \LaTeX, via 
non-intrusive semantic
annotations of arbitrary informal document fragments. That way
formal knowledge management services become available for informal
documents, accessible via an IDE for authors and via generated
\emph{active} documents for readers, while remaining fully compatible
with existing authoring workflows and publishing systems.

Additionally, an extensible library of reusable
document fragments is being developed, that serve as reference targets
for global disambiguation, intermediaries for content exchange
between systems and other services.

Every component of the system is designed modularly and extensibly,
and thus lay the groundwork for a potential full integration of
interactive theorem proving systems into established informal document
authoring workflows.

\paragraph{} The general \sTeX workflow combines functionalities
provided by several pieces of software:
\begin{itemize}
  \item The \sTeX package 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.
\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{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
          the setup routine documented 
          \href{https://uniformal.github.io//doc/setup/}{here}.

          Following the setup routine (Step 3) will entail designating
          a |MathHub|-directory on your local file system, where
          the \mmt system will look for \sTeX/\mmt content archives.

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

\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}
  \input{packages/stex-basics}
  
  \input{packages/stex-terms}

  \input{packages/stex-references}
\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}

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

  \input{packages/stex-symbols}

  \input{packages/stex-inheritance}

  \begin{sfragment}{Advanced Structuring Mechanisms}
    \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}

  \input{packages/stex-proofs}
\end{sfragment}

\begin{sfragment}{Additional Packages}
  \input{packages/stex-tikzinput}
  \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}
    \input{packages/stex-problem}
    
    \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\end{document}\fi