Breaking recursion in Python and fix-ing it back up again

Trying out github repos for what started off as a blog post, on how fixpoint combinators relate to Python:

https://github.com/benclifford/python-fixpoint#readme

berlin strava openstreetmap mashup

I made a mashup (so last decade) of my strava rides since I've been in Berlin.

You can see it here: http://www.hawaga.org.uk/ben/berlinmap/.

It uses leaflet.js to draw the map, Open Street Map to provide the base street map, Strava on my phone to record my rides, and jpravetz' strava CLI to get the data out of Strava and into a file.

commandline editing for zoom meetups

In the last year, I've helped host a bunch of meetups and conferences on Zoom. We've recorded them, and I wanted to turn each talk into a separate YouTube video.

Zoom can give you a giant MP4 of the whole session, and I wanted to cut that video into pices.

A few times, I tried using OpenShot but: my laptop struggled to cope with the load; the UI was focused on more interesting editing than what I wanted; that UI isn't natural for me, who spends 99% of my time not using editing software.

I figured out a workflow that worked better for me:

• Use VLC on the giant MP4 to quickly identify the start and end times for each talk.
• Make an ffmpeg command line for each talk, for example:

  ffmpeg -i day1.mp4 -ss 2:31:54 -to 2:47:07 day1-7-madany.mp4
  ffmpeg -i day1.mp4 -ss 2:47:16 -to 2:57:46 day1-8-foster.mp4
  ffmpeg -i day1.mp4 -ss 2:58:17 -to 3:13:10 day1-9-glanzman.mp4
  ffmpeg -i day1.mp4 -ss 3:13:34 -to 3:23:42 day1-10-ward.mp4
  ffmpeg -i day1.mp4 -ss 3:24:02 -to 3:33:22 day1-11-reynier.mp4
  ffmpeg -i day1.mp4 -ss 3:45:52 -to 4:13:18 day1-12-clifford.mp4
  ffmpeg -i day1.mp4 -ss 4:15:17 -to 4:55:14 day1-13-shaffer.mp4
    

  which will copy ranges out of `day1.mp4` in to the named file.
• Then, let this run. It's quite slow on my laptop but doesn't need any human interaction.

A1120EUA Hall Effect Switch vs Pi Zero W

I'm building a bike-wheel LED project that wants to know how fast the wheel is turning, and what position it is in as it spins.
Got A1120EUA-T from hobbytronics
turns out you can't set pullups from sysfs (/sys/class/gpio) ... so i'll have to install wiringpi for the gpio command.

$ gpio export 0 in
$ gpio mode 0 up

and now I can wave my neodymium magnets nearby (about 1.5cm) and see the input go low as it passes by.

$ while true; do gpio read 0 ; done
1
1
1
0

`stg uncommit` the first commit

I wanted to edit the first commit of a repository using `stg`. (Actually I wanted to edit all of them, which was easy except for the first).

`stg` doesn't like this:

$ stg uncommit -n 1
Uncommitting 1 patches ... done
stg uncommit: Trying to uncommit 38a035a7667c9417e10a4f53e7c88a57711ca440,
              which does not have exactly one parent

... the root commit is not formed in the way that `stg` wants.

I worked around this by:

1. making a new empty commit in a new repo:
   

   mkdir ~/empty-repo
   $ cd ~/empty-repo
   $ git init
   $ git commit -a --allow-empty -m "Empty initial commit"
   [master (root-commit) 38a035a] Empty initial commit
   

2. getting that empty commit into my real repo ...

   $ cd ~/real-repo
   $ git remote add empty-repo ~/empty-repo
   $ git fetch empty-repo
   

3. cherry picking the original root commit on top of the empty commit ...

   $ git tag tmp1
   $ stg pop -a
   $ git reset --hard empty-repo/master
   $ git cherry-pick tmp1
   

4. and now this cherry-picked originally original commit can be `stg uncommit`ted:

   $ stg uncommit -n 1
   

temporary merge tool

