Joachim Breitner

Blog

Das Mitschriebwiki zieht um

Published 2016-05-11 in sections Digital World, Deutsch.

Vor bald 12 Jahren habe ich die Webseite http://mitschriebwiki.nomeata.de/ (damals noch unter anderem Namen) ins Leben gerufen, auf der Karlsruher Studenten ihre schön geTeXten Mitschriebe ihrer Mathematik-Vorlesungen hochladen konnten. So kamen im Laufe der Jahre 35 Dokumente zusammen.

In letzter Zeit wurde es ruhig um das Mitschriebwiki, und auch ein Layout-Redesign durch meinen Bruder konnte die Seite nicht mehr mit neuem Leben füllen. (Wo teilen die Studenten heute eigentlich ihre Mitschriebe?) Da ich selbst bald aus Karlsruhe wegziehen werde, ist es nicht mehr sinnvoll, wenn die Software weiter auf meinem privaten Server läuft.

Andererseits floß dort viel Arbeit rein und einige der Mitschriebe werden auch weiterhin regelmäßig von heutigen Studenten heruntergeladen (600 Downloads dieses Jahr, 2000 Downloads letztes Jahr). Außerdem wird es an einigen Stellen im Internet verlinkt.

Daher stelle ich das Mitschriebwiki auf folgende, nachhaltige, Hosting-Lösung um:

Die Wiki-Software “latexki”, die ich eigens für das Mitschriebwiki gebaut hatte, wird dabei auch weiter verwendet, allerdings nur noch um die Ausgabedateien zu generieren – die Skripte, die es ermöglichten, im Webbrowser die Dokumente zu bearbeiten und (mit Konfliktresolution!) direkt ins SVN zu schreiben werden nicht weiter verwendet (was mich ruhiger schlafen lässt). Ich habe nicht vor an der Software noch viel zu ändern, außer dafür zu sorgen, dass sie weiter kompiliert. Ihr findet den Code auf https://github.com/nomeata/latexki

Ich möchte mich an der Stelle nochmal bei allen Mitschriebwiki-Mitautoren bedanken und hoffe, dass die Texte noch vielen weiteren Studentengenerationen eine wertvolle Hilfe ist.

Doctoral Thesis Published

Published 2016-05-09 in sections English.

I have officially published my doctoral thesis “ Lazy Evaluation: From natural semantics to a machine-checked compiler transformation” (DOI: 10.5445/IR/1000054251). The abstract of the 226 page long document that earned me a “summa cum laude” reads

