On Sunday, November 10th, 2024 at 08:20, Mikael Sundqvist
------------------------------ Hi,
On Sun, Nov 10, 2024 at 2:45 AM ntg-contextmailingli.expedited080--- via ntg-context ntg-context@ntg.nl wrote:
I'm test driving luametatex. My needs usually extend to expressing formulas in TLA+ using nested display math formulas. Although I have suitable templates for doing this in Mark IV, I can't reproduce these satisfactorily in luametatex. For example, here's a formula from Leslie Lamport's 2006 "Lower Bounds for Asynchronous Consensus":
~~~~~~~~~~~ transitive_reduction.tex ~~~~~~~~~~~~~
\define\lbr {\lbrace \mkern 0.9mu} \define\rbr {{}\mkern 0.9mu \rbrace} \define\∀ {∀\mkern1mu} \define\∃ {∃\mkern2mu}
\startdocument
\startplaceformula \startformula [split=yes, align=flushleft, margin=standard, interlinespace=1ex] \bgroup \setupinterlinespace [line=1ex] \startalign [n=1, align={left,left}]
\NC \text{\it TransitiveClosure}(R) ≜ \NR
\NC \quad \bgroup \setupinterlinespace [line=1ex] \startalign [n=2, align={left,left,left}, location=top]
\NC \text{\sc let} \quad \NC \bgroup \setupinterlinespace [line=1ex] \startalign [n=1, align={left,left}, location=top]
\NC \text{\it Dom} ≜ \lbr r[1]: r ∈ R \rbr \NR
\NC \text{\it Rng} ≜ \lbr r[2]: r ∈ R \rbr \NR
\NC \text{\it TC}[i ∈ ℕ] ≜ \NR
\NC \quad \bgroup \setupinterlinespace [line=1ex] \startalign [n=1, align={left,left}, location=top]
\NC \text{\sc if}\ i = 0\ \bgroup \setupinterlinespace [line=1ex] \startalign [n=2, align={left,left,left}, location=top]
\NC \text{\sc then}\ \NC R \NR
\NC \text{\sc else}\ \NC \bgroup \setupinterlinespace [line=1ex] \startalign [n=1, align={left,left}, location=top]
\NC \lbr 〈d, e 〉∈ \text{\it Dom} × \text{\it Rng}: \NR
\NC \quad \∃ c ∈ \text{\it Dom} ∩ \text{\it Rng}: \bgroup \setupinterlinespace [line=1ex] \startalign [n=1, align={left,left}, location=top]
\NC ∧ 〈d, c〉∈ \text{\it TC}[i-1] \NR
\NC ∧ 〈c, e〉∈ R \,\rbr \NR \stopalign \egroup \NR \stopalign \egroup \NR \stopalign \egroup \NR \stopalign \egroup \NR \stopalign \egroup \NR
\NC \text{\sc in}\ \NC \text{\sc union}\ \lbr \text{\it TC}[i] : i ∈ ℕ \rbr \NR \stopalign \egroup \NR \stopalign \egroup \stopformula \stopplaceformula
\stopdocument
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The command
$ context --luatex transitive_reduction.tex
produces the desired result, but
$ context transitive_reduction.tex
rejects the alignments and centers the lines instead. Can anyone suggest how I might adapt such nesting of alignments to luametatex?
I must admit that I don't know what is the expected output and if I did break any of the rules or missed what you want, but the following could hopefully work as a start for you:
\define\lbr {\lbrace \mkern 0.9mu} \define\rbr {{}\mkern 0.9mu \rbrace} \define\∀ {∀\mkern1mu} \define\∃ {∃\mkern2mu}
\definemathsimplealign [myalign] [align=left, location=top]
\definemathsimplealign [myouteralign] [align=left, location=center]
\definemathsimplealign [mydistancedalign] [align=left, distance=1em, leftmargin=1em]
\definemathsimplealign [mymarginedalign] [align=left, leftmargin=1em]
\startdocument
\startplaceformula \startformula [align=flushleft] \startmyouteralign \NC \mathtextit{TransitiveClosure}(R) ≜ \NR
\NC \startmydistancedalign \NC \mtext{\sc let} \NC \startmyalign \NC \mathtextit {Dom} ≜ \lbr r[1]: r ∈ R \rbr \NR \NC \mathtextit {Rng} ≜ \lbr r[2]: r ∈ R \rbr \NR \NC \mathtextit {TC\/}[i ∈ ℕ] ≜ \NR \NC \startmymarginedalign \NC \text{\sc if } i = 0\ \startmyalign \NC \text{\sc then}\ \NC R \NR
\NC \text{\sc else}\ \NC \startmyalign \NC \lbr 〈d, e 〉 ∈ \text{\it Dom} × \text{\it Rng}: \NR
\NC \quad \∃ c ∈ \text{\it Dom} ∩ \text{\it Rng}: \startmyalign
\NC ∧ 〈d, c〉 ∈ \mathtextit {TC\/}[i-1] \NR
\NC ∧ 〈c, e〉 ∈ R \rbr \NR \stopmyalign \NR \stopmyalign \NR \stopmyalign \NR \stopmymarginedalign \NR \stopmyalign \NR \NC \mtext{\sc in} \NC \mtext{\sc union } \lbr \mathtextit {TC\/}[i] : i ∈ ℕ \rbr \NR \stopmydistancedalign \NR \stopmyouteralign \stopformula \stopplaceformula
\stopdocument
/Mikael ___________________________________________________________________________________ If your question is of interest to others as well, please add an entry to the Wiki!
maillist : ntg-context@ntg.nl / https://mailman.ntg.nl/mailman3/lists/ntg-context.ntg.nl webpage : https://www.pragma-ade.nl / https://context.aanhet.net (mirror) archive : https://github.com/contextgarden/context wiki : https://wiki.contextgarden.net ___________________________________________________________________________________