Develop sMarkDown, make a mock course, and add it to ALeA

[kohlhase]

Like #280, but for Markdown, we also need to develop semantic Markdown and have an extended sMarkDown2SHTML compiler. In contrast to #280 we need the build system to generate the SHTML from the sources.

Language Specification

Here is a first specification of the sMD syntax, based on sTeX examples. We want to have two levels: sMDlite (revy restricted, e.g. for ALeA blog entries that want to use ALeA concepts - e.g. from the system documentation).

sMDlite

gives three (plus maybe one) basic features that allow to reference information

• [ ] Term References: e.g.\sr{foo}{bar} is written with a prefixed link:>bar, wherebaris the link text andfoois the symbol name (this can also beFOO?foo(for disambituation) or evenhttps://mathhub.info/thefoomods?FOO?foo. For the short form\sn{foo}(of\sr{foo}{foo}we use>[foo]`.
• [ ] Input references: e.g. \inputref[arch]{path} is written as <d[path](arch) where path is a path in the local archive and arch is (optional) a name of an external archive. So the short sorm <d[path] is the "same-archive" form. Note that they can only be used for archives that already exist on the MathHub server.
• [ ] usemodule: e.g. \usemodule[arch]{path} is written as <u[path](arch) just as above. This opens the respective modules for using in term references or sTeX formulae.
• [ ] (maybe) sTeX formulae: Just use LaTeX formulae as always, just with sTeX semantic macros. A sMD transformer should use RusTeX instead of MathJax.

sMD

adds the following functionality to cover much of sTeX (a fragment that covers most non-math content).

• [ ] Statements: e.g. the sdefinition, sassertion, saxiom, sparagraph environments. E.g. \begin{sdefinition}[id=foo,title=bar,for=foobar] would be written as :::sdefinition {{id=foo,title=bar,for=foobar}} (all in one line) and \end{sdefinition} as :::. Note we generally use the {{... }} for dictionary-like metadata that sTeX annotates in optional arguments. We use double curly braces, as the values can have commata, and then we (like in LaTeX) enclose the values in {...}.
• [ ] Sectioning: e.g. \begin{sfragment}[id=foo]{The Title} is written as !# The Ti!tle {{id=foo}} (all in one line). Note that we have to deal with nesting here in the HTML transformation:

  !# First Header
  !## Frist Subheader
  !## Second Subheader
  !# Second Header

  becomes

  <div sfragment><div title>First Header</div>
  <div sfragment><div title>Frist Subheader</div></div> 
  <div sfragment><div title>Second Subheader</div></div>
  <div sfragment><div title>Second Header</div>
  ...
  </div>

  i.e. the number of hashes signifies the file-internal nesting structure which must be transformed into a nesting structure in the SHTML.

• [ ] importmodule: e.g. \importmodule[arch]{path} is written as <i[path](arch) just as above.
• [ ]

sTeX features beyond sMD

The following features are intentionally left out of sMD to make parsing and interpretation easier. In particular, we want to get around

• modules: We hard-code the one-file-one-module paradigm, so we can just pick up the module name from the file name.
• symbol definitions: the notations are too complicated --> use sTeX.
• symbol declarations: these we just pick up from the definienda.
• proofs: we would have needed nested block-level environments here.
• inline statements: we would need nesting (e.g. an inline definition in an assertion) here.

[kohlhase]

I am sitting in Bonn with Nicolas Thierry and we are discussing syntax. He has already worked on Markdown annotations for his Jupyter-based courses (he will add links). His/Our systax from last year is based on myst (https://mystmd.org/). We should take a good look at that. They seem to have extensive tooling already.

[nthiery]

Here is a (start of) blog post from after my visit last year; I followed the notations given there to annotate my course notes this year with various environments (definition, ...) and definiendum and (some) symrefs.

The course notes rendered in html (presumably shtml in fact; but I need to double check on that) are here:

• an example of annotated definition
• Its rendering

At this stage, I haven't annotated tasks with didactic metadata, by lack of a immediate benefit and schema. The natural way in MyST would be to use YAML frontends. But really the important thing is to fix a schema; and then it will be easy to swap the syntax between json/yaml or something else.