* toolchain

* chore: bump toolchain to v4.23.0-rc1

This PR fixes the vararg syntax after it was accidentally broken by the
introduction of polymorphic range syntax in core and attempts to make
the grammar a bit more robust against future changes by only accepting
strings or identifiers in several places where it accepted arbitrary
terms before and limiting sub-commands to identifiers.

Notably, this PR contains a **breaking change**: Multi-line flag and
argument descriptions can now not contain inline-uses of `++` anymore.
It is advised to use [string
gaps](https://lean-lang.org/doc/reference/latest//Basic-Types/Strings/#string-literals)
instead.

This breakage unfortunately wasn't noticed in time due to our current
build setup excluding `Tests.lean` and `Example.lean`, which will be
fixed in a future PR.

Fixes #51.

This PR ensures that all tests in `Tests.lean` cause an error when there
is a test failure by using `#guard_msgs`, that `Tests.lean` and
`Example.lean` are run by `lake test` and that CI runs `lake test`. This
should hopefully prevent situations like the one in #51 from occurring
in the future.

It also replaces `Lean.RBTree` with `Std.TreeSet`.