I've been an enthusiastic user of stgit for some time. This lets you work on a series of commits at the same time, so that you can edit them to look good before sending them out into the world (i.e. pushing upstream). You can move up and down a series of git commits making changes to them, rather than adding new commits onto the end of a branch.

One use I often make of this is preparing a bunch of orthogonal patches: patches which don't interact with each other or need to be applied in a strict order, but that I want all applied at once while I'm making day to day use of my software, so that I can test the changes in real use.

It's pretty awkward (i.e. impossible) to do this collaboratively though: all of git's support for collaborative work is by making new commits onto the end of branches, not editing earlier commits.

So I have been trying a new workflow: lots of features branches at once, instead of lots of stg patches; with a script I wrote, tmt, which makes your checkout look like the merge of all of those feature branches, but lets you commit your changes onto one specific feature branch.

Here's the repo, with a README. Yes, it's Haskell. Of course. https://github.com/benclifford/tmt

sous vide

I built a sous vide cooker, driven by a PWM/PID controller written in Erlang.

Then I gave a talk about it (and some other related temperature control that I've done) at a Raspberry Pi meetup.

Here's the video (login required) and here are the slides.

Build a Crap Web Form in Haskell in 28 days.

I've been writing an informal series of posts about a small scout camp registration system that I've been building:

Build a Crap Web Form in Haskell in 28 days

Yellow Pages for Modern Times

Early on in my career it was pretty common to use clusters comprised of a pile of heterogeneous unix systems: some Sun boxes, some Linux machines, maybe IRIX and AIX in there too.

The thing that made them into a single cluster was that your user account existed on them all, and you had the same home directory on them all: make files on one machine, and they're visible on the other machines; but you still had access to the machine specific features of each host.

The technology of the time often used Network File System (NFS) and Network Information Service (NIS) (formerly known as Yellow Pages, with that name living on in the yp prefix of commands like yppasswd).

Fast-forward a decade or two and things look different: virtual machines are thing now, and more recently, containers. It's now very common to custom build a virtual machine or a container, both with something approximating an entire OS, specifically for running one application, or for running just a single piece of one application.

So maybe you'd connect these pieces - virtual machines or containers - with some kind of socket connection: a web front end exposing HTTP and talking to a PostgreSQL database in another container with no shared files between them.

I did a bunch of stuff this way, and it was great: you can install separate package stacks in isolation from each other. Want this weird version of a library or compiler? Or to run some curl | sudo script without messing up the rest of your system? Or stick with an old distribution of your OS just for one tool? Easy.

But it was a pain getting getting files between different places. Got my text editor and version control set up in one place, but need to compile in another? There are all sorts of different ways to get files between those places: for example, commit regularly to version control; or rsync.

Docker running on one host has options for mounting pieces of the host file system inside containers; but I lacked a good idea of what to mount where.

It was all so simple before: you had ~ everywhere, and nothing else.

So I started using the unix cluster model, described at the top of this post, to guide how I set up a lot of my containers and virtual machines.

The actual technology (NFS, docker volume mounts, YP, LDAP, HESIOD, ...) isn't massively relevant: I've used different mechanisms in different places.

What really matters is: all the (regular human) users get their home directory, mounted at the same place (under /home).

Pretty much with most ways of sharing files, that means the unix user id for that user should be the same everywhere too.

I've implemented this basic model in a few different ways: for a couple of VMs inside the same physical server, a traditional NFS and OpenLDAP setup (NFS for file sharing, LDAP for distributing account details) which is a more modern replacement for NFS/NIS; on my laptop and some of my physical servers, I've got a wrapper around docker called cue which creates exactly one user (the invoking user) inside the container, and mounts their home directory appropriately; I have some ad-hoc docker server containers (eg inbound SMTP) where the whole of /home is volume-mounted, and then OpenLDAP is used to share accounts.

There are plenty of downsides: for example, your whole home directory is accessible in more places than it needs to be and so is more vulnerable; you can't access files outside your home directory, so ~ is now a specially magic directory; posix filesystems work badly in distributed systems. For lots of what I want, these downsides are outweighed by the upsides.

One twist that doesn't happen so much with a cluster of physical machines: a server such as a mail server is now a container which has a mail queue which I want to persist across rebuilds. Rebuilding would be unusual in the physcial machine model because you don't usually rebuild physical servers often. So where should that persistent data go? Inside a specific /home directory? in a /container-data directory that is mounted too, like an alternate version of /home? What user-id should own the queue? Different builds of a container might assign different user-ids to the mail server.

A string of DNS protocol bugs.

I went to turn on DNSSEC for cqx.ltd.uk today - the server that signed it broken right before my Christmas busy period so I disabled DNSSEC on that zone until I got round to fixing it.

I've encountered three different apparent protocol implementation bugs in the space of a few hours:

• Andrews and Arnold's web based control panel accepts DS records as generated by BIND's dnssec-keygen tool but then throws a complicated looking error when talking to Nominet, the UK domain registry, to put those records where they need to be. As far as I can tell, this is because the BIND output has whitespace in the middle of a hex string, something RFC 4034 s5.3 seems to think is acceptable. Why is installing crypto keys always so hard?
• For a while, Hetzner's recursive resolvers were unable to verify (and therefore refused to answer) results for my zone. I have a suspicion (but I don't have much to go on other than a hunch) that this was something to do with DS records and the actual zone having some kind of mismatch - although Google Public DNS at 8.8.8.8, and Verisign's DNSSEC checker both worked ok.
• I discovered an implementation quirk in the Haskell dns library, which I use inside a debugging tool I'm slowly building. This is to do with the mechanism which DNS uses to compress replies: where a domain name would be repeated in a response, it can be replaced by a pointer to another occurence of that name in the reply. It looks like in this case that the dns library will only accept those pointers if they point to regions of the reply that have specifically already been parsed by the domain name parsing code, rather than pointers to arbitrary bytes in the reply. This is frustratingly familiar to another bug I encountered (at Campus London) where their (not-so) transparent firewall was reordering DNS replies; giving a bug that only manifested when I was sitting in their cafe. (github issue #103)

