Keeley Hoek

`expr.fold` uneccesarily(?) is not defined for `pexpr`s

3

The statement of `expr.fold` is ```` meta constant expr.fold {α : Type} : expr → α → (expr → nat → α → α) → α ```` which prohibits folding...

This is very easy. There are two options, since if we are currently in a namespace the builtin `tactic.open_namespaces` returns the current namespace as the first entry: 1) Modify the...

fix(hid): Eliminate data race in USB pathway causing dropped keys

5

As I found out diagnosing #2253, there is a data race in the USB HID core on many platforms; the call to `hid_int_ep_write()`, a Zephyr function, doesn't always copy the...

fix(hid): Eliminate data race in USB pathway causing dropped keys [ALTERNATIVE]

2

Alternative to https://github.com/zmkfirmware/zmk/pull/2257, solving the same problem which happens there, perhaps more elegantly. We simply move the existing mutex to protect calls to `hid_int_ep_write()` as well as the passed buffer,...

NKRO breaks layer-tap with "extended" keycodes

9

The binding `&lt my_layer F24` doesn't work properly with NKRO on, even with extended reporting enabled. I observe that: with `CONFIG_ZMK_HID_KEYBOARD_NKRO_EXTENDED_REPORT=n` I never see an `F24` at all when tapping...

USB core has a data race during write on many platforms

3

The function `hid_int_ep_write()` has a data race where the TX data may change underneath the USB driver. For example, `hid_int_ep_write()` calls `usb_write()` directly passing the user's data buffer. Many USB...

refactor(hog): Cleanup ble message sending

4

We deduplicate a bunch of code removing about 80 lines (not clear from the diff due to dependence on other PR), fixing a very minor copy-paste typo in the process....