Post #4119647

2026-05-29 12:28 UTC

looks like "no syntax highlighting without trust" is specific to Lean, not VSCode, because Lean has strong syntactic metaprogramming (hey, I like mixfix and syntax extensions!) but this means you have to run Lean code to parse Lean (eh, okay...) and Lean is also a general-purpose programming language (useful...) which can access your filesystem in arbitrary ways (uh oh) and it doesn't come with a sandbox so... yeah, you have to trust the project to syntax highlight it iiuc. argh.

Replies (4)

@rntz@recurse.social 2026-05-29 12:30

Likewise, mathlib being 7G compiled is not *that* ridiculous given it's a formalisation of substantial parts of modern math (as someone pointed out to me on twitter). And, yeah, many modern languages do per-project dependency management to avoid versioning difficulties. there is like, no individual part of this that is indefensible. but the combination of everything just results in something that is... not great as a first experience.

Open ##4119649
@tonyg@pubsub.leastfixedpoint.com 2026-05-29 12:38

@rntz@recurse.social You'd think for people swimming in fancy types they'd have considered using, say, some kind of effect system in conjunction with ocaps. Ah well.

Open ##4119652
@jonmsterling@mathstodon.xyz 2026-05-29 13:08

@rntz@recurse.social I think it basically amounts to the fact that Lean is using the language server protocol to vend semantic highlights directly from the compiler. This is actually a better approach than using something like tree-sitter (or, god forbid, regexp), even for languages without metaprogramming, for the simple reason that you don't have to maintain two grammars. But it does mean that you have to trust the code.

Open ##4119653
@samth@mastodon.social 2026-06-01 18:08

@rntz@recurse.social This is just fundamental to macros. If you want on-the-fly syntax errors you have to run code. There's not really a third option.

Open ##4398827