findmnt

One of my customers uses cPanel to administer their internet facing servers.

It has an interesting virtual filesystem setup for sandboxing user accounts: cPanel creates, per user, a new root filesystem for that user, and then chroot into that before running user code (shells, php, ...).

To create that file system, cPanel uses bind mounts to make the root-jail file system look very much like the real root file system.

bind mounts are a thing that appeared after the 1997-era of me spending a lot of time learning Linux. (if it was invented post 2000, lol I've never heard of it)

In the intervening years, isolation techniques like this have been becoming more mainstream - for example, my main use of docker (via my tool cue) has been to prepare and use different root file systems.

Anyway, back to cPanel. I was trying to figure out how this virtual filesystem was constructed. Bind mounts don't appear in the output of mount or df or /proc/mounts with all the information I wanted: the mount just shows are being from the same device that its target is, without saying where that target is.

For example, I can see that /home/virtfs/x/usr/sbin goes to somewhere in the filesystem on s_os-lv_root but not where. (I can guess it's /usr/sbin in this case).

/dev/mapper/vg_os-lv_root   50G   21G   30G  41% /home/virtfs/x/usr/sbin
/dev/mapper/vg_os-lv_root   50G   21G   30G  41% /home/virtfs/x/var/spool
/dev/mapper/vg_os-lv_root   50G   21G   30G  41% /home/virtfs/x/etc/apache2
/dev/mapper/vg_os-lv_root   50G   21G   30G  41% /home/virtfs/y/usr/sbin

Anyway, surely this can't be the way things are??

So along comes findmnt, which gives me this info:

...
│ │ ├─/home/virtfs/x/usr/sbin     /dev/mapper/vg_os-lv_root[/usr/sbin]
      xfs         ro,relatime,seclabel,attr2,inode64,sunit=512,swidth=512,usrquota
...

... which tells me that yes that really is mounted from /usr/sbin.

Anyway, a nice new command to discover, around since only util-linux v2.18 in mid 2010.

Infrared Raspberry Pi

When I ordered my Pi Zero W with a no-IR-filter camera, I also ordered a single infrared LED. This was enough to prove that I could illuminate things with IR, but not really good enough for more than a small dot of light.

So, then I ordered 50 x £0.04 infrared LEDs from RS (which arrived overnight!) and wired them up yesterday onto a single breadboard powered by a regular USB 5v power supply. You can see the layout in the first picture.

Here's a scene: the first with natural light showing the LEDs on a board, and the next two with infrared illumination. The two infrared scenes appeared almost pitch black to a human eye.

And then I set it up overnight, with a timelapse video of myself sleeping:

Unix exit codes as an indicator of tooling (im)maturity.

If your compiler for your new language, or your test running, or whatever, doesn't return a unix exit code when it exits with an error - that's something that annoys me - and it's an indicator that no one is using your tool for serious - for example in an automated build system.

I've hit this a couple of times at least in the last year. grr.

Pattern matching in Idris `do` notation has surprising reliance on type checking the action.

Idris is syntactically quite Haskell-like, and especially it has do notation for sequencing "actions".

Like (traditional) Haskell, do blocks are desugared to a sequence of >>= (bind) operators. But, unlike (traditional) Haskell, that >>= is not always the monadic >>= : m a -> (a -> m b) -> m b. (This can also happen in Haskell using rebindable syntax)

In Idris, you can use different "better-than-monad" types to statically (at compile time) reason about a computation beyond using the monad laws. For example, an effect system might track which effects are in scope.

Total parsing

In the case of Text.Parser (in the Idris contrib/ package) the type signature of actions (Grammar _ _ _ indicates whether a parser consumes any characters so that the compiler can tell if a parser might loop forever. (see http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.html)

I was trying to write a new JSON parser for idris-todaybot using Text.Parser. Previously JSON was parsed using lightyear, but Text.Parser has more gratuitous dependent types so was an obvious way to proceed.

A problem.

I ran into a surprising compile error which initially made no sense to me at all.

This code compiles:

objectValuePair : Grammar Char True (List Char, ())
-- definition elided

jsonObject : Grammar Char True (List Char, ())
jsonObject = do
  llll <- objectValuePair
  pure llll

where llll is a tuple; but the following version of jsonObject, which desconstructs that tuple and reassembles it, does not compile:

jsonObject : Grammar Char True (List Char, ())
jsonObject = do
  (k,v) <- objectValuePair
  pure (k,v)

It gives this error:

When checking right hand side of Main.case block
in jsonObject at bug-bind.idr:55:14 with expected type
        Grammar Char c2 (List Char, ())

Type mismatch between
        Grammar Char False (List Char, ()) (Type of pure (k, v))
and
        Grammar Char c2 (List Char, ()) (Expected type)

Specifically:
        Type mismatch between
                False
        and
                c2

Another attempt to deconstruct llll also fails:

  jsonObject : Grammar Char True (List Char, ())
  jsonObject = do
    llll <- objectValuePair
    let (k,v) = llll
    pure (k,v)

but the following deconstruction by function application rather than pattern matching succeeds:

jsonObject : Grammar Char True (List Char, ())
  jsonObject = do
    llll <- objectValuePair
    let k = fst llll
    let v = snd llll
    pure (k,v)

That type error

Let's dig into that type error:

Type mismatch between
        Grammar Char False (List Char, ()) (Type of pure (k, v))
and
        Grammar Char c2 (List Char, ()) (Expected type)

Grammer _ _ _ is the type of parser actions, where the first parameter Char is the type of symbols we're consuming, the final parameter (List Char, ()) is the type that the parser will return on success, and the middle parameter (False or c2) represents whether the parser will definitely consume input (True) or might succeed without consuming anything (False - for example, a parser which removes whitespace, or pure which never even looks at the input stream).

This "consumes" parameter contains the main novelty in Text.Parser beyond monadic parser combinators: Text.Parser combinators manipulate and use this value at compile time to help check that parsers really will consume things: for example, a parser that definitely consumes followed by a parser that might not, results in a parser that definitely consumes; while sequencing two parsers that might not consume results in a parser that might not consume. (See: the source)

So what on earth has this parameter, manipulated by >>=, got to do with pattern matching pure values after they've already been returned by an action?

Desugaring

It turns out we can forget that our troublesome tuple is being returned from an action; let (a,b) = (1,2) breaks in the same way when run inside a Text.Parser do block.

Let's (very roughly) desugar some of the examples above, and then look at the types involved:

jsonObject : Grammar Char True (List Char, ())
jsonObject = do
  llll <- objectValuePair
  pure llll

-- becomes:
jsonObject = objectValuePair >>= (\v => pure v)

jsonObject = do
  (k,v) <- objectValuePair
-- becomes: 
    objectValuePair >>= (\(k,v) => pure (k,v))
-- becomes: 
    objectValuePair >>= (\llll => case llll of
      (k,v) => pure (k,v)
     )

So in the second fragment, there's an extra case expression in there to deconstruct llll using pattern matching.

Apparently that gets in the way of type inference/checking:

• On the one hand, that pure has type: Grammar Char False (List Char, ()) - false because it may (actually, will always) succeed without consuming input.
• On the other hand, >>= doesn't care whether the right hand side consumes or not - it will take either, as shown by the compile time variable c2 appearing in the error message.

Idris doesn't manage to unify c2 = False.

With further pinning of types using the, an uglier form of pattern matching does work:

export jsonObject : Grammar Char True (List Char, ())
  jsonObject = 
   do
    llll <- objectValuePair
    the (Grammar Char False (List Char, ())) $ do
        let (k,v) = llll
        pure (k, v)

Ugh

Thanks

Thanks to Melvar on #idris for explaining this.

highlight.js in blogger

Syntax highlighting is pretty. highlight.js can do it in a browser. I just added it to this blog.

1. In Blogger, click "Theme" then "Edit HTML"
2. Find the <head> section of the theme.
3. Insert the following at the end, before the closing <head> tag:

   <link href='//cdnjs.cloudflare.com/ajax/libs/highlight.js/9.12.0/styles/default.min.css' rel='stylesheet'/>
   <script src='//cdnjs.cloudflare.com/ajax/libs/highlight.js/9.12.0/highlight.min.js'/>
   <script src='https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.12.0/languages/haskell.min.js'/>
   

4. Add as many copies of the third line as you want, modifying haskell to the additional languages that you want to be able to highglight.
5. When writing code, wrap it in <pre><code class="haskell"> YOUR CODE </code><pre>

Raspberry Pi Zero W + cam timelapse

I got a Raspberry Pi Zero W and a camera module.

I wanted a timelapse video.

This is how I did it:

Capture a sequence of image frames

This will capture a sequence of images (forever) approximately every minute, with the filename being a unix timestamp.

while true; do raspi-still -o $(date +%s).jpeg ; sleep 60s; done

Leave this to run for as long as you want to collect frames, and you'll end up with a bunch of numerically named files, like this:

$ ls
1504014800.jpeg
1504014866.jpeg
1504014931.jpeg
...

Combine the sequence of image frames into a jpeg

After you've got all the frames you want, use ffmpeg to join the frames together. I do this on a different Linux box (my laptop) but you should be able to do it on the Pi too.

First make a command file listing all the jpeg files:

ls *jpeg | while read a ; do echo file $a; done > e.cmd

Next, feed that command file into ffmpeg to generate a video:

ffmpeg -f concat -i e.cmd -b:v 1500000 -r 24 -c:v libx264 e8.mp4

As a result, the output video should be in e8.mpg which is in a form suitable for playing with vlc or uploading to YouTube.

An income tax explorer, using R and Shiny

I got carried away with my R code for plotting income tax rates, and now it is an interactive webapp https://benc.shinyapps.io/r-income-tax/ using Shiny, a web framework for turning your R code into a website. Thanks Tom Nielsen for convincing me (in this talk about making a Haskell port of Shiny) to try it out.

A first project in R / UK income tax graphs

The UK income tax system has a progressive tax rate that gets higher as your income is higher. However it has a few quirks. I've been meaning to graph the effective rates, and today I felt like learning a bit more R to do it. I've included income related student loan repayments and National Insurance because they are, to some extent, income-tax-like.

The code at https://github.com/benclifford/r-income-tax can generate the following three graphs:

Marginal income tax rates, coloured by component, for varying income:

Total tax, for varying income:

Fraction of income taken as tax, for varying income:

WinTec GRays 2 GPS device feeding to NTP

USB driver

When I got a wintec g-rays2, it didn't work on USB out of the box with whatever laptop I had (probably a macbook), but was OK on Bluetooth, so that's what I stuck with.

Now, eight years later, I plugged it into one of my Raspberry Pis and it appears as /dev/ttyUSB1 by magic!

Getting NMEA sentences in minicom

minicom --device=/dev/ttyUSB1 --baud=4800 gives some garbled stuff every second, so I'm receiving the NMEA sentences but at the wrong serial port settings.

The manual didn't give any help but a bit of fiddling reveals sensible looking output at 57600 baud, 8N1 (here you can see where I live).

$GPRMC,121815.000,A,5130.3697,N,00003.7216,W,0.00,148.43,240717,,,A*72     
$GPGGA,121815.000,5130.3697,N,00003.7216,W,1,05,2.9,46.2,M,47.0,M,,0000*70 
$GPGSA,A,3,21,26,31,27,16,,,,,,,,4.3,2.9,3.2*38                            
$GPGSV,3,1,12,05,03,021,28,10,08,157,19,21,67,086,34,26,69,175,39*7C       
$GPGSV,3,2,12,29,12,083,,07,08,333,,31,06,193,26,20,27,059,24*72           
$GPGSV,3,3,12,49,,,35,27,43,274,31,16,72,283,39,18,26,132,23*4D 

These lines are spewed out once a second without needing to send any start command to the GPS unit.

Getting ntpd to pay attention

$GPRMC and $GPGGA are the relevant sentences for ntpd, according to the manual.

I already have ntpd runnning on this Pi, with an MSF receiver configured already.

This gives a /dev/gps0 (at least until reboot):

cd /dev
sudo ln -s ttyUSB1 gps0

and this line in /etc/ntpd.conf makes ntpd look for NMEA time sentences on /dev/gps0:

server 127.127.20.0 mode 67

The mode, decimal 67, means hexadecimal 0x43: 0x01 listen for GPRMC, 0x02 listen for GPGGA, 0x40 use 57600 baud.

And after a restart, tada! (although apparently a 160ms delay compared to all my other time sources. ick)

pi@faeroe /dev $ ntpq --peers
     remote           refid      st t when poll reach   delay   offset  jitter
==============================================================================
 2001:8b0:1638:9 81.2.122.172     2 u   39   64   17    0.952  157.794   0.783
 ntp2.aa.net.uk  195.66.241.2     2 u   41   64   17   14.923  162.505   0.671
 SHM(2)          .MSF.            0 l    -   64    0    0.000    0.000   0.000
*GPS_NMEA(0)     .GPS.            0 l   55   64    7    0.000   -5.660   0.819
 tyne.cqx.ltd.uk 81.2.122.172     2 u   46   64   17    0.674  157.858   0.759

/etc/hosts - the gift that keeps on giving

/etc/hosts

The gift that keeps on giving, when you're paid on an hourly rate to do tech support. It is like the regexps of DNS: "I know, I'll modify /etc/hosts" ... now you have two problems.

• You modify /etc/hosts because you want to override the global DNS view of name N.
• Things works!
• Because things work, you don't undo your change in /etc/hosts. After all, things work.
• A year passes.
• You forget that you made the change.
• Suddenly on your machine only, but no one else's, you can't access the website at N any more.
• Hours of debugging!

Why modify /etc/hosts? Testing a new version of a site under real name (only on your own machines though), or because DNS is broken and you don't know why, or because you didn't plan your DNS change so now the caches are not updating fast enough and you are impatient.

/etc/hosts doesn't have an "eventual consistency" mehanism in place - DNS caches eventually expire and at least give vaguely consistent behaviour across the whole internet over a long enough period of time. /etc/hosts will never converge.