Jon Sterling

I think my code suffered from a kind of subtle version of the “Goodbye, Lenin” problem — which was hard to tell since I have never run it 🫠🤣

But yesterday I took some time to rearchitect things and I believe I have forestalled any possible version of this. Famous last words, etc., etc.

I’ve also (I believe!) corrected my implementation of observational postponement, which had been way too naïve and wasn’t stable under weakening.

Mar 25 at 8:48amWeb
Show threadJon Sterling4d ago
Implementing proof assistants is really arcane, isn’t it? If I were reading this post as someone inexperienced in this area I would think it was gobbledygook.
Show threadG. Allais4d ago
@jonmsterling what we need is a week (more?) long summer school on implementing something that's not a toy.
Show threadJesper Agdakx 🔸4d ago
@gallais @jonmsterling or a whole special semester bringing together all the experts so they can figure out both all the good ways to implement one and perhaps even write a book on it.
Show threadJon Sterling4d ago
@jesper @gallais I love the idea... but I can't imagine being away from my job (teaching!) or my wife for a whole semester.
Show threadMeven Lennon-Bertrand4d ago
@jesper @gallais @jonmsterling This would be extremely cool!
Show threadJan de Muijnck-Hughes4d ago

@mevenlennonbertrand @jesper @gallais @jonmsterling not cool but Dagsthul…

Although, iiuc, it’s not the kind of thing Daghtul is for. But Scotland could lead forwards with an FP Castle sort of gig….

Show threadterru4d ago
@jonmsterling so now i am curious: what is the 'goodbye lenin' problem? (an internet search seems to turn up nothing fitting)
Show threadJon Sterling4d ago

@stuebinm It's an allusion, made by @pigworker, to the film “Goodbye, Lenin” which concerns a patriotic/civic-minded woman in East Germany who fell into a coma just before the fall of the Berlin Wall, and then how when she wakes up her son tries to protect her from the shock by creating fake news reels and so on that perpetuate the illusion that the DDR had kept on going.

In the context of proof assistants, what it refers to is that you may evaluate some terms at one point in time, and in doing so produce closures that capture the state of knowledge at the time they were frozen, and if you are not careful to "refresh" old things against the current state (which may have new solutions to various problems) you can run into trouble.

Show threadMorgan Arnold4d ago
@jonmsterling can confirm! i've been trying to follow along with development, and it's damn hard to follow without a lot of rather specific background in the implementation of dependently typed programming languages. i've been trying to learn, but it's definitely not the easiest thing to break into
Show threadMorgan Arnold4d ago
@jonmsterling oh, out of curiosity, is continuing with the current implementation of pterodactyl written in swift the long-term plan for the language, or is the plan to write a proof-of-concept implementation in swift before pivoting to an implementation in some other language? i ask because i spent a bit of time yesterday attempting to build pterodactyl locally on my machine and ran into... issues. indeed, i'm not sure if it's possible to build pterodactyl on linux?
Show threadMorgan Arnold4d ago
@jonmsterling i documented some of the specific issues that i ran into here: https://mathstodon.xyz/@mra/116286636195133945, but they probably aren't of much interest. there are a lot of nixos-specific issues that i ran into, but the crux of it seems to be that `.linux` is not a `SupportedPlatform`, so it can't be added to the `platforms` field of the `package` declaration in Package.swift.
Show threadJon Sterling3d ago
@mra I expect to stay with Swift. It should indeed be possible to build with Linux, but I haven't tried. Swift is used on Linux all the time, and I'm certain there is no obstacle to building via Package.swift (but maybe I need to change it in some way)...
Show threadMorgan Arnold3d ago
@jonmsterling ah, you're right that it is possible to build on linux. i guess i misunderstood the meaning of the `platforms` field. my issue appears to be a nixpkgs issue, since the status of swift support in nixpkgs is pretty abysmal. the best i can do is to compile pterodactyl within one of the docker containers provided by the swift folks. this works, but i can't run the resulting binary on my system because it's dynamically linked, and i can't patch it because the required libraries aren't in nixpkgs
Show threadMorgan Arnold3d ago
@jonmsterling i had hoped that the static linux sdk might save me by making it possible to compile pterodactyl as a static binary for linux, but compiling pterodactyl against the static linux sdk fails for some rather arcane-looking reason. on the bright side, pterodactyl seems to build just fine on linux in general, the problem is just with nix
Show threadJon Sterling3d ago
@mra Ah OK. Yeah, I just did it in docker and I did have one little issue with an Apple-platform-only API in Foundation, but this was easily resolved: https://tangled.org/jonmsterling.com/swift-pterodactyl/commit/bd5f87117d4561f4b4d026b059ebb11f8339984d
Get Pterodactyl building on Linux · jonmsterling.com/swift-pterodactyl@bd5f871

A repository on Tangled

Tangled
Show threadMorgan Arnold3d ago
@jonmsterling ah, sorry i forgot to mention that! i commented that out to get it to compile. i reached out to the team working on swift 6.2 packaging in nixpkgs, and it sounds like they have swift 6.2 building with nixpkgs on darwin, but it's still not working on linux. once they get swift 6.2 building on linux i'll write a nix flake for pterodactyl