lean4

lean4 copied to clipboard

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]...

digama0

Decide on memory representation of opaque type definitions

1

In short, the question is whether the following cast is safe: ```lean opaque Foo : Type := Bool unsafe def foo : Foo := unsafeCast "123" ``` This pattern is...

gebner

Add a safe wrapper around `ptrEq`

3

We want to use pointer equality as a performance optimization. For example, as a first check in `DecidableEq` instances: if the two arguments are pointer-equal, then we can immediately return...

gebner

I have more requests: - [x] `Float.abs : Float → Float` seems to be missing - [ ] `Float.toInt : Float → Int`, where it returns a best-effort GMP integer...

EdAyers

[RFC] Pretty Printer / Code Formatting

8

I'm currently looking into improving the pretty printer and would like to hear what you think about how we should format Lean code. This is important for many potential editor...

larsk21

Double-backtick quotations with other syntax categories/parsers

2

Currently ``` ``(cat| ...) ``` is not supported, i.e. it can only be used with `command/term`. I'd like to wait with this change until we have unified the `|` notation...

Kha

feat: reserved names

1

- Add support for reserved declaration names. We use them for theorems generated on demand. - Equation theorems are not private declarations anymore. - Generate equation theorems on demand when...

leodemoura

feat: upstream apply helper tactics from Mathlib

1

These are used in Mathlib's `congr!` and `convert` tactics, which will be upstreamed soon.

kim-em

fix: use builtin_initialize in library_search

1

This replaces a few uses of initialize with builtin_initialize, and removes some unneeded functionality added when it was unclear if lazy discriminator trees would be efficient enough.

joehendrix

feat: upstream Std's rfl tactic

2

This allows tagging lemmas with `@[refl]`, that will then by used by `rfl`. This is preparatory to upstreaming Mathlib's `convert` tactic.

kim-em