fun with dependent types

reading and searching gmane with gnus, fast

Reading mailing lists via Gnus by pointing it to the usenet service news.gmane.io is a well-known trick among emacsers. It has a couple of drawbacks, though: network latency and no search. The two problems have, as almost always with almost any problem in Emacs land, a cure. The names of the game are, in this case, leafnode and notmuch.

reading source code is fun

From a recent checkout of the Emacs source code:

;;; desktop.el --- save partial status of Emacs when killed -*- lexical-binding: t -*-

;; Copyright (C) 1993-1995, 1997, 2000-2021 Free Software Foundation,
;; Inc.

;; Author: Morten Welinder <terra@diku.dk>
;; Keywords: convenience
;; Favorite-brand-of-beer: None, I hate beer.

;; This file is part of GNU Emacs.

Mine is Guinness :)

notmuch queries via consult

This package provides notmuch queries in emacs using consult. It offers interactive functions to launch search processes using the notmuch executable and present their results in a completion minibuffer and, after selection of a candidate, single message and tree views.

simplicity pays off

i've been using Bastian Bechtold's org-static-blog for this blog for more than a year now. Back in the day, i mentioned how well it integrated with my emacs workflow and how its simplicity was a big asset¹.

consulting hunks

I use Dmitry Gutov's diff-hl to highlight (with fringe marks) modified hunks in my files under git revision control. The package comes with a command, diff-hl-next-hunk, that one can use to navigate them. So, taking a peek at consult-lines, it was straightforward to put together a consult function to navigate, with completion and preview (although i disable the latter) the hunks in the current file:

consulting spotify in a better way

After my latest adventures writing a small spotify library and learning in the process a bit more about consult, its author, Daniel Mendler, was kind enough to comment on how i had implemented the asynchronous search using consult's API, showing me better ways.

an emacs packages hat trick

i've found these last days a handful of really useful little emacs packages:

an even better video wharf

A couple of days ago, i was writing about embark and my first experiment defining a new embarking to play remote video streams. Omar Antolín Camarena, embark's author, has been kind enough to not only read it, but comment on a couple of significant improvements that i think well deserve this follow-up.

embarking videos

Inspired by Prot's musings on completion, i've, ahem, embarked in a reconsideration of my completions setup (as you might have intuited from my recent experiments with the spotify API and consult). As it happens, i'm starting to feel quite at home with a combination of selectrum, prescient and consult, and the ideas to augment what i have with contextual actions using embark seem really natural to me.

consulting spotify

Note: you can tangle this file (e.g., with C-c C-v t inside Emacs) into three elisp packages, namely espotify.el, consult-spotify.el, and ivy-spotify.el.

what's not to like

I've just discovered Codeberg, a code hosting site that, finally, has let me create a user with plain emacs-w3m, shows me content reasonably well there, with a refreshingly uncluttered layout, handles graciously org files (why, it's even generating a table of contents for me), has a good privacy policy, it's not under the wings of any corporation and had my preferred username free for grabs.

appius and virginia

two decades of gnu mdk

I've just published GNU MDK 1.3.0, its 28th release, which finally migrates MDK's graphical user interface to GTK+ 3, to keep up with the, ahem, not-so-modern times and see to it that MDK keeps alive for at least another decade or two.

the simulacra

exhalation

xmobar: a battery trick

i've been maintaining xmobar for more than a decade now, and i still use it daily and tweak it almost as often. With almost a hundred contributors besides myself, and many bugs to solve, i am always learning new things. The latest one, that font awesome thing everyone seems so fond of.

this is shakespeare

the mode lines i have not seen

i don't dislike emacs' mode line, i just wish (possibly out of a fetish for simplicity and minimalistic user interfaces) sometimes it wasn't there.

unlearn

For years, i've been using C-x p, C-x o and C-c <n> to move to other windows, but with ace window i am substituting all of them with M-o. Problem is, muscle memory interferes and i find myself clumsily moving around (and often lost) with the former ones. Or i did, before i followed an advice from Stefan Monnier in emacs-devel: unbind those keys you want to forget, and you'll get an error when you relapse.

ace window

As i've mentioned in a previous post, i organise my emacs sessions in workspaces, a.k.a. frames, a.k.a. a thematic tiling of windows. It is therefore important to have quick ways of jumping from a window to another. Until very recently, i used a home-cooked collection of shortcuts (C-c 1, C-c 2 … C-c n) that would move my point to the nth window in the workspace (i trained myself to count them quick enough, i suppose), and used that together with the stock C-x o and with C-x p bound to (other-window -1), for something similar to "previous window", to move around. But i've discovered a better way.

a gnus enters a side-bar

i typically organize my computing sessions around workspaces, which in emacs are simply glorified default window configurations, sometimes in a one-to-one relationship with emacs frames¹. That's specially natural if you use exwm, where there's a concept of workspace essentially equivalent to emacs frame. So here too i'll have a "coding" workspace with programming buffers, a "browsing" one inhabited by emacs-w3m buffers in a two-pane layout, an "X" for the few non-emacs applications i use, and one devoted to "email/calendar/agenda", where Gnus plays a central role.

observatory

i've been learning a tiny bit about web security at mozilla's Web Security pages, and used their Mozilla Observatory to analyize this site and make it a bit safer. it was just a matter of adding a handful of headers to the webserver configuration, to wit:

transient

Emacs being, essentially, my operating system and window manager, i've had since i remember a set of keybinding maps grouped by functionality (sleep and related operations, media player control, network access, and so on), whereby every group of commands starts with the same prefix. E.g., all my commands controlling media have a keybinding starting with `C-c m`. Nothing earthshaking, and pretty common. Recently, the transient library has made my life easier in this department.

dancers at the end of time

imagine

Posted to comp.lang.scheme on January 17, 1996, for Scheme's twentieth birthday.

literate programming

I got started with literate programming many years ago, out of admiration for almost everything else i knew done by Donal Knuth, and tried my hand at it in some toyish projects in OCaml and Scheme. So it wasn't without lack of enthusiasm that i plunged into the literate world.

signel, a barebones signal chat on top of signal-cli

Unlike most chat systems in common use, Signal lacks a decent emacs client. All i could find was signal-msg, which is able only to send messages and has a readme that explicitly warns that its is not a chat application. Skimming over signal-msg's code i learnt about signal-cli, a java-based daemon that knows how to send and receive signal messages, and how to link to a nearby phone, or register new users. And playing with it i saw that it can output its activities formatted as JSON, and that offers (when run in daemon mode) a DBUS service that can be used to send messages.

simplicity

I like simple things. As simple as possible, but not simpler: they should live well in my little emacs universe. Bastian Bechtold's org-static-blog, a static site generator using org-mode, is the latest star in that virtual world.

gödel's incompleteness illustrated

I am having a great time reading Smullyan's Gödel's Incompleteness Theorems, a thin volume with the most elegant description of Gödel's and Tarski's work i've read so far. It's also the most succint, and it starts with a very nice and very clear demonstration of indecidability that is the simplest i have ever seen. I like it a lot, and it's short enough for a quick blog post. Here it goes.