nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe (nprofile…rrqe) Yeah at first I thought the Lean lsp was so cool and slick, but then over time I grew to prefer the agda-mode in emacs, with its manual control over reloading.
Of course, it's a lot more work to go outside of the lsp model, and sadly vscode support is probably important for pterodactyl because you don't want to waste a class every semester teaching students how to install emacs...
I feel like the ideal experience would be a clutch pedal: you hold it down while you are making an edit and the lsp takes a chill pill, and then you release it when you are done and you get up to date semantic information.
I do think that continual semantic highlighting is nice, just I don't want the squiggly underlines causing me stress.
Owen Lynch
npub1cj…fxs07
2025-10-19 20:26:55 UTC
in reply to nevent1q…6t9p
Author Public Key
npub1cjyyl7y66997ewku92pzvvhkyec43k7cde44rhgayxdwwl63axdqafxs07Seen on
wss://relay.ditto.pubPublished at
2025-10-19 20:26:55 UTCEvent JSON
{
"id": "f1d85777e112055d79a7b63cbcc11d9cac2b0cd63d50e6b771be44545dc696cd",
"pubkey": "c4884ff89ad14becbadc2a822632f6267158dbd86e6b51dd1d219ae77f51e99a",
"created_at": 1760905615,
"kind": 1,
"tags": [
[
"p",
"934feab351ac5e89a35eb05d4dd0be4c6ad19583792f609db6dcf7d3a9e71f49",
"wss://relay.ditto.pub/"
],
[
"p",
"ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"wss://relay.ditto.pub/"
],
[
"e",
"fc68794690f9cce435df74be0b7b73c0620dbe08430eacb4708338bba26662df",
"wss://relay.ditto.pub/",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/olynch/statuses/115402710418806709",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "nostr:nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyzf5l64n2xk9azdrt6c96nwshexx45v4sduj7cyakmw005afuu05jm4rrqe Yeah at first I thought the Lean lsp was so cool and slick, but then over time I grew to prefer the agda-mode in emacs, with its manual control over reloading.\n\nOf course, it's a lot more work to go outside of the lsp model, and sadly vscode support is probably important for pterodactyl because you don't want to waste a class every semester teaching students how to install emacs...\n\nI feel like the ideal experience would be a clutch pedal: you hold it down while you are making an edit and the lsp takes a chill pill, and then you release it when you are done and you get up to date semantic information.\n\nI do think that continual semantic highlighting is nice, just I don't want the squiggly underlines causing me stress.",
"sig": "a19a109bf0a17b431933663dea08e3c18f251a0175a456ba706fea7dcd109c06b0d2118e06f22df444c4135e5b617a8cea301bbba31f92700c74a9d5b3cd5a1d"
}