In order to solve a long-standing problem with list fusion, a new compiler transformation, 'Call Arity' is developed and implemented in the Haskell compiler GHC. It is formally proven to not degrade program performance; the proof is machine-checked using the interactive theorem prover Isabelle. To that end, a formalization of Launchbury`s Natural Semantics for Lazy Evaluation is modelled in Isabelle, including a correctness and adequacy proof.

and I assembled all relevant artefacts (the thesis itself, its LaTeX-sources, the Isabelle theories, various patches against GHC, raw benchmark results, errata etc.) at http://www.joachim-breitner.de/thesis/.

Other, less retrospective news: My paper on the Incredible Proof Machine got accepted at ITP in Nancy, and I was invited to give a keynote demo about the proof machine at LFMTP in Porto. Exciting!

Tiptoi-Bastelei mit meinem Neffen

Published 2016-05-07 in sections Deutsch, Tiptoi.

Schon mit einem 4½-jährigen kann man wunderbar eigene Tiptoi-Bastelein erstellen, so wie ich gestern abend mit meinem Neffen:

Der Künstler und sein Werk

Der Künstler und sein Werk

  1. Mein Neffe durfte ein DIN-A4-Blatt bemalen, mit worauf immer er Lust hatte. Bei uns kam das Werk, das im obigen Bild am unteren Rand zu sehen ist.

  2. Dann ließ ich ihn alle Elemente des Bildes beschreiben, während ich seine Stimme mit dem Laptop aufnahm. Zwar nur mit mit dem eingebauten Mikro, aber für eine kleine schnelle Bastelei genügt das, wenn ich die Aufnahme hinterher mit Audacity laut genug mache (Ich habe das über „Normalisieren“ gemacht, bin aber nicht sicher ob dass der richtige Knopf dafür war). Da er das Werk dann zu Hause seiner Schwester zeigen will, ließ ich ihn zusätzlich ein „Hallo Schwester“ für den Anschalt-Sound sprechen.

    Meinem Neffe machte es sichtlich Spaß, seine Stimme aufzunehmen; gleichzeitig ist es eine gute Übung im deutlich Sprechen und im Hand-aus-dem-Mund nehmen.

    Das war es leider auch schon an Arbeitsschritten, an denen mein Neffe mitarbeiten konnte.

  3. Die Aufnahmen speicherte ich (22050Hz, mono, OGG) in ein Verzeichnis, und legte eine einfache YAML-Datei neffe.yaml an:

    language: de
    welcome: HalloSchwester
    product-id: 901
    scripts:
      Auto:
        - P(Auto)
      Feuerwehrhaus:
        - P(Feuerwehrhaus)
      ...
  4. Mit dem Tiptoi-Tool und dem Befehl tttool assemble neffe.yaml erstelle ich die GME-Datei für den Stift, und mit tttool oid-codes neffe.yaml die PNG-Dateien mit den optischen Codes.

  5. Ich fotografierte das Blatt Papier ab und lud das als Hintergrund in ein GIMP-Projekt mit den üblichen Einstellungen (1200dpi, A4). Die Qualität ist nicht wichtig; ich habe das nur genommen, um die Codes ungefähr zu positionieren und auszurichten. Danach blendete ich das Hintergrundsbild wieder aus.

  6. Diese Codes druckte ich auf ein leeres Blatt Papier. Dieses legte ich über die Zeichnung und hielt es gegen das Licht, um zu prüfen, ob die Codes wirklich gut ausgerichtet sind. Jene, die etwas daneben lagen, hab eich dann in GIMP noch einmal verschoben.

  7. Als alles passte, legte ich die Original-Zeichnung in den Drucker (auf die Richtige Orientierung achten!) und druckte die Codes darauf. Das geht nur einmal, also nichts falsch machen!

Achtung: Aufnahme!

Achtung: Aufnahme!

Und fertig: Eine Kinderzeichnung mit Erklärungen vom Künstler persönlich, für seine Schwester und alle seine Freunde. Alles in allem etwa 60 bis 90 Minuten, davon mehr als die Hälfte mit meinen Neffen gemeinsam.

Doktorhut

Published 2016-04-27 in sections Deutsch.

Vorgestern, am 25. April um kurz vor 16 Uhr, wurde mir aus gegebenem Anlass von meinen Kollegen am Lehrstuhl für Programmierparadigmen des Karlsruher Instituts für Technologie ein schwarzer, viereckiger Hut überreicht:

Mein Doktorhut

Mein Doktorhut

Der Tradition entsprechend ist der Hut mit verschiedenen Aufbauten versehen, die etwas mit meinen Hobbies oder meiner Arbeit am Institut zu tun haben. Im Folgenden eine Erklärung der Aufbauten, vor allem für mich selbst in 30 Jahren:

  • Ein Gleitschirm, da ich seit ein paar Jahren Gleitschirm fliege
  • Eine organene Pyramide, das Logo der Karlsruher Spielepyramide, deren dienstäglichen offenen Spieleabend ich oft besuche, und wo ich schon viele Brettspiele kennen gelernt habe
  • Tanzende Paare, da ich, seit ich vor 2½ Jahren mit dem Swing-Tanzen angefangen habe, nun mehrmals die Woche zu Kursen oder zu Socials gehe
  • Ein Straßenschild, was auf die Geschichte mit der Freierzone anspielt
  • Eine leere Knoppers-Packung. Zeitweise wurde am Lehrstuhl nach Feierabend eine Runde Enemy Territory gespielt, und eines Tages ersetzte ich ein paar der Audio-Samples des Spiels durch Aufnahmen meiner Stimme, wo statt „Tank“ oder „Bomb“ eben von „Knoppers“ die Rede war. Dank netzwerkweiter Installation des Spiels ertönte das dann auch bei all meinen Kollegen aus dem Lautsprecher. Soweit ich weiß wurde das bisher nicht rückgängig gemacht.
  • Legosteine, mit denen man Beweise im Stile der Incredible Proof Machine zusammen bauen kann
  • Eine Packung „Philadelphia – Postdocstufe“, da ich diesen Sommer als Post-Doc an der University of Pennsylvania in Philadelphia anfangen werde.

All diese Aufbauen sind per Magnet am Hut befestigt und fehlten ursprügnlich. Erst als ich mit einem Tiptoi-Stift diese Papierzettelchen angetippt hatte, und der Spruch “evaluating thunk” ertönte, wurde mir der jeweilige Aufbau gegeben – ganz im Sinne der „Lazy evaluation“, die auch im Titel meiner Dissertation steht, und selbst eine Anspielung auf meine Tiptoi-Basteleien und das tttool.

Der Zylinder des Huts ist mit Bilderrätseln dekoriert, die noch die Begriffe „Haskell“, „Isabelle“ und „Debian“ darstellten.

Zusätzlich bekam ich eine Langhaar-Perücke, mit der ich mich wieder in die Zeit vor dem großen Schnitt zurückversetzen kann, wie man auf den Bildern von meiner Verteidigung sieht.

Vielen Dank an die Bastler!

Free Paradoxes

Published 2016-02-17 in sections English, Comedy.
Maybe it works if he is a freelancer?

Maybe it works if he is a freelancer?

GHC performance is rather stable

Published 2016-02-09 in sections English, Haskell.

Johannes Bechberger, while working on his Bachelor’s thesis supervised by my colleague Andreas Zwinkau, has developed a performance benchmark runner and results visualizer called “temci”, and used GHC as a guinea pig. You can read his elaborate analysis on his blog.

This is particularly interesting given recent discussions about GHC itself becoming slower and slower, as for example observed by Johannes Waldmann and Anthony Cowley.

Johannes Bechberger’s take-away is that, at least for the programs at hand (which were taken from the The Computer Language Benchmarks Game, there are hardly any changes worth mentioning, as most of the observed effects are less than a standard deviation and hence insignificant. He tries hard to distill some useful conclusions from the data; the one he finds are:

  • Compile time does not vary significantly.
  • The compiler flag -O2 indeed results in faster code than -O.
  • With -O (but not -O2), GHC 8.0.1 is better than GHC 7.0.1. Maybe some optimizations were promoted to -O?

If you are interested, please head over to Johannes’s post and look at the gory details of the analysis and give him feedback on that. Also, maybe his tool temci is something you want to try out?

Personally, I find it dissatisfying to learn so little from so much work, but as he writes: “It’s so easy to lie with statistics.”, and I might add “lie to yourself”, e.g. by ignoring good advise about standard deviations and significance. I’m sure my tool gipeda (which powers perf.haskell.org) is guilty of that sin.

Maybe a different selection of test programs would yield more insight; the benchmark’s games programs are too small and hand-optimized, the nofib programs are plain old and the fibon collection has bitrotted. I would love to see a curated, collection of real-world programs, bundled with all dependencies and frozen to allow meaningful comparisons, but updated to a new, clearly marked revision, on a maybe bi-yearly basis – maybe Haskell-SPEC-2016 if that were not a trademark infringement.

Protecting static content with mod_rewrite

Published 2016-02-08 in sections English, Digital World.

Since fourteen years, I have been photographing digitally and putting the pictures on my webpage. Back then, online privacy was not a big deal, but things have changed, and I had to at least mildly protect the innocent. In particular, I wanted to prevent search engines from accessing some of my pictures.

As I did not want my friends and family having to create an account and remember a password, I set up an OpenID based scheme five years ago. This way, they could use any of their OpenID enabled account, e.g. their Google Mail account, to log in, without disclosing any data to me. As my photo album consists of just static files, I created two copies on the server: the real one with everything, and a bunch of symbolic links representing the publicly visible parts. I then used mod_auth_openid to prevent access to the protected files, unless the users logged in. I never got around of actually limiting who could log in, so strangers were still able to see all photos, but at least search engine spiders were locked out.

But, very unfortunately, OpenID did never really catch on, Google even stopped being a provider, and other promising decentralized authentication schemes like Mozilla Persona are also phased out. So I needed an alternative.

A very simply scheme would be a single password that my friends and family can get from me and that unlocks the pictures. I could have done that using HTTP Auth, but that is not very user-friendly, and the login does not persist (at least not without the help of the browser). Instead, I wanted something that involves a simple HTTP form. But I also wanted to avoid server-side programming, for performance and security reasons. I love serving static files whenever it is feasible.

Then I found that mod_rewrite, Apache’s all-around-tool for URL rewriting and request mangling, supports reading and writing cookies! So I came up with a scheme that implements the whole login logic in the Apache server configuration. I’d like to describe this setup here, in case someone finds it inspiring.

I created a login.html with a simple HTML form:

<form method="GET" action="/bilder/login.html">
 <div style="text-align:center">
  <input name="password" placeholder="Password" />
  <button type="submit">Sign-In</button>
 </div>
</form>

It sends the user to the same page again, putting the password into the query string, hence the method="GET"mod_rewrite unfortunately cannot read the parameters of a POST request.

The Apache configuration is as follows:

RewriteMap public "dbm:/var/www/joachim-breitner.de/bilder/publicfiles.dbm"
<Directory /var/www/joachim-breitner.de/bilder>
 RewriteEngine On

 # This is a GET request, trying to set a password.
 RewriteCond %{QUERY_STRING} password=correcthorsebatterystaple
 RewriteRule ^login.html /bilder/loggedin.html [L,R,QSD,CO=bilderhp:correcthorsebatterystaple:www.joachim-breitner.de:2000000:/bilder]

 # This is a GET request, trying to set a wrong password.
 RewriteCond %{QUERY_STRING} password=
 RewriteRule ^login.html /bilder/notloggedin.html [L,R,QSD]

 # No point in loggin in if there is already the right password
 RewriteCond %{HTTP:Cookie} bilderhp=correcthorsebatterystaple
 RewriteRule ^login.html /bilder/loggedin.html [L,R]

 # If protected file is requested, check for cookie.
 # If no cookie present, redirect pictures to replacement picture
 RewriteCond %{HTTP:Cookie} !bilderhp=correcthorsebatterystaple
 RewriteCond ${public:$0|private} private
 RewriteRule ^.*\.(png|jpg)$ /bilder/pleaselogin.png [L]

 RewriteCond %{HTTP:Cookie} !bilderhp=correcthorsebatterystaple
 RewriteCond ${public:$0|private} private
 RewriteRule ^.+$ /bilder/login.html [L,R]
</Directory>

The publicfiles.dbm file is generated from a text file with lines like

login.html.en 1
login.html.de 1
pleaselogin.png 1
thumbs/20030920165701_thumb.jpg 1
thumbs/20080813225123_thumb.jpg 1
...

using

/usr/sbin/httxt2dbm -i publicfiles.txt -o publicfiles.dbm

and whitelists all files that are visible without login. Make sure it contains the login page, otherwise you’ll get a redirect circle.

The other directives in the above configure fulfill these tasks:

  • If the password (correcthorsebatterystaple) is in the query string, the server redirects the user to a logged-in-page that tells him that the login was successful and instructs him to reload the photo album. It also sets a cookie that will last very long -- after all, I want this to be convenient for my visitors. The query string parsing is not very strict (e.g. a password of correcthorsebatterystaplexkcdrules would also work), but that’s ok.
  • The next request detects an attempt to set a password. It must be wrong (otherwise the first rule would have matched), so we redirect the user to a variant of the login page that tells him so.
  • If the user tries to access the login page with a valid cookie, just log him in.
  • The next two rules implement the actual protection. If there no valid cookie and the accessed file is not whitelisted, then access is forbidden. For requests to images, we do an internal redirect to a placeholder image, while for everything else we redirect the user to the login page.

And that’s it! No resource-hogging web frameworks, not security-dubious scripting languages, and a dead-simple way to authenticate.

Oh, and if you believe you know me well enough to be allowed to see all photos: The real password is not correcthorsebatterystaple; just ask me what it is.

Dreaming of role playing

Published 2016-01-28 in sections English.

Recently, at a summer-school-like event, we were discussing pen-and-paper role playing. I’m not sure if this was after a session of role-playing, but I was making the point that you don’t need much or any at all of the rules, and scores, and dice, if you are one of the story-telling role players, and it can actually be more fun this way.

As an example, I said, it can make sense if one of the players (and the game master, I suppose) reads up a lot about one aspect of the fantasy world, e.g. one geographical area, one cult, one person, and then this knowledge is used to create an exciting puzzle, even without any opponents.

I’m not quite sure, but I think I fell asleep shortly after, and I dreamed of such a role playing session. It was going roughly like this:

I (a human), and my fellows (at least a dwarf, not sure about the rest) went to some castle. It was empty, but scary. We crossed its hall, and went into a room on the other side. It was locked towards the hall by a door that covered the door frame only partly, and suddenly we could see a large Ogre, together with other foul folk not worth mentioning, hammered at the door. My group (which was a bit larger in that moment) all prepared shooting arrows at him the moment it burst through the door. I had the time to appreciate the ingenuity that we all waited for him to burst through, so that none of the arrows would bounce of the door, but it did not help, and we ran from the castle, over a field, through a forest, at the other side of which we could see, below a sleep slope, a house, so we went there.

The path towards that was filled with tracks that looked surprisingly like car tracks. When we reached the spot there was no house any more, but rather a cold camp side. We saw digging tools, and helmets (strangely, baseball helmets) were arranged in a circle, as if it was a burial site.

We set up camp there and slept.

It occurred to me that I must have been the rightful owner of the castle, and it was taken by me from my brother and his wife, who denied my existence or something treacherously like that. When we woke up at the camp side, she were there, together with what must be my niece. My sister in law mocked us for fighting unsuccessfully at the castle, but my niece was surprised to see me, as I must have a very similar appearance to my brother. She said that her mother forbid it, but she nevertheless sneakily takes out something which looks like a Gameboy with a camera attachment and a CompactFlash card from her mothers purse, puts it in and take a photo of me. This is when I realize that I will get my castle back.

At that moment, I woke up. I somewhat liked the story (and it was a bit more coherent in my mind than what I then wrote down here), so I wanted to write it down. I quickly fetched my laptop. My friends at the summer school were a bit worried, and I promised not to mention their names and concrete places, and started writing. They distracted me, so I searched for a place of my own, lied down (why? no idea), and continued writing. I had to to touch writing on my belly, because my laptop was not actually there.

I also noticed that I am back at the camp side, and that I am still wearing my back protector that I must have been wearing while fighting in the castle, and which I did not take off while sleeping at the camp side. Funnily, it was not a proper medieval amour, but rather my snowboarding back protector.

At that moment, I woke up. I somewhat liked the story (and it was a bit more coherent in my mind than what I then wrote down here), so I wanted to write it down. I quickly got up, started my laptop, and wrote it down. And this is what you are reading right now.

Off to bed again, let’s see what happens next.

A multitude of early Christmas presents

Published 2015-12-18 in sections English, Tiptoi, Haskell.

Today was a nice day with a surprising number of early Christmas presents:

  • I submitted my Ph.D. thesis “Lazy Evaluation: From formal semantics to to a machine-checked compiler transformation” about an Isabelle formalisation of Launchbury’s natural semantics (also found in the Launchbury entry in the Archive of Formal Proofs), about the GHC optimization “Call Arity” that I developed (see the TFP 2014 paper) and a formal proof that it is indeed an optimization (Haskell Symposium 2015 paper, AFP entry). After 243 pages, it is finally done and I can now turn to new things.

    Speaking of “something new”: I’m hunting jobs right now. I am in particular interested in academic post-doc positions in my field (functional programming languages and/or interactive theorem proving), but I’d also like to hear about attractive non-academic positions that fit my profile.

  • Someone who I value and respect a lot asked me to co-author a paper with him. I am not sure whether further details at this stage belong to a public blog post, so I’ll keep them back. But nevertheless this is very nice.

  • A paper on information flow control by my colleagues Jürgen Graf, Martin Hecker and Martin Mohr, my advisor Gregor Snelting and (although only marginally) me was accepted at POST 2016, and the notification reached us today.

  • Together with Carsten Podszun, I have written an article about the Ravensburger Tip-toi pen and how to create your own books for that using the tttool program that I have created for the German magazine Make:, and it is included in issue 6/2015, which arrived today in my mailbox.

  • The Incredible Proof Machine attracts new contributors. Well, one. But a few days ago, I heard that a 11½ year old girl has great fun with it!

  • Tonight, my group is having their Christmas party and I can expect to be fed well by home-cooked Mexican something. Got to go...

HaL 10

Published 2015-12-04 in sections English, Haskell.

Today I had the honour to hold my first invited talk: I was the keynote speaker at the tenth Haskell in Leipzig workshop. I chose to present how I used the MonadFix type class to conveniently and by-construction-correctly calculate offsets while serialising to a binary data format in the implementation of tttool. Johannes Waldmann could not resist to point out that MonadFix was already a topic at the very first HaL meeting nine years ago, but nevertheless I think that my live-coded slide-less talk was quite suitable for the given audience of roughly 55 attendees.

I have uploaded a transcript of this talk.