Kategorie ‘Code’

Es gibt mal wieder ein Projekt...
Wer -- wie ich -- noch kein Smart Meter, sondern einen ganz gewöhnlichen elektromechanischen Stromzähler hat (Fachleute sprechen vom Ferraris-Zähler), hat nur einen recht groben Überblick über seinen Stromverbrauch. Üblicherweise wird einmal im Jahr abgelesen; wer mag, kann in kürzeren Abständen Buch führen, z.B. monatlich. Das versuche ich zwar, aber oft vergesse ich die pünktliche Ablesung, oder in der Hektik des Alltags ist keine Zeit dafür.

Da wäre es doch schön, wenn man das ganze automatisieren könnte -- und damit auch gleich die Ablesehäufigkeit stark erhöht. Martin Kompf hat dafür auf Basis eines Arduino ein Gerät entwickelt, das mir gefällt.

Das möchte ich nun auch in Angriff nehmen. Meine Wahl ist auf den Arduino MKR Wifi 1010 gefallen, der auf ARM-Basis arbeitet. Die Programmierung soll -- zumindest für die eigentliche Funktionalität -- in SPARK erfolgen.

Die ersten -- zugegebenermaßen einfachsten -- Schritte sind schon erledigt:

  • Hardware besorgt: Arduino, Shield (Extraboard) zur Datenspeicherung, externe Beschaltung (im wesentlichen IR-Emitter und Phototransistor)
  • Arduino-Entwicklungsumgebung installiert
  • SPARK-Umgebung und Toolchain für ARM installiert

Als nächstes an der Reihe:

  • Board mit Strom versorgen und per USB mit dem Rechner verbinden
  • ein einfaches SPARK-Programm ausführen
Kommentare deaktiviert für Zählen

It has taken me some time, but I have pushed my lox-spark project one step further: the code is now complete up to the end of chapter 5 in Bob's book.

