max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/pkg
History
Sebastian Ullrich c7d3401417
fix: split ngen on async elab (#12000) 
This PR fixes an issue where go-to-definition would jump to the wrong
location in presence of async theorems.

While the elaborator does not explicitly depend on `FVar`s not being
reused between declarations, the language server turned out to do so. As
we would have to split the name generator in any case as soon as we add
any parallelism within proofs, we now do so for any async code in order
to uphold this invariant again.

---------

Co-authored-by: mhuisi <mhuisi@protonmail.com>
2026-01-14 12:35:25 +00:00
..
builtin_attr chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
debug chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
def_clash chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
deriving chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
frontend chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
initialize chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
leanchecker feat: re-integrate lean4checker as leanchecker (#11887) 2026-01-08 09:41:33 +00:00
linter_set chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
misc fix: local syntax should create private definitions 2025-08-19 14:49:12 -07:00
mod_clash chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
module fix: split ngen on async elab (#12000) 2026-01-14 12:35:25 +00:00
path with spaces chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
prv feat: improve error message in the case of type class synthesis failure (#11245) 2025-11-21 21:24:27 +00:00
rebuild feat: module system is no longer experimental (#11637) 2025-12-12 21:20:26 +00:00
setup chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
signal chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
structure_docstrings chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
test_extern chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
user_attr chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
user_attr_app chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
user_ext chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
user_opt chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
user_plugin chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
ver_clash chore: ensure every pkg/ test has a correct lean-toolchain file (#11782) 2025-12-23 17:17:22 +00:00
.gitignore test: module clash across packages (#11246) 2025-11-19 02:23:34 +00:00