Mac Malone

@Kha combining your suggestion with @gebner's your original example we would have something like: ```lean mut (·.push 42) references mut (·.push 42) ctx.references mut (· + 1) ctx.references[7] let mut...

> This is also `$=` in Idris' structure notation, but I suppose we now avoid this meaning of `$`. > FWIW, I recall that `jq` has `|=` for update assignment....

**EDIT:** @gebner, you literally posted your example while I was spell-checking mine. 🤣 So, I went ahead an coded up a quick demonstration of @gebner's original idea mixed with mine....

@Kha > What do you think, should we use `withRef` in preference to token antiquotations in macros, and then tag nodes created by quotations with the reference's full range? I...

@Kha > ``` > syntax compStmt := "{" declaration* cStmt* "}" > syntax compStmt : cStmt > ``` Oh. I had assumed that `syntax (name := foo) "foo" : cat`...

At the moment, it would have made the effort of writing this [regression test for Lake](https://github.com/leanprover/lake/blob/master/test/49/test.sh) much easier. Instead, I had to figure out a lot more about how the...

Also, on a related note, in this section: https://github.com/leanprover/lean4/blob/d78e7cd011dda386d6d57efb9def5c0e6a3164fb/src/Lean/Server/Watchdog.lean#L702-L705 The `let` statement should be `let Message.notification "exit" _` as the `let` otherwise fails on `exit` notifications with empty `params` (which...

Oops! I discovered that I had provided the wrong plugin when testing this (which was thus missing the symbol). Providing a plugin with the proper symbol **does work** (the server...

The hanging that occurs when trying to evaluate a missing symbol appears to be caused by the bug described in #640.

@Kha While I would prefer the error being recoverable, I would at the very least hope it would actually kill the worker than exist in a zombie state that persists...