Thunderlink is a fantastically useful add-on for the Thunderbird mail user agent. It lets you create links to email that you can put into all sorts of documents (like ToDo lists or notes). The links use the URI scheme thunderlink that needs to be handled by whatever mechanism you use …
read moreOther articles
Make Firefox play embedded MP4 videos
For some reason (at least on Mac OS X and according to a quick search also on other platforms) Firefox does not play MP4 videos embedded into websites using the
<video>tag. Seems that enabling the two config optionsmedia.fragmented-mp4.enabledandmedia.fragmented-mp4.exposedfixes the issue.
read more
vim-like ctrl+v enter in Emacs
Suppose you have a list like this
foo, bar, baz, quuxin your Emacs buffer, but you’d rather have one element per line like this
foo bar baz quuxWhat to do? In vim this is easy:
:%s/,/^M/gwhere ^M is inserted using
Ctrl+vBut what …
read moreDevelopment environment for the STM32F4DISCOVERY board on Mac OS
This is just a quick post with information on how to get up and running with a development environment for the STM32F4DISCOVERY evaluation board which is a cheap and fun way to get started with developing software for ARM microcontrollers.
First, you need to install the development toolchain. I use …
read moreThunderbird line breaking behaviour
Because I keep forgetting which options to set to force Thunderbird to send and display line breaks instead of flowed plain text emails that may or may not come out right at the other end (usually those emails exhibit unsightly long lines which among other things might make quoting from …
read moreSnippets for LaTeX + Emacs users
Several ways to prove a simple proposition
Coq provides many tactics. In this post we show a number of proofs that use different tactics to prove a simple proposition of first order logic, namely \(\forall P\;Q,\, P \wedge Q \rightarrow Q \wedge P\) which in Coq translates to
read moreforall P Q : Prop, P /\ Q -> Q /\ P …Using Qucs for filter design
Qucs, short for Quite Universal Circuit Simulator, is as the name suggests a simulation package for electronic circuits. It's free and sports a nice graphical schematic capture interface. One of its many nice and useful features is the ability to write equations so you can calculate all kinds of stuff …
read moreBeginning Ltac
One of the strong points of Coq is its powerful proof automation facility embodied in the tactic language \(\mathcal{L}_{tac}\). Instead of having to write new tactics in ML, compiling them, and jumping through all sorts of hoops in the process, we can simply write down new tactics …
read moreHow to draw commutative diagrams in LaTeX with TikZ
Sooner or later everyone who uses LaTeX to typeset documents containing maths will encounter the problem of how to draw commutative diagrams. There are many packages, some general purpose other specialized for the task. An excellent survey of some of these alternatives by James Milne can be found here.
I …
read moreAnother script font for LaTeX
Doepfer MCV4 MIDI to CV interface editor in Max
A little Max patch for changing the parameters of a Doepfer MCV4 MIDI to CV interface I made a while ago. It's not extensively tested, but seems to work so far. The user interface is in German, but I guess everything is pretty self-explanatory and obvious even if you don't …
read moreThe Maybe monad in Coq
The Maybe monad is pretty useful whenever you're dealing with partial functions, especially in a language like Coq (or rather Gallina if you want to be exact) which requires all functions to be total.
The first idea is a to lift the codomain of a partial function \(f : A \rightharpoonup …
read more