Mario Carneiro

feat: FFI thread initialization

4

* #2490 * [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Expose.20thread.20management.20routines.20to.20FFI.3F/near/387373357) This exposes the following functions to FFI: ```c void lean_finalize_runtime_module(); void lean_finalize(); void lean_thread_initialize(); void lean_thread_finalize(); bool lean_in_thread_finalization(); void lean_reset_thread_local(); void lean_register_thread_finalizer(void (*fn)(void *), void...

feat: `opaque_repr` attribute to suppress "trivial structure" opt

1

This adds an attribute `@[opaque_repr]` which is used by both the old and new compilers to suppress the "trivial structure" optimization (which deletes `mk` and `proj` applications for newtype structures),...

Alternative version of #2263 . This modifies the desugaring for the cdot parser to apply eta-reduction to the resulting term if possible. So `(· + ·)` elaborates to `HAdd.hAdd` instead...

fix: resolve `_root_` in `macro`, `syntax`, `elab`

9

This is not just a convenience feature: Because `_root_` is resolved in `def`, if we do not also resolve it in `macro` there will be a mismatch between the syntax...

There was an ABI mismatch between the storage of `@[init]` declarations and the load in the interpreter, leading to garbage results. Discussed on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60lake.20exe.60.20interpreted.20mode.3F/near/361224125).

This PR normalizes usage of `binderIdent` vs `ident` across the lean grammar. To construct this PR I reviewed every occurrence of `ident` to determine whether (1) it is introducing a...

chore: normalize naming convention in theorems

4

Now that the [naming convention](https://github.com/leanprover-community/mathlib4/wiki#naming-convention) has been tested in mathlib, I think it is safe to backport the changes to lean core and normalize any remaining inconsistencies in theorem names....

feat: `show` tactic (full version)

2

This implements the TODO in the `show` tactic: `show e` will first try to change the goal to `e`, and if that doesn't work it will try to change one...

feat: `--continue-on-error` to produce .olean file even if elaboration fails

5

Implementation of the lean side of #3567. Passing `--continue-on-error` to lean will cause it to produce an `.olean` file even if the file had an error, but it will still...

feat: support idents in auto tactics

1

This is still experimental, but it implements identifier support in auto tactics "in the obvious way". It also converts `quoteAutoTactic` to generate Expr directly instead of going via syntax (this...