Eli Dupree

Make sertop respond consistently to SIGINT

1

Currently, [these notes](https://github.com/ejgallego/coq-serapi/blob/v8.12/notes/ser-control-protocol.md#interrupting) appear to be the most detailed documentation on interrupting sertop: > ### Interrupting > > 1. The IDE must send an interrupt signal to sertop. > 2....

Add a query to perform a diff of terms

6

In my [work-in-progress proof explorer GUI](https://github.com/elidupree/coq_experiments/tree/main/proof_explorer), I currently display diffs of goals by doing a diff on their string representations. It would be better to diff the term structure -...

ConsAccess always yields the same value indefinitely

2

[This impl](https://github.com/rotty/lexpr-rs/blob/master/serde-lexpr/src/value/de.rs#L336-L352) never modifies `self`, resulting in an infinite loop. The tests missed this case because [ConsAccess is only constructed if you arrive at visit_seq through deserialize_any](https://github.com/rotty/lexpr-rs/blob/master/serde-lexpr/src/value/de.rs#L69) rather than [deserialize_seq](https://github.com/rotty/lexpr-rs/blob/master/serde-lexpr/src/value/de.rs#L182-L192).

The body of `to_value` does nothing but call `serde::Serialize::serialize`, which takes `&self`; thus, like other serialization methods, `to_value` should take `&T`.

[SerAPI](https://github.com/ejgallego/coq-serapi) represents struct fields as `(name value)` (inheriting that behavior from [Sexplib](https://github.com/janestreet/sexplib), I think), while serde-lexpr represents them as `(name . value)`. To make serde-lexpr compatible with more kinds of...

Whenever I undo while agda-mode is active, it undoes twice. This is rather inconvenient! This is on a fresh install of Atom and agda-mode from December 2; Atom 1.53.0, agda-mode...

Currently, the behavior of mouse_scroll_y is inconsistent (going in opposite directions) between Linux and Windows. The Enigo docs state "Positive numbers for length lets the mouse wheel scroll down and...

I actually ran into this issue while using [Prunkton's fork](https://github.com/Prunkton/enigo), where it caused a segfault, but it seems like it would affect mainline Enigo as well. [This source code from...

I ran into this panic during actual usage, then reduced it to these tests (borrowing test code from `test_tensor_ops_grad.rs`). It seems like maybe it's trying to take the gradient of...

Newbie-friendly documentation would be a huge benefit

3

I'm currently working on some ML projects where autograd looks like the ideal tool for the job. Unfortunately, I had a bit of trouble figuring out the basics of autograd,...