Sebastian Ullrich

feat: snapshot trees and language processors

8

This is the foundation for work on making processing in the language server both more fine-grained (incremental tactics) as well as parallel. Includes: - #2959 - #3013 TODOs before merging:...

Sort messages by position when printing

4

As exhibited in #2276 but already encountered many times before I believe, so it is high time to make the message ordering more deterministic. Unfortunately there is some perhaps unwanted...

Make token parser customizable

10

In theory, users can implement arbitrary lexical grammars as the built-in token parser is merely another combinator whose use can be avoided; in practice, avoiding it also means forgoing the...

feat: incremental elaboration of definition headers, bodies, and top-level tactic blocks

1

Implements a syntax-based approach for incremental reporting and reuse for the following intra-command elaboration steps: * finished definition (`def`/`theorem`/`abbrev`/`opaque`/`instance`/`example`) headers (binders and result type) when all syntax above is unchanged...

fix: do not dllexport symbols in core static libraries

6

On Windows, we now compile all core `.o`s twice, once with and without `dllexport`, for use in the shipped dynamic and static libraries, respectively. On other platforms, we export always...

feat: introduce auto-imported `Base` package

3

We are planning to introduce a new package to core for functionality that a) is not strictly necessary for building Lean (so it should not be in `Init` or `Lean`)...

feat: enforce indentation of command contents

5

Only affects parts using `colGt/Ge`, e.g. arguments to functions See test case for motivation

feat: bundle std4

1

Let's see if anything breaks

feat: new snapshot architecture on the cmdline

10

This is #3014 with cad5cce reverted for testing.