Mario Carneiro

`linter.unusedVariables` false positive

1

```lean example : ∀ (l : List α) n, l.get? n = some a → True | _::_, _+1, _ => trivial | _::_, 0, rfl => trivial --^ unused...

```lean example (P : Nat → Prop) (a) (h : ∃ n, a = n + 1 ∧ P n) : ∃ n, P n := by let ⟨n', e,...

panic in info handler on unterminated doc comment

4

The following lean file: ``` /-- ``` causes this panic: ``` PANIC at Lean.Server.Snapshots.Snapshot.infoTree Lean.Server.Snapshots:68:2: assertion violation: s.cmdState.infoState.trees.size == 1 backtrace: /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f] /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at_Lean_Server_FileWorker_handleDocumentHighlight___spec__1+0x92)[0x7fe4326b5b12] /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x36)[0x7fe4326eeb06] /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1+0x9a8)[0x7fe4326ef9a8] /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0xa4b)[0x7fe4326f143b] /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4] /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343] /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4] /home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]...

feat: norm_num extensions

1

This PR is an almost complete rewrite of `norm_num` to implement its functionality via an extensible attribute for plugins, and use `Qq` for expression construction.

The `simp_intro` tactic is a combination of `simp` and `intro`: it will simplify the types of variables as it introduces them and uses the new variables to simplify later arguments...

``` $ mix bors.cleanup --months 1 Cleaning data older than 1 months ** (ArgumentError) errors were found at the given arguments: * 1st argument: no persistent term stored with this...

The original code was using `this.bbox.expandByScalar(-0.25);` to decrease the size of mines (for reasons I was unable to determine), but the bbox is only 0.328 large in the x direction...

Debugging fails to start on Ubuntu + Rust, "Connection shut down by remote side..."

8

OS: Ubuntu 22.04.1 LTS VSCode version: 1.75.1 CodeLLDB version: v1.8.1 Compiler: rustc 1.69.0-nightly (5243ea5c2 2023-02-20) Debuggee: x86_64-unknown-linux-gnu I get an error `Connection shut down by remote side while waiting for...

feat: lake: add `lake dump-config` command

18

This adds a mechanism to dump most of lake's workspace configuration state (everything except the functions, more or less) to standard out in JSON format. This is roughly equivalent to...