Mario Carneiro

perf: rewrite UnusedVariables lint

23

This is a rewrite of the `UnusedVariables` lint to inline and simplify many of the dependent functions to try to improve the performance of this lint, which quite often shows...

fix: don't write padding bits to olean files

4

With `USE_GMP=OFF`, the implementation of `mpz` used a `bool` next to a `size_t`, resulting in 7 bytes of padding that are faithfully copied into the `.olean` files on affected systems,...

fix: segfault in old compiler due to noConfusion assumptions

4

This fixes #2901, a bug in the old compiler which causes a segfault. The issue is that when visiting `noConfusion` applications, it assumes that each constructor case has `nfields` arguments,...

[Bug]: Building the examples don't work (cargo apk + bin = fail)

2

### What happened? Building the examples according to the instructions fails with the error `Error: Invalid args.`. This exceptionally bad error message comes from `cargo apk`, which [expects the cargo...

It would previously encode a relative import with a suffixed `_0`, which can collide with actual lean names.

fix(frontends/lean/parser): start positions of trailing parser (NuD) nodes

1

As observed by @eric-wieser , the node for `notation[$]` in ```lean theorem foo : true := id $ trivial ``` was covering only the span `$ trivial` instead of `id...

Set up github actions for automatic build and deploy

3

A lot of issues are being caused by the lack of prompt binary releases. It is possible to set up github actions so that it will automatically build mmj2 and...

mm0-rs as a library

3

This is a tracking issue for mm0-rs as a library: * Have an API for usage from other rust projects, deploy on crates.io * Make the API usable using C...

Some maps like `Shirobon - Into the Zone` make use of the `Mapping Extensions` add-on(?), in which `_lineIndex` and `_lineLayer` are not in the range 0..3, 0..2 but are instead...

* [ ] depends on: #198 This completely hides the off-hand and disables all feedback for it when in OneSaber mode; otherwise it's just an awkward thing you have to...