Note that Lean doesn’t have a monopoly on verification languages. Dafney, Rocq, Why3, ATS, Agda, Idris… these all can do it too. The fact that Lean is controlled by Microsoft should cause folks pause considering how they are trying to monopolize so many other spaces… & the author works on Lean. Rather than comparing Lean to performance like OCaml/Haskell like the article does, Why3 is a superset of OCaml, Agda can compile to Haskell, & ATS2 compiles to C—rather than needing to adopt an entirely new language.

Would be super dope if they brought back headphone jack Google teased Samsung over then a year later removed entirely. I haven’t even once considered GrapheneOS since I refuse to go without basic I/O.

XML works great for XMPP. KDL is compatible with it too.

What gets me is going from this structured data to Markdown which doesn’t even have enough features & syntax that the LLMs try to invent or co-opt things like the blockquote for not quoting sources.

If it’s GPL then you must care about “free software”. If that is the case, you should reconsider hosting on a fully-proprietary code forge. It requires cognitive dissonance to thing FLOSS is the right license for your project but not for your tooling/community.

You’re projecting that you would feel cognitive dissonance if you made the same choices as OP.

It’s perfectly reasonable for people to want to license their own work under a particular license without believing that everyone else should do the same, for example. Someone with that opinion, or a whole host of other positions that allow for different licenses to coexist, wouldn’t experience any cognitive dissonance.

The question then becomes what you are going to do about your cognitive dissonance. Continue to believe that “everyone else must be wrong”?

Not the same thing to compare how others should license their software versus keeping ideals consistent in your own project+tooling. If “everyone else must be wrong”, why are there continually waves of projects leaving ever since the Microsoft acquisition in particular? There’s a correlation with the kinds of projects that left too being philosophically aligned with free software & copyleft.

kitty terminal has diff like this builtin https://sw.kovidgoyal.net/kitty/kittens/diff/

I use it with

    darcs diff --diff-command="kitten diff %1 %2"

Nice, I did not know about this!

I feel Kitty doesn't get enough love, it's all ghostty this, ghostty that, but Kitty has been my top performing terminal emulator for 10 years now.

I tried looking at the Ghostty homepage & it doesn’t even work without JavaScript so you can’t use a TUI web browser.

So to signal to users that your project isn’t slop, the strongest symbol is to stop using GitHub Actions… or more easily, leave Microsoft.

Why does it need to be Git? What’s wrong with Darcs, Pijul, Mercurial, Fossil, & so on?

Wonderful. If Nixpkgs would leave, I could finally start considering deleting this account with Microsoft.

Most developers haven’t seemed to use another workflow unfortunately—& they scoff at suggesting the only workflow they know could be wrong.

Coincidentally, my most-used project is on Codeberg, & is a filter list (such as uBlock Origin) for hiding a lot Microsoft GitHub’s social features, upsells, Copilot pushes, & so on to try to make it tolerable until more projects migrate away <https://codeberg.org/toastal/github-less-social>.