@acegikmo My engine: (+x,-y,1-z)
@j3rn There's a preprocessor, but IMO that's not worth the fuss.
These bots are made for walkin'
And that's just what they'll do
One of these days these bots are gonna walk all over you
@Firefishy @internetarchive Friends don't let friends deal with PayPal.
@BoydStephenSmithJr Can you fold on the index and do a projection from the cursor to children nodes in each of the streams?
@alois Cool! What would happen when the deadline comes? Are you betting on counting reductions? So many questions... 😅
@ericflo Not gonna bite the bitter lesson, are you? 😄
@shapr It will be demand-driven. Whenever the next line is required for processing it will read it from a buffer, block until there's input, or stop.
It shouldn't retain previous lines unless you keep references to them somewhere.
@alois Real-time as in "executes under a hard deadline"?
@anandamide It doesn't matter. As long as he can deliver an interplanetary logistic network the humanity is in the green. I think it is just simpler to rally midwits with The Mars Colony than "actually, let's just strip-mine it with nuclear excavators and build huge orbitals". L5 society tried the latter and failed to gain interest.
@jesper wide.
("none", even, if a dependency is on Stackage)
It's cheaper to pin down version than to fuss around allow-newer.
@tristanC They aren't migrating if I understood correctly. Just need a way to produce TS apps from Agda sources and LLM translation happens to do a better job at it than a "real" compiler.
2022: We need end-to-end certified compilation!
2024: Nah, just stuff your "proofs" into an LLM to get "executables".
https://x.com/VictorTaelin/status/1837925011187027994
> Since the AgdaJS compiler isn't maintained, and since creating one would be a $1m-budget project, we're now compiling 590 Agda files to TypeScript using Sonnet-3.5, to let us run our apps on the browser.
> The results are excellent. Almost all files work with no intervention. Error rate is lower than the current AgdaJS compiler, on which we found bugs. Performance is 20x higher. We're now automating this in a loop.
Toots as he pleases.