Why has this taken so long, even though the new code is still unproven (i.e. the proof hasn't progressed beyond chapter 4)?

The Visitor pattern turned out to be quite​ a nut to crack. Bob has used templated accept() methods. This means a concrete visitor can choose to return whatever type it needs -- the example AST printer returns a string, but later in the book, other types might come in handy. Unfortunately, in Ada generic functions cannot be overloaded, so I couldn't copy this approach. I tried to code around this restriction only to discover I didn't really understand the Visitor pattern (which I hadn't encountered before).

After some searching, I found an Ada implementation by Matthew Heaney. He, too​, uses generics, but in a different way. The gist is that instead of returning a value, the Visitor type ("object") stores the data internally -- this is not a problem because the abstract visitor type is extended (subclassed) anyway -- and can then be queried by the caller. There seems to be a bit more boilerplate code, but most of this is written by Lox's source code generator, so this is no real problem.

The second nut stems from a shortcoming in current prover technology: Gnatprove cannot deal with aliasing (i.e. writing to one variable changes the value of another), and therefore access variables (pointers) are not allowed in SPARK. This is not as large a problem as it may seem since Ada programmers use access variables very sparingly. But the abstract syntax tree has nodes containing other nodes, so some kind of reference is needed.

I have decided to store all Exprs in a Formal_Indefinite_Vector (a container supplied by the standard library) and refer to them by their index in the vector.

I am quite satisfied with how far lox-spark has come, this is a good way to start the weekend.

What's next? Obviously, the new code needs to be annotated and proven. Also, chapter six has been out for almost two weeks, so there's still more code to be written. I haven't yet decided on where to start, so maybe I'll take advantage of git and do both in parallel.

Kommentare deaktiviert für Visited

My current pet project is coming along quite well: the implementation is complete up to chapter four (Scanning). More importantly, the AoRTE proof (absence of runtime errors) is also completely done. The only shortcomings are a handful of package bodies that are compiled with SPARK_mode => off: Ada.Command_Line and SPARK.Text_IO come to mind.

A few days ago, Bob has published the fifth chapter of his book. It is mainly about theory, and the only code it contains is a tool that generates source code for a part of the interpreter (the type hierarchy of the abstract syntax tree).

I thought about this for a while, and came to the conclusion I would not follow his path. Instead, I planned to write the types by hand. Here is why: generating source code is not really a problem, and since the generator would not be part of the final program, I would write it in plain Ada (without proving anything). The resulting code, however, would be part of the interpreter and thus needs to be proven. I could add the necessary annotations by hand, but that would defeat a big advantage of the generator: one can make changes at a high level (namely, change the input to the generator) and regenerate the sources. This is fine for ordinary languages, but it will kill my hand-written annotations.

Meanwhile, about a dozen Lox ports have appeared on github. I looked at all those I could find, but nobody seems to have written code related to the new chapter. Either the other developers have not yet found the time to implement the generator, or they, too, have their doubts.

Somehow, this lack of activity has prompted me to revise my decision: I will implement the generator, and I will generate annotations as well. After all, this project was meant to help me learn something new, and to be a challenge. But what good is a challenge unless it is challenging?

This should keep me busy in the coming days (I have not yet written any code for the generator). A quick Google search tells me that I can build multiple executables from the same project with GNAT, so that simplifies things on the organisational side.

Watch this site (or better yet, github) for updates!

Kommentare deaktiviert für Generation Lox

For some time, I've taken an interest in software engineering. With that, I mean robust software. After learning about Ada (my first project is from 2011), I haven't looked back (at C/C++, that is); Since then, I've learned a little about formal methods. So far, a few half-hearted attempts at SPARK/Ada have been the only results.

Now, I have stumbled across a project of Bob Nystrom's: He has designed a simple programming language, Lox, and is writing (and continuously publishing) a book on how to implement it. He has chosen Java and C, but quite a few folks have taken his code and re-implemented it in various languages: Alejandro Martinez (Swift), Ivan Katanic (C++), Paul Jackson (Go), Sasha Matijasic (Python).

So, why not do a SPARK port? I have some past experience with various parsers, so writing the bare code should not be that hard. Once that is done, annotations could be added and proofs done. The advantage of this project is that Bob is doing it now, chapter by chapter; I expect to follow at more or less the same pace, so if SPARKifying means I have to change something fundamental, I do not have to do that to the complete program. Instead, I can deal with problems as they crop up in the early stages.

I should add that SPARK can be used in different ways (or maybe I should say intensities). In the simplest case, only absence of runtime errors is proven. However, it is also possible to prove functional correctness at various levels: For example, one might set out to prove that a sorting subroutine actually returns a sorted list. This approach can be extended to more and more routines and eventually encompass the whole program. I do not know how far down this path I will (manage to) go, and in any case I have no idea how to prove functional correctness for a compiler.

Time will tell, I guess. Back to writing code now.

Kommentare deaktiviert für Sparkling Lox

Here's a solution for a problem I have been unable to find anything about on the net, so I would like to share it with you.
It results from a particular combination of choices that are not exactly mainstream, so it is probably quite rare:

Setup

First, I use the i3 window manager. Like many of the more usual window managers, it supports the notion of work spaces. I also use multiple monitors, and this is where i3 is different: instead of building up a huge desktop stretching over all monitors (and changing its contents via workspaces), each monitor is taken seperately; and each can be assigned one or more workspaces.You start working on a different workspace either by moving the mouse pointer, or by a key combination.

Here's where factor number three comes in: I use an absolute pointing device, namely a Wacom Intuos3. By default, the tablet maps to the whole screen area -- treating it as a single desktop,
conceptually very diferent from i3's approach.

Culture Clash

This shows: when I switch to a different screen, i3 has the ability to warp the mouse pointer, i.e. make it jump to the newly focused window. This is a nice touch for an ordinary (relative) mouse, but an absolute mouse will jump right back. You have to manually move it over.
It might seem like a good idea to switch screens using the mouse instead, but this does not work well if you need a workspace that lingers at the back of your other monitor -- you have to click on a tiny icon at the bottom. Besides, using the mouse to switch workspaces does feels wrong with keyboard-centric i3.
I ended up using a key combination and moving the mouse over, which feels redundant and annoying.

I looked for a way to confine my Intuos to just the active monitor, but have been unsuccessful until recently. Here's my setup:

Solution

First, bund workspaces to monitors:
workspace 1 output HDMI-0
workspace 2 output HDMI-0
workspace 3 output HDMI-0
workspace 4 output HDMI-0
workspace 5 output HDMI-0
workspace 6 output DVI-I-1
workspace 7 output DVI-I-1
workspace 8 output DVI-I-1
workspace 9 output DVI-I-1

Then, replace the ordinary workspace-switching key combinations by extended ones that also remap the input device:

bindsym $mod+1 exec --no-startup-id " i3-msg workspace 1; exec $HOME/bin/wacom-left"
bindsym $mod+2 exec --no-startup-id " i3-msg workspace 2; exec $HOME/bin/wacom-left"
bindsym $mod+3 exec --no-startup-id " i3-msg workspace 3; exec $HOME/bin/wacom-left"
bindsym $mod+4 exec --no-startup-id " i3-msg workspace 4; exec $HOME/bin/wacom-left"
bindsym $mod+5 exec --no-startup-id " i3-msg workspace 5; exec $HOME/bin/wacom-left"
bindsym $mod+6 exec --no-startup-id " i3-msg workspace 6; exec $HOME/bin/wacom-right"
bindsym $mod+7 exec --no-startup-id " i3-msg workspace 7; exec $HOME/bin/wacom-right"
bindsym $mod+8 exec --no-startup-id " i3-msg workspace 8; exec $HOME/bin/wacom-right"
bindsym $mod+9 exec --no-startup-id " i3-msg workspace 9; exec $HOME/bin/wacom-right"
bindsym $mod+0 exec --no-startup-id " i3-msg workspace 10; exec $HOME/bin/wacom-right"

Note the double quotes -- single quotes get messed up in some internal shell call and lead to weird error messages.
The remap scripts apply a coordinate transformation matrix that depends on your monitor setup and sizes.
#!/bin/bash -x
xinput set-prop "Wacom Intuos3 6x8 stylus" --type=float \
"Coordinate Transformation Matrix" 0.6 0 0 0 1 0 0 0 1

For some hints on how to calculate the proper matrices, see the linuxwacom wiki.

Kommentare deaktiviert für Focus

Nach meinem Systemwechsel auf dem Desktop habe ich mich mit meinem iPhone immer ein bißchen wie ein Außerirdischer gefühlt: so richtig Spaß macht es nur auf dem Planeten iTunes, und iTunes ist weit weg. Als das iPhone den Geist aufgab, lag es also nah, auch hier einen Systemwechsel zu vollziehen. Das heißt fast automatisch Android  (nur mit Jolla habe ich kurz geliebäugelt). Das erst Problem war, in der Fülle der Hersteller und Geräte etwas passendes zu finden. Gelandet bin ich schließlich beim Galaxy A3, das eine angemessene Ausstattung in einem nicht allzu großen Gerät unterbringt.
Etwas in den Abmessungen des iPhone 4 wäre mir lieber gewesen, ich habe aber nichts passendes gefunden.
Die erste große Überraschung mit dem neuen Gerät war, daß es um die Konnektivität nicht so gut bestellt ist wie gedacht. Das Android-Lager setzt genauso auf Cloud-Dienste wie die Firma Apple, und eine lokale Datensicherung oder die Verwaltung des Smartphones vom Rechner aus ist nicht vorgesehen. Zum Abgleich von Musik gibt es MTP, aber das erwies sich also so gruselig instabil, daß es nicht sinnvoll nutzbar ist.
Wenn der neurotische Kram nicht funktioniert, helfen meist Standard-Tools. In diesem Falle ist das ein Android-sshd namens SSHDroid,mit dem ich meine Plattensammlung bequem und sicher aufs Telefon bringen kann. Damit sie dort dann auch erkannt werden, ist derzeit noch ein Reboot vonnöten, ich bin aber guter Hoffnung, das noch verbessern zu können.

1 Kommentar

Rsnapshot is flawed, claims Espen.   I've stumbled upon a problem he does not directly mention: when a backup run fails, it won't be retried until (ana)cron decides to run the job again. This should not be a problem for hourly runs, but can become troublesome for the weeklies and monthlies. Even worse, cron runs might be correlated with backup failures: when anacron tends to run your backup job two minutes before you connect the external hard drive, you might be without any long-term backup while merrily retiring old hourlies.

I am convinced a better solution will consider all backup lines (including weekly and monthly runs) at each invocation (say, hourly). Here's a proposition: for each line, compare the time stamp of the most recent copy to the oldest copy in the next (more frequent) line. If the difference is sufficiently large, perform a migration.

In other words: if the oldest daily backup is more recent than the latest weekly by at least a week, call rsnapshot weekly to move that copy over.

Here's the script I use:

#!/bin/bash

TARGET=/backup/snapshots

[ -d $TARGET ] || exit 2

function invoke() {
  SERIES=$1
  PERIOD=$2
  PRED=$3
  if [ ! -e $TARGET/$PRED ]; then
    return
  fi
  if [ -e $TARGET/$SERIES.0 ]; then
    MTIME=`stat -c %Y $TARGET/$SERIES.0`
    PTIME=`stat -c %Y $PRED`
    if [ $((PTIME-MTIME)) -gt $PERIOD ]; then
      rsnapshot $1
    fi
  else
    rsnapshot $1
  fi


}

invoke monthly $((30*24*3600)) weekly.4
invoke weekly $((7*24*3600)) daily.6
invoke daily $((24*3600)) hourly.23
rsnapshot hourly

It goes into /etc/cron.hourly, and this is the only place rsnapshot is called -- no more fiddling around with half a dozen cron entries.

Edit: if e.g. rsnapshot weekly is invoked but daily.6 is absent, the oldest weekly snapshot is still deleted, so check for this.

Kommentare deaktiviert für A Better Way to Invoke rsnapshot

Inzwischen habe ich Zeit gehabt, mein EMail-Setup im Alltag zu testen und noch ein paar Verbesserungen anzubringen. Die größte Änderung ist dabei die Einbindung von procmail gewesen.

Gefiltert

Ich bin ein großer Freund von Mailinglisten, und komme allein deswegen um das Filtern nicht herum (lies: Listenmail soll in passende Ordner wegsortiert werden, um den Posteingang freizuhalten). Bei dienstlichen Mails habe ich dafür auf die etwas umständlich einzurichtenden Filterregeln des Exchange-Serers zurückgegriffen, privat Mails blieben einfach ungefiltert, weil mein Provider hier nichts anbietet. Beides ist kein haltbarer Zustand, es musste also eine lokale Lösung her.

Geliefert

Procmail ist ein Mail delivery agent (MDA), der sehr mächtige Filterfunktionen bietet (die weit über das bloße Wegsortieren hinausgehen). Diesen galt es jetzt nur noch mit offlineimap zu verheiraten. Mein erster Ansatz -- ein Cronjob, der die gesammelten Mails auf Neuzugänge durchsucht -- erwies sich als unzureichend:  viel zu leicht hat man eine exponentiell arbeitende Mail-Loop gebaut. Hier lohnt es sich gar nicht, die genauen Fehler zu suchen, denn schon das Konzept stimmt nicht: ein MDA stellt Mail zu, wenn aber offlineimap die lokalen Mails mit dem Server abgleicht, sind sie schon längst zugestellt.

Gekriegt

Ich musste also die Mail aus der Inbox des Servers erst zustellen, bevor offlineimap sie zu Gesicht bekam. Dazu kann man z.B. Fetchmail verwenden oder aber das modernere getmail. Dessen Autor hat übrigens ein paar deutliche Worte für fetchmail übrig. 

Ich habe mich dann für einen Fork entschieden, der auf meine verschlüsselte Passwortdatei zugreifen kann:

passwordeval = gpg -d ~/.mutt/pw.gpg |awk '/my_gwdg/{print $NF}' |tr -d '"'

Getmail kann die Zustellung an Procmail delegieren:

[destination]
type = MDA_external
path = /usr/bin/procmail
arguments = ("$HOME/.procmailrc.gwdg",)

[options]
delete = true
message_log = ~/Mail/getmail.log

Die Inbox liegt in der Mailverarbeitung jetzt also vor der Zustellung und ist für offlineimap tabu:

folderfilter = lambda folder: folder not in ['INBOX']

Das heißt andererseits, daß ich lokal einen neuen Posteingang brauche, damit offlineimap diesen wieder mit dem Server synchronisieren kann. Das geht mit einer passenden Zeile in der procmailrc:

DEFAULT=SPOOL/

Fazit

Jetzt word meine Mail per Getmail vom Server nur aus der Inbox abgeholt, üer procmail hefiltert und zugestellt, befor sie per offlineimap wieder auf dem Server landet, und zwar schön sortiert in Dutzenden von Ordnern -- bloß nicht in der Inbox, sonst haben wir doch woeder eine Loop. und hanz nebenbei bietet mir procmail die Möglichkeit, nach Herzenslust Mailinglist-Tags aus Betreffzeilen zu entfernen oder z.B. Mails von mir an mich gleich in Todos zu verwandeln.

Kommentare deaktiviert für Postmoderne

Jetzt ist also Firefox der letzte größere Community-Browser.

Tschüß, Camino. Es war schön mit Dir.

Kommentare deaktiviert für Another One Bites the Dust

Vor ein paar Wochen hatte ich von Gitzilla berichtet, das aus git-Commits automatisch Bugzilla-Kommentare generiert. Gestern ist mir eine neue Idee gekommen. Dazu muß ich aber etwas weiter ausholen.
Ein Rechencluster funktioniert ein bisschen wie eines von den ganz alten Rechenzentren. Dort hat man sein Programm in Form eines Stapels Lochkarten abgegeben. Wenn ein Rechner frei wurde, hat ein RZ-Mitarbeiter (Operator) den Stapel abarbeiten lassen, und das Ergebnis wurde vom Schnelldrucker ausgegeben, so daß man es sich später abholen konnte.
Heutzutage ist der Lochkartenstapel einer Datei gewichen, die Aufgabe des Operators hat eine Software namens Batch-System übernommen, und die Ausgabe landet statt auf dem Schnelldrucker auf der Festplatte -- aber das Prinzip ist gleich geblieben, interaktives Arbeiten wie auf dem PC am Arbeitsplatz gibt es hier nicht.
Unser Cluster ist meist bis zum Anschlag voll mit Jobs, aber gelegentlich sind doch einige Nodes frei -- besonders die älteren haben nicht immer voll zu tun. Weil Strom teuer ist,1 haben wir ein Lights-Out-Management, das unbenutzte Nodes abschaltet.2
Idealerweise sollte das vom Batchsystem erledigt werden, denn das ist die Instanz, die am besten weiß, welche Sorte Nodes wann in welcher Zahl benötigt wird. Die SGE kann das aber nicht, und so läuft bei uns ein externes System. Neben dem bloßen Ein- und Ausschalten nach Bedarf kann es auch noch ein paar weitere Sachen, zum Beispiel kann man defekte Nodes als "poweroff" markieren.
Das Lightsout-Management solche Nodes dann für neue Jobs, wartet ab, bis die aktuellen abgearbeitet sind, und schaltet die Node dann ab. Jetzt kann sich einer der Kollegen an die Reparatur machen -- wenn er merkt, das die Node aus ist.
Da wäre es doch schön, Lightsout und Bugzilla so zu integrieren, das eine Meldung über das Abschalten gleich in dem Bug erscheint, der für die defekte Node angelegt worden ist. Ich habe große Teile des heutigen Tages damit verbracht, eine sinnvolle Implementation dazu zu finden -- aber viel gebracht hat das nicht, außer, daß ich einiges über Web-Services gelernt habe. Die Kurzform geht ungefähr so: es gibt verschiedene Protokolle, z.B. JSON, REST, XML/rpc und SOAP. Leider unterstützt Bugzilla nur JSON und XML/rpc, für Ada habe ich aber nur eine Bibliothek für SOAP gefunden.3 Da ist wohl eine Eigenentwicklung angesagt. Look for me on Github. Mal sehen, wie aufwendig das wird.

  1. typischerweise erreichen die Stromkosten über drei Jahre Dauerbetrieb den Anschaffungspreis []
  2. und bei Bedarf natürlich auch wieder an []
  3. Und REST? Mir schwirrt schon der Kopf []
Kommentare deaktiviert für Integration II