Me, a year ago or so:
Cool, I can teach termux to use an SSH key protected by the android hardware and unlocked by my fingerprint. No more passwords!
Me, today, at #gpn, trying to log into my server to play tron:
Termux-API since stopped working on Android 14, so no access to any SSH key, so no tron playing.
No wonder passwords never die.
I managed to access my server using the virtual console at the Hetzner cloud web interface, and because I luckily enabled "password less root shell on the local console" a while ago.
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.
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!
@thea@andrejbauer the branch at https://github.com/Wasm-DSL/spectec/pull/2 contains a working Lean formalization of the typing and evaluation relation generated from that Wasm spec. It's unfortunate it's not yet available on the master branch since a long while… but eventually I hope it will be, and then projects like your's can choose to target “the” official Wasm spec within lean, including compatibility with all the hopefully myriad of other wasm-related formalization projects.
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.
@angerman And writing a Github App is silly in the sense that it could be a purely static page running only in the user’s browser, if Apps didn’t need secrets. Now I’d need to host it somewhere.
@sandro I’m just amused to see this backed by infobeamer, which was a project that began for the yearly CCC Karlsruhe event a long time ago, and I think I even contributed back then. Good to see it pop up in another context!
Packing for the flight towards #ICFP23, I wanted to warm up my nix store for a few select projects, when I get “no more disk space“ despite the partition being only 70% full – the dreaded no-more-inodes problem. So now running nix store --gc, and hope I remember to re-enter all relevant nix shells once before the flight. I think #lean ’s (experimental) one-dervation-per-file nix support and me recompiling #mathlib a few times recently is partly to blame…
@raito I googled “best file system for nix store” a few times in the past, but got nothing conclusive out of it. It would be great if the official docs would give a clear recommendation for those who just want to be told what to do.
#haskell q: are there any small and living haskell implementations with power at least partially close to ghc? (e.g., vectors, concurrent IO and TyFams)
@EyalL yes, if the code you import avoids punning (use of the same name in both namespaces), you would not need such qualifiers. But if the code you import is not written with this in mind, it helps to bridge the gap.
It seems counterintuitive that Nix -- a culture which values reproducibility of software builds much higher than packager and maintainer convenience -- is also the distribution with the highest number of maintained packages, and, of those, the most up to date ones.
But this echoes my experience with testing culture. If you set the bar high enough and the goal is worthy (e.g. "100% unit test coverage is necessary but not sufficient"), motivated people will come out of the woodwork.
@chrism It might also be a consequence of the all-in-one-repo and no-maintainer-fiefdoms design, making packaging significant more efficient. And little things like not maintaining per-package changelogs.
Reminder that the only safe dummy domains to use are:
example.com
example.net
example.org
And nowadays there's also a safe dummy TLD: .example
These are safe because they are reserved by IANA as as special-use domain names for documentation purposes on direction of IETF in RFC 2606 and RFC 6761.
Any other domain can be registered and as such should never be used as a dummy domain for documentation or as eg. an example in default configs.