Here we provide a summary overview of recent changes, bug fixes, and new features added to Lurch in reverse chronological order. This will continue to be updated with the most recent changes at the top.
Validation algorithm efficiency - used Claude Code AI to profile the validation code and find bottlenecks. Three very minimal improvements were made that improve algorithm efficiency by 29%. When combined with previous improvements Lurch is now 43 times faster at validation than it was at the end of Spring 2024. The improvements are shown in order in the following table.
| Desc | Acid (s) | All Tests (s) | Δ% | Net % |
|---|---|---|---|---|
| baseline | 15.3 | 1411 | 0% | 100% |
| cached Declares | 8.8 | 504 | 64% | 36% |
| non-recursive filter | 8.2 | 473 | 6% | 34% |
| recursive filter | 5.5 | 313 | 38% | 22% |
| matching special case | 3.5 | 290 | 7% | 21% |
| treat Declares global | 3.3 | 256 | 12% | 18% |
| cache global constants | 3.2 | 251 | 2% | 18% |
| cache accessible fromLC | 3.1 | 219 | 13% | 18% |
| cache some CNFProps | 2.7 | 124 | 43% | 9% |
| looped tree traversal | 2.4 | 102 | 18% | 9% |
| inst just one weenie | 1.8 | 46 | 55% | 3% |
| deepCopy/fast prop/cache sigs | 1.7 | 33 | 29% | 2% |
Playwright web UI test suite - added a test suite for the web UI based on Playwright. Currently tests that the gallery documents load and validate and only produce green checks (at least one). It also loads some custom test files that check feedback markers against expectations.
Declarations with environment bodies - upgraded the validation algorithm to support declarations with environment bodies, and handle unsupported declarations which have declarations in their body or start a Rule or Theorem environment (as they are unnecessary). With this change Lurch’s global validation algorithm now supports the final missing feature of super-natural deduction. This also fixed edge case bugs where validation would cause validation to throw an error and hang if the user had a leading declaration in a Rule or Theorem or a declaration with environment body in a Rule that had more metavariables than other expressions in the rule, which caused a crash when it tried to match the declaration.
Type checking of numeric constants - the built in Arithmetic rules can now validate statements of the form $x \in \NN$, $x \in\ZZ$, $x \in \QQ$, $x\in \RR$, and $x \in \CC$ where $x$ is a numeric constant expression that is allowed by the Arithmetic rule for the corresponding number system. It also assumes $\NN\subseteq\ZZ\subseteq\QQ\subseteq\RR\subseteq\CC$. For example, it will validate $42\in\NN$ and $42\in\RR$ but not $-42\in\NN$. It doesn’t matter what number system the Arithmetic rule itself specified, as these are explicit type declarations.
Subscripted constant relations and relation variables
- in order to support an infinite family of infix relations, you
can declare ~ to be a constant, and optionally
subscript it with natural numbers (or a sequence of natural
numbers), e.g., ~, ~_(0),
~_(1,2) etc. But in the rules that define the
properties of general relations (symmetry, transitivity, etc.) we
also need an infix operator that is not declared as a constant (so
it can be a metavariable in the rules). For this you can now enter
rel which formats as $\backsim$ so it looks *very
much like a generic infix relation and $\sim$ but can easily be
distinguished visually by an instructor when creating rules and
contexts. The implemented rules can be seen in the
Relations-Rules context.
Comments in expressions - you can now add
comments at the end of any meaningful expression by appending
// followed by plain text for the comment you want to
add which continues until the end of the expression dialog, even
when it is not a transitive chain. The plain text of the comment
can include expository LaTeX math expressions. For example you can
have a meaningful expression dialog entry like
contradiction // since we showed $x\neq 0$ and $x=0$.
This mechanism is not really necessary because you can just end
the dialog with the meaningful content and simply type the comment
in the editor direction, including the LaTeX expressions using the
expository math dialog, but we allow it for consistency with the
same mechanism available in transitive chains for convenience.
Comments in transitive chains - you can now
optionally add expositional comments after individual lines of a
transitive chain by appending // followed by any
plain text for the comment you want to add (until the end of the
line). The content can contain math expressions written in LaTeX
and surrounded by dollar signs. You can still add
by algebra or by arithmetic after an
individual line and it will format as meaningful when Meaning is
shown. Expositional comments following a // will
format in black font like the other expositional content in
Lurch.
Expression editor expands horizontally - the text input area of the expression dialog (both meaningful and expository) now will automatically increase its width to accommodate its contents in addition to adjusting vertically. The user can also manually resize the input area with their mouse as well.
Multiple Arithmetic rules - it is desirable to be able to override a context that contains, say, the Arithmetic rule for natural numbers with the Arithmetic rule for integers or rationals without removing the original rule from the document. Lurch now uses the last Arithmetic rule in the document rather than the first.
Support for + as an exponent - to allow set notation like $\RR^+$ for the positive reals.
Toggle editor margins - there is now a context menu item to toggle the document side margins on and off. This is useful for opening both a document and its context side-by-side (see Open Context in new document below), especially in presentations on a classroom projector. It is also useful if some math expressions in your proof are wider than the default content width.
Quantification Type support - Lurch now supports the notation $\forall x\in A.P(x)$ and $\exists x\in A.P(x)$, and expands them automatically under the hood to $\forall x.x\in A \implies P(x)$ and $\exists x.x\in A \xand P(x)$, respectively.
NoMatrixOps flavor of the Algebra Rule - In
documents where you want the algebra rule to be available but
disallow matrix operations you can now provide an option to the
algebra rule as AlgebraRule(NoMatrixOps).
Matrix support for the Algebra Rule - you can
now justify any identity that can be validated by
Algebrite, including identities
involving matrices. The input for the expression must be valid
Algebrite syntax (with the exception that = must be
used in place of ==) and you can use the added tick
marks to transpose the formatting of a matrix or vector (not the
meaning). The tick marks are stripped off before sending to
Algebrite.
Improvement to expression dialogs - added a shortcut-help footer to the expression entry dialogs that appears when the dialog loses focus and the current contents have not been saved.
Open Context in new document - added the ability to open the context in a separate document to facilitate split-screen viewing of the document and its context at the same time. Implemented this as part of the context menu (pardon the pun) that comes up when you right-click (or two finger tap on Mac) on the visible context in the document. Adjusted the placement of the logo for narrow screens that can occur when using it split-screen. This is useful for in-lecture presentations.
UI tweaks - added toolbar buttons for showing the context and validation. Changed the default view for new documents to the show-meaning view since that’s what almost everyone uses 99% of the time. Changed the default for environments when hiding meaning to unindented, since that matches normal math prose and illustrates what the meaning view is revealing. Removed change of background color on hover when showing meaning since the environments are clearly visible in that view and the hovering interferes when projecting Lurch in the classroom during lecture.
ChangeLog Page! - added this changelog page to this site. 😎
Improved parser docs page - made it easier to enter lengthy expressions in the parser docs page, by making the input text area full width and auto-resizing vertically to fit content. Improved overflow and resizing for the rendering and meaning outputs.
Fit-to-Content environment option - environment widths can be toggled between full width and just wide enough to fit their contents (and centered) from the right-click context menu. This is useful for examples like the group theory example, or linear algebra examples #2 and #3, where you want to define a formula (i.e., a single expression rule) temporarily for a particular problem (as opposed to adding it to the context).
Environment labels - can be customized and toggled on and off from the right-click context menu. The new default is to hide them, since they are redundant (the environment background colors distinguish them).
Full screen mode - is available on the toolbar and via the context menu if you right-click anywhere in the editor.
Group Theory and Linear Algebra examples - added to the examples gallery. The group theory example uses the Linear Algebra context.
Linear Algebra Context - added a starter context for Linear Algebra for two and three dimensional vector spaces over the reals. It defines linear transformation and subspace. It is not enough for an entire course, but more rules and definitions can be added in the future.
Friendly Rule Name Options - the Algebra Rule
can now be specified by entering
"algebra rule" (case insensitive, double
quotes are required) as a single expression in a rule environment,
instead of AlgebraRule (case sensitive). Similarly,
"equations rule" or
"chains rule" can be used instead of
EquationsRule or ChainsRule. This makes
it easier to format the rule in a more natural mathematical way,
instead of the more computery camel case originals (which still
work for backward compatibility).
Error highlight in parser docs - the input text area on the parser docs page now turns red when the contents can’t parse.
Algebra Rule includes Arithmetic($\mathbb{Q}$) - the Algebra Rule now validates inequalities which can be checked by the Arithmetic($\mathbb{Q}$) rule.
New Infix Operators - the expressions
x star y, x oplus y,
x otimes y, and x odot y now render as
$x\star y$, $x\oplus y$, $x\otimes y$, and $x\odot y$
respectively. Semantically they are treated as $n$-ary operators.
For example, x star y star z means
(★ x y z) under the hood in putdown notation.
Matrix Product and Inverses - the expression
dot([[a,b],[c,d]],[[e,f],[g,h]]) formats as
$\left[\begin{matrix} a & b \\ c & d \end{matrix}\right]
\cdot \left[\begin{matrix} e & f \\ g & h
\end{matrix}\right]$ and inv([[a,b],[c,d]]) formats
as $\left[\begin{matrix} a & b \\ c & d
\end{matrix}\right]^{-1}$. This notation is compatible with
Algebrite, so can be used with by algebra to validate
identities.
Added $\neq$ support - the Arithmetic rules now can validate the $\neq$ relation in addition to $=$, $<$, and $\leq$.
Column Vector Support - placing a tick mark after a tuple or matrix transposes the output (but not the internal meaning). This allows a user to format the output of tuples as column vectors.
Custom Parsing Tracer - wrote a development tool for tracing the parsers when debugging, and integrated it with Lode. Only useful for developers who are customizing the parsers.
Indexed Product support - added to the $\LaTeX$
parser so that product(E(n),n,a,b) formats as
$\displaystyle\prod_{n=a}^{b} E\left(n\right)$. Additional forms
of input might be added later, corresponding to how it handles
indexed sums, with some reasonable precedence.
Absolute value support - added to the $\LaTeX$
parser so that abs(x) formats as $\left|x\right|$.
100 Theorem Challenge - added Theorem 66 proof by Dan Cerra, and updated the context of Theorem 1.
Improved formatting of Summations in Products -
there was a parsing bug that would prevent expressions entered as
sum(f(k),k,0,n)*x from parsing because summation was
higher precedence than products. Now products have a higher
precedence than summations, and the tex formatter takes this into
account when deciding whether to add parentheses around a
summation.
Algebra Rule Support in Transitive Chains - Users can now cite ‘by algebra’ after any equation within a transitive chain when the Algebra Rule is available to check simple algebraic identities by CAS.
Even More Efficiency Improvement - Lurch is now 31 times faster at validating typical documents than it was in May 2024. Multiple things contributed, but the main one was only instantiating one expression per pass for a given rule to avoid lots of duplicates. There is quite a bit of finesse required to do that in a way that doesn’t avoid instantiations.
Expression editor checks both parsers - upgraded the expression editor dialog so it forbids any Lurch notation that can’t parse with both parsers, LaTeX and putdown (it was only checking conversion to LaTeX).
Symbol Names with Spaces - You can now use
double quoted strings containing spaces as symbol names, e.g.,
declare is, "natural number" and
Assume n is a "natural number". Here,
“natural number” is a single Lurch symbol. In the editor, the
surrounding quotes are hidden, so the latter expression appears
simply as Assume n is a natural number as desired. If
user-defined MixFix operator capability is implemented in the
future, double quotes may no longer be necessary.
Summation notation fix - Summations no longer require parentheses around the upper or lower bound when the bound is a sum.
Improved Rule Searching Interface - The search tool input box now gets focus when the hotkey to show the context is pressed. The hotkey still functions when focus is in the search box. It also puts a nice title on the search results and gives an informative message when no rules match the search string.
Clear Feedback on Remove Environment - if there
are validation feedback icons in the document and the user selects
the Remove this environment context menu item, it now
clears the feedback icons. Any document change that may affect
validation should also clear existing feedback. This was one of
the missing edge cases.
Modal Validation Dialog - replaced the non-modal
validation progress notification with a modal dialog. Also added
an application setting that determines if it will show a
Validation... done! message for 0.75 seconds when
validation completes. In progress validation can be terminated
immediately by pressing the escape key or closing the dialog.
Using a modal dialog has two advantages:
Expository Math Dialog Label - added a label and tooltip to distinguish it from the meaningful math dialog.
Lurch notation - The Lurch notation ‘neg’ and
‘not’ both semantically parse the same way, but ‘neg’ renders as
$\neg$, while ‘not’ renders as not
Context Display Overhaul
Added MathLive and KaTeX locally to the Lurch repository to prevent Lurch rendering from breaking when the CDN doesn’t deliver MathLive (as happened with the unpkg and the current version used by Lurch)
Enabled Editing Marginal Labels for environments that show up in Show Meaning view.
Major Efficiency Improvements
Improved Benchmarking and Profiling Reports and integrated with Lode
Added Transitive Chain Support for Inequalities
(trans_chain arg1 op1 arg2 op2 ... op_n arg_n).Changed Feedback Icon - for preemies from to , to be consistent with the rest of Lurch feedback icons which only get a when they are known to be wrong, not simply currently unproven.
Changed the Formatting for ‘and’ in Declaration Sequences when showing meaning
and and the grammatical insertion of the word
and before the last constant being declared.