nomeata

nomeata, 23 hours ago to random

I've implemented functional induction theorems in Lean, shipping with the upcoming version 4.8.0, and wrote a tutorial-style blog post about it:
https://lean-lang.org/blog/2024-5-17-functional-induction/
(h't to David Christiansen for the tooling behind the hover features.)
#lean #leanlang

maralorn, 2 months ago to random

Wow, I just got #arbtt capturing to run with a #wlroots based #wayland compositor (like #sway, I use #river) and it was surprisingly simple. Just run this command once per minute:

lswt --json | jq '{date:now|strftime("%FT%TZ"),rate:60000,inactive:0,windows:map({title,program:.app_id,active:.activated}),desktop:""}' | arbtt-import -a -t JSON

I have also a homegrown solution to set the inactive flag, but it’s not as pretty.

cc @nomeata

nomeata, 2 months ago to random

Prolog and FARM? This café feels like #icfp.

nomeata, 2 months ago to NixOS

I have switched from #nixos containers to a relatively simple bubblewrap script to isolate my home directory from possibly malicious stuff that could run as I am developing. It's a bit ad-hoc and not a very thorough protection, but convenient enough that I might get in the habit.

https://www.joachim-breitner.de/blog/812-Convenient_sandboxed_development_environment

nomeata, 2 months ago to NixOS

Noticed that developing with access to my personal data is dangerous, given random dependencies and auto-updating Code extensions…
Set up a nice local #nixos container for dev stuff…
Hoped to keep all tokens and keys out of it (would run git push outside that container)…
Only to notice that #Github #copilot only works with a full-access github token… sigh.

Anyways, still an improvement. Blog post to follow.

nomeata, 2 months ago to random

There might be train driver strikes in Germany soon again. I guess if I want to give my #lean tutorial at #bobkonf2024 in presence, I have to start cycling soon…

nomeata, 3 months ago to random German

Am Freitag, 1. März starte ich mit ein paar Leuten ein regelmäßiges #Comedy #standup Open-Mic in #freiburg! 19-22 Uhr im Harmoniekeller.
https://kellerkinder-comedy.de/
Seit dabei und lasst euch das Debut nicht entgehen!

nomeata, 3 months ago to haskell

#Haskell Interlude episode 42: Jezen Thomas

https://haskell.foundation/podcast/42

Jezen Thomas is co-founder and CTO of Supercede, a company applying Haskell in the reinsurance industry. In this episode, Jezen, Wouter and I talk about his experience using Haskell in industry, growing a diverse and remote team of developers, and starting a company to create your own Haskell job.

nomeata, 3 months ago to haskell

I have resigned from my post as GHC Steering Committee secretary, and wrote a little retrospective at https://www.joachim-breitner.de/blog/811-GHC_Steering_Committee_Retrospective
#haskell

nomeata, 4 months ago to random

This probably happens all over the place now, but still, the comment
https://issuetracker.google.com/issues/112096115?pli=1#comment117
made my day. #xkcd

thea, 4 months ago to random

I wrote a C0 (subset of C) to Wasm compiler in #Lean4 that can be ran in the browser. You can try it out here: https://theabrick.com/c0/

While the end goal is to completely verify it, only part of that is completed as of right now.

I am also working on tooling and other somewhat tangential features. One of these tools that I wrote that was particularly cool/interesting is a Lean inductive definition to LaTeX'd inference rule converter.

Essentially you can encode inference rules in Lean (see first image) and with minimal configuration, the tool will output a corresponding typeset inference rule (see second picture). I've posted the static semantics that I've been able to generate for C0 so far here: https://theabrick.com/c0/statics.pdf

I see this having a couple of benefits. Number one being that I think it is much easier to double check inference rules for correctness than to read lines of code (and likewise the reader doesn't need to know Lean to understand the rules). I also find typesetting inference rules to somewhat difficult and tedious, but writing them in Lean is much easier (likewise this also removes potential typos between the two different versions of the rules).

I still need to flesh out and cleanup the converter before I would consider it generally usable. I just couldn't resist showing it off right now though : ) Hopefully I will have it finished soon!

The LaTeX'd typing inference rule for variables. Similar to the Lean version, if an identifier/symbol

nomeata, 6 months ago to random

Exited to start a new job working on #lean at @leanprover tomorrow:
https://www.joachim-breitner.de/blog/809-Joining_the_Lean_FRO

nomeata, 6 months ago to github

Squashing your Github PR (if that’s what the project you want to contribute expects) is surprisingly annoying. So I created https://squasher.nomeata.de/ to do it for you. #git #github

nomeata, 6 months ago to random

Why do some project maintainers send a PR back to you as ”approved, but please merge” instead of pressing the Merge (Squash) button? Why doesn't GitHub doesn't allow branches to be squashed from the UI (and thus on the go as I get the please-squash? Why am I ranting about PR processes on Saturday night… ah, right: because that at least I can do.

nomeata, 7 months ago to random

The GHC Steering Committee has accepted Adam Gundry’s proposal to redesign the HasField type class:
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0583-hasfield-redesign.rst

sperbsen, 7 months ago to random

Aaarrglll ... es heißt nicht "dringt”, Leute, "drängt” … "DRÄNGT”!

nomeata, 7 months ago to random

Finally I can use #nix flakes in directories with spaces!
https://github.com/NixOS/nix/issues/6394
(As soon as that fix makes it into a nix release, I mean)

nomeata, 8 months ago to random

I am still utterly confused why Github Actions defaults to silently checking a synthetic merge state with the target branch, instead of just checking the state of the PR as shown under “Files”? It is super confusing if things work locally but are red in CI – or the other way around.
(Yes, without “strict merges” enabled, just checking the state of the PR is not enough either to safely merge… but that’s what strict merges are for!)

nomeata, 8 months ago to haskell

At my talk at #ICFP2023 I claimed that with observable sharing one can write a parser combinator library where left-recursion works (in the presence of sharing), and someone asked if I had, and I had to admit I hadn’t, so the next day I did:
https://www.joachim-breitner.de/blog/807-Left_recursive_parser_combinators_via_sharing
#Haskell

sandro, 8 months ago to NixOS

nix-output-monitor is recommend by Sandro: "I recommend it"

https://cdn.infobeamer.com/dynimg/blob/image

#nixos #nixcon