Having had the unfortunate experience that K-9 Mail on Android set to polling mail every 10 minutes almost caused my telephone to burn a hole in my jeans pocket I investigated the IMAP push functionality. Luckily there’s already an informative article by a fellow faced with nearly the same problem that describes how to set up a sane configuration for IMAP push using Dovecot 2. That’s all good and well, but I was still running Dovecot 1.2 on my Debian stable system. Consequently I needed to upgrade to Dovecot 2 to make the best of the situation. Luckily, this did not prove to be too big of a problem. Just add the apropriate URL from http://wiki.dovecot.org/PrebuiltBinaries to your
/etc/apt/sources.list and do what the error messages and/or warnings upon restarting the newly installed Dovecot imapd tell you (i.e., create a fresh config file that’s in line with the new options and defaults of Dovecot 2.0). So far everything works well, keeping my fingers crossed.
I’ve been using Emacs to edit LaTeX for some time now, mostly resorting to AUCTeX’s keyboard commands to insert fonts, environments and some other stuff that I need in some documents. But I’m also a big fan of yasnippet, the de facto standard for inserting more or less complex templates and, well, snippets of text into an Emacs buffer. Just now I discovered that some people have already started quite a nice collection of templates ranging from fonts to matrices to whole document skeletons for LaTeX over at github. If you are not a user of AUCTeX yet and find keyboard commands hard to deal with, perhaps this could make your day. And if you are not already using Emacs, the only true text editor for complex editing duties (for quick edits, config files, editing on remote computers, etc. I still use vim religiously), then here’s another reason to switch. 😉
BTW, the yasnippet documentation is very enlightening. For instance, I did not know that you can use the power of ELisp in your snippets to do quite amazing things automatically.
If you’ve got some time to kill I’d suggest heading over to Edsko de Vries’ presentations page where he’s collected a few slides and some notes on topics ranging from linear and separation logic to proof theoretical basics and category theory useful for functional programmers. Chances are that there will not be very much new knowledge here depending on your background but I found some of it enjoyable and useful in case I want to look something up but cannot be bothered to grab a book from the shelf and find what I am looking for myself.
There’s actually a free (as in beer) software for Mac OS X that hosts VST plugins compiled for Windows (it uses WINE under the hood). It is the editor software for the V-Machine, a rack unit that can host VST plugins. You can download it from the manufacturer’s website. MIDI input works out of the box, but there is no way to configure the audio output, so you have to use Mac OS’s own “Audio MIDI Setup” application to select the default destination. By using SoundFlower you can effictively integrate VFX and thus the Windows VST plugins into the DAW of your choice. All without a Windows installation and without paying any extra money. Enjoy the free VST plugins out there. I know I will. 😉
After a good two months of being annoyed by a burning hot MacBook Pro with short battery life, I discovered gfxCardStatus, a menu bar application that lets you choose between the integrated and discrete graphics card manually or based on whether a power adapter is plugged in. It’s free and very useful. Nicely done!
Just discovered Alfred, a free program launcher for Mac OS X (including 10.7 aka Lion), that works really well as a replacement for Quicksilver. Cool feature: Includes a calculator mode (but of course it’s not nearly as nice and feature complete as the Emacs calc mode).
Time Machine for Mac OS is actually a nice backup tool that I use religiously (and that saved my data at least once from total annihilation) since it came out. But what I did not know is that you could pretty easily use a GNU/Linux based file server to hold your backups instead of plain old hard disks or Apples proprietary hardware solutions. Unfortunately though some of the descriptions of setting up such a system you find readily on the web are outdated, so I’ll try to provide a short write-up of the necessary steps (mostly for my own convenience).
Posted in Tools
Tagged GNU/Linux, Mac OS
So, I got my diploma, got a job, and I got a Machinedrum UW mk2. That’s right, I had been lusting after one of these babies for quite some time now after having a non userwave mk1 model for a week or two some last year. It is limited and I am not sure whether it’s limited purely in a good way. Loading samples is a pain and you only get so many slots to put samples into. And don’t get me started on naming samples and kits. The user interface sometimes feels like something straight out of the 80s. And that’s probably one of the reasons why the Machinedrum is the king of the hill in its domain of purely digital sample playing (and synthesizing) x0x style drum machines: It gives you ideas and you get things done. What’s true of many “hardware instruments” is especially true of the Machinedrum in a way. I can certainly see why many people use one as part of their live setup. And once again it is proved that “You can create art and beauty on a computer.”
If you’re looking for the name of a specific (La)TeX symbol, you can draw it on the canvas of the Detexify site and maybe one of the suggestions is the desired symbol.
And if you want to look at some LaTeX snippets by searching for parts of it (or for some of the text contained in it), you can try LaTeX Search by the Springer Verlag.
Posted in Tools
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 which in Coq translates to
forall P Q : Prop, P /\ Q -> Q /\ P