I really like having ~8-12 active Ghostty windows tiled so I can keep an eye on everyone's progress, and then I'll expand one or two for deeper work. Would love to see some sort of auto-expand/contract so I can keep an eye on everything but then when I foreground a pane it grows, or something like that.

Ah, like a way to maximize the current pane you're focused on?

Yep! Also a simple text editor pane would be sweet too.

Haha, it's like we're moving towards an IDE but starting from the opposite direction.

My two cents - don’t do it. There’s plenty of terminal editors (and personal opinions about them) to chose from. You will end up reinventing an IDE.

>So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task.

Is this true?

e.g. the Riemann hypothesis is in mathlib:

  def RiemannHypothesis : Prop :=
    ∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2

If I construct a term of this type without going via one of the (fairly obvious) soundness holes or a compiler bug, it's very likely proved, no? No matter how inscrutable the proof is from a mathematical perspective. (Translating it into something mathematicians understand is a separate question, but that's not really what I'm asking.)

Sorry, I mean verify the semantics of what the LLM has generated is exactly what you were asking for.

I don't understand that. If it has a correct statement of the theorem and no `believe-me`s or whatever, it should be correct.

Yep, same here, with those exact prefixes...

Non-async functions are absolutely blocking. The question is if they’re expected to block for a meaningful amount of time, which is generally suggested by your async runtime.

It’s really not that bad, you might just need a better mental model of what’s actually happening.

Depends, on Linux you can call set_nonblocking on a TcpListener and get a WouldBlock error whenever a read would block. That's called non-blocking.

Doesn't this miss the forest for the trees? The entire point is to drive with epoll.

Well, yes. But it means you can do sync non-blocking IO by hand.

You can absolutely do global knowledge in proc macros via the filesystem and commit their output to version control: https://github.com/trevyn/turbosql

You can introduce side effects to a proc macro (but please avoid if at all possible), but you cannot control the order in which proc macros are run. If you need to reason about the global schema while generating code, that won’t work.

Lol, you haven’t learned your lesson with Vercel yet?

“The flawless binary is free to use, but only distributed as a closed source binary.”

Insta-pass.

Note that you can be anti-Russia and anti-Ukraine at the same time.

Also, crucially, Starlink has been proactive in trying to disconnect Russian operatives who have managed to attain a Starlink connection. All the same, Elon’s backing of Trump doesn’t bode well for a good outcome for Ukraine (nor other ex-USSR satellites that are feeling very nervous right now)

I misspoke. They've been very quick to react to Ukranian intel. If they were staffed, perhaps they'd have the capability to be proactive, but I can't necessarily say they would be motivated to, esp. when the military is doing that for them. And the Ukr. military are perhaps more effective because they know where their communication centers are supposed to be under the fog of war. That said, I'm only going on what has been said in public

The Feds said they were proactive. It's not SpaceX that claimed that

Forced. The word proactive is in a statement from a Pentagon official, not SpaceX.

AlotOfReading, based on your other post in this thread, your information on Starlink limits is very out of date.

Readers, I would take posts from this user with a large grain of salt.

>Starlink limits to low hundreds (~300) of terminals per cell.

That’s… very incorrect.

Do you have a correct number by chance?