Lurch Changelog
Recent changes and updates
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:
- It prevents the user from editing the document while validation
is in progress, and potentially receiving incorrect feedback as
a result.
- 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.