---

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.

• 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 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 on the home page. 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 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 inequalites 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 use cite 'by algebra' after any equation within a transitive chain when the Algebra Rule is available to check simple algebric 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 instaitiations.
• 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:
  1. It prevents the user from editing the document while validation is in progress, and potentially receiving incorrect feedback as a result.
  2. If the user edits an expression while validation is in progress, when the notification closed it would also close the user's expression editor dialog.
• 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
  • Showing context now summarizes declared constants at the top.
  • Reports when the context is empty rather than showing nothing or an alert
  • No longer highlights on hover - behaves more like an image
• 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 upkg and the current version used by Lurch)
• Enabled Editing Marginal Labels for environments that show up in Show Meaning view.
  • Added the necessary dialog
  • Added the context menu to open the dialog
• Major Efficiency Improvements
  • Validation is now 11 times faster than it was in May 2024
  • Cached some of the CNFProp computations and propositions
  • Major speed improvements to tree iterator utilities by Matthew Kilgore (thanks, Matthew!).
• Improved Benchmarking and Profiling Reports and integrated with Lode
• Added Transitive Chain Support for Inequalities
  • It now supports transitive chains with =, <, and $\leq$ in any combination
  • Semantically they all convert to (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
  • Distinguishes between actually declaring the constant and and the grammatical insertion of the word and before the last constant being declared.
  • The grammatical 'and' is shown in black, while the meaningful symbol is shown in gold.