Post #4119644
2026-05-27 01:53 UTC
checking out a tutorial project and I need to "trust" the project folder - which AFAICT allows arbitrary code exec on my machine by whoever authored the repo - in order to interact with Lean code in any way, even syntax highlighting, it seems? What the actual fuck? Who thought the correct options were (a) things just don't work at all, (b) arbitrary code exec, and NOTHING IN BETWEEN?
modern development baffles me.
Replies (2)
-
@rntz@recurse.social 2026-05-29 12:28
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.
-
@flippac@types.pl 2026-05-27 10:46
@rntz@recurse.social it's the purple slop prover, what's there to be baffled by?... (screaming "WTF?!?!?!" isn't bafflement)