tag:blogger.com,1999:blog-49832650761110251452024-03-13T16:43:16.312+00:00Ben Clifford Technical BlogUnknownnoreply@blogger.comBlogger214125tag:blogger.com,1999:blog-4983265076111025145.post-83160318496957028492021-11-07T19:03:00.002+00:002021-11-07T19:03:24.468+00:00Breaking recursion in Python and fix-ing it back up again<p>Trying out github repos for what started off as a blog post, on how fixpoint combinators relate to Python:</p>
<p><a href="https://github.com/benclifford/python-fixpoint#readme">https://github.com/benclifford/python-fixpoint#readme</a></p>Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-52442920910641077792021-01-28T18:33:00.001+00:002021-01-28T18:33:29.198+00:00berlin strava openstreetmap mashup<p>I made a mashup (so last decade) of my strava rides since I've been in Berlin.</p>
<p>You can see it <a href="http://www.hawaga.org.uk/ben/berlinmap/">here: http://www.hawaga.org.uk/ben/berlinmap/</a>.</p>
<p>It uses <a href="http://leafletjs.com/">leaflet.js</a> to draw the map, <a href="https://www.openstreetmap.org/">Open Street Map</a> to provide the base street map, <a href="http://www.strava.com/">Strava</a> on my phone to record my rides, and <a href="https://github.com/jpravetz/strava">jpravetz' strava CLI</a> to get the data out of Strava and into a file.</p>
<img width="480" src="http://www.hawaga.org.uk/ben/berlinmap/example.png">
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-34978694707670598942021-01-04T11:11:00.000+00:002021-01-04T11:11:11.322+00:00commandline editing for zoom meetups<p>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.</p>
<p>Zoom can give you a giant MP4 of the whole session, and I wanted to cut that video into pices.</p>
<p>A few times, I tried using <a href="https://www.openshot.org/">OpenShot</a> 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.</p>
<p>I figured out a workflow that worked better for me:
<ul><li>Use <a href="https://www.videolan.org/vlc/">VLC</a> on the giant MP4 to quickly identify the start and end times for each talk.</li>
<li>Make an ffmpeg command line for each talk, for example:
<pre>
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
</pre>
which will copy ranges out of `day1.mp4` in to the named file.
</li>
<li>
Then, let this run. It's quite slow on my laptop but doesn't need any human interaction.
</li>
</p>Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-74613029761789483562020-03-11T21:11:00.001+00:002020-03-11T21:11:31.264+00:00A1120EUA Hall Effect Switch vs Pi Zero W<div dir="ltr" style="text-align: left;" trbidi="on">
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.
<br />
Got A1120EUA-T from hobbytronics
<br />
turns out you can't set pullups from sysfs (/sys/class/gpio) ... so i'll have to install wiringpi for the <code>gpio</code> command.
<br />
<pre>
$ gpio export 0 in
$ gpio mode 0 up
</pre>
<br />
and now I can wave my neodymium magnets nearby (about 1.5cm) and see the input go low as it passes by.
<pre>
$ while true; do gpio read 0 ; done
1
1
1
0
</pre>
</div>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-21330080601457236752018-10-07T15:23:00.000+01:002018-10-07T15:23:09.601+01:00`stg uncommit` the first commit<div dir="ltr" style="text-align: left;" trbidi="on">
<p>
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).</p>
<p>`stg` doesn't like this: <br/>
<pre>
$ stg uncommit -n 1
Uncommitting 1 patches ... done
stg uncommit: Trying to uncommit 38a035a7667c9417e10a4f53e7c88a57711ca440,
which does not have exactly one parent
</pre>
... the root commit is not formed in the way that `stg` wants.</p>
<p>
I worked around this by:
<ol>
<li>making a new empty commit in a new repo:<br/>
<pre>
mkdir ~/empty-repo
$ cd ~/empty-repo
$ git init
$ git commit -a --allow-empty -m "Empty initial commit"
[master (root-commit) 38a035a] Empty initial commit
</pre>
</li>
<li>getting that empty commit into my real repo ...
<pre>
$ cd ~/real-repo
$ git remote add empty-repo ~/empty-repo
$ git fetch empty-repo
</pre>
</li>
<li>
cherry picking the original root commit on top of the empty commit ...
<pre>
$ git tag tmp1
$ stg pop -a
$ git reset --hard empty-repo/master
$ git cherry-pick tmp1
</pre>
</li>
<li>and now this cherry-picked originally original commit can be `stg uncommit`ted:
<pre>
$ stg uncommit -n 1
</pre>
</li>
</ol>
</p>
</div>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-81441038638010442552018-05-20T12:20:00.000+01:002018-05-20T12:22:31.800+01:00temporary merge tool<p>I've been an enthusiastic user of <code>stgit</code> 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.
</p>
<p>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.
</p>
<p>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.
</p>
<p>
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, <code>tmt</code>, 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.
</p>
<p>Here's the repo, with a README. Yes, it's Haskell. Of course. <a href="https://github.com/benclifford/tmt">https://github.com/benclifford/tmt</a>
</p>Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-53292445951942544232018-03-05T01:32:00.000+00:002018-03-05T01:32:03.703+00:00sous vide<p>I built a sous vide cooker, driven by a PWM/PID controller written in Erlang.</p>
<p>Then I gave a talk about it (and some other related temperature control that I've done) at a Raspberry Pi meetup.</p>
<p><a href="https://skillsmatter.com/skillscasts/11586-basic-heating-and-snooty-cooking-with-a-pi">Here's the video (login required)</a> and <a href="http://www.hawaga.org.uk/ben/tech/raspberry-pint-temperature/">here are the slides</a>.</p>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-39227318508218475182018-02-16T18:12:00.001+00:002018-02-16T18:12:39.572+00:00Build a Crap Web Form in Haskell in 28 days.<p>I've been writing an informal series of posts about a small scout camp registration system that I've been building:</p>
<p><a href="https://cwfh28.blogspot.co.uk/">Build a Crap Web Form in Haskell in 28 days</a></p>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-2046412098092109382018-01-29T06:00:00.000+00:002018-01-29T10:45:18.476+00:00Yellow Pages for Modern Times<p>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 <a href="https://en.wikipedia.org/wiki/IRIX">IRIX</a> and <a href="https://en.wikipedia.org/wiki/IBM_AIX">AIX</a> in there too.</p>
<p>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.</p>
<p>The technology of the time often used <a href="https://en.wikipedia.org/wiki/Network_File_System">Network File System (NFS)</a> and <a href="https://en.wikipedia.org/wiki/Network_Information_Service">Network Information Service (NIS)</a> (formerly known as Yellow Pages, with that name living on in the <code>yp</code> prefix of commands like <code>yppasswd</code>).</p>
<p>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.</p>
<p>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.
</p>
<p>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 <code>curl | sudo</code> script without messing up the rest of your system? Or stick with an old distribution of your OS just for one tool? Easy.</p>
<p>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.</p>
<p>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.</p>
<p>It was all so simple before: you had <code>~</code> everywhere, and nothing else.</p>
<p>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.</p>
<p>The actual technology (NFS, docker volume mounts, YP, LDAP, HESIOD, ...) isn't massively relevant: I've used different mechanisms in different places.</p>
<p>What really matters is: all the (regular human) users get their home directory, mounted at the same place (under <code>/home</code>).</p>
<p>Pretty much with most ways of sharing files, that means the unix user id for that user should be the same everywhere too.</p>
<p>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 <code>cue</code> 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 <code>/home</code> is volume-mounted, and then OpenLDAP is used to share accounts.</p>
<p>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.</p>
<p>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.</p>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-64679400767769932012018-01-21T21:03:00.001+00:002018-01-21T21:03:10.863+00:00A string of DNS protocol bugs.<p>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.</p>
<p>I've encountered three different apparent protocol implementation bugs in the space of a few hours:</p>
<ul>
<li><a href="https://www.aaisp.net.uk/">Andrews and Arnold</a>'s web based control panel accepts <code>DS</code> records as generated by BIND's <code>dnssec-keygen</code> 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 <a href="https://tools.ietf.org/html/rfc4034#page-18">RFC 4034 s5.3</a> seems to think is acceptable. Why is installing crypto keys always so hard?</li>
<li>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 <a href="https://developers.google.com/speed/public-dns/">Google Public DNS</a> at <code>8.8.8.8</code>, and <a href="https://dnssec-debugger.verisignlabs.com/www.cqx.ltd.uk">Verisign's DNSSEC checker</a> both worked ok.</li>
<li>I discovered an implementation quirk in the Haskell <a href="https://hackage.haskell.org/package/dns">dns</a> 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 <code>dns</code> 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. (<a href="https://github.com/kazu-yamamoto/dns/issues/103">github issue #103</a>)</li>
</ul>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-2749584245508097472018-01-18T11:57:00.000+00:002018-01-18T11:57:38.228+00:00findmnt<p>One of my customers uses <a href="https://cpanel.com/">cPanel</a> to administer their internet facing servers.</p>
<p>It has an interesting virtual filesystem setup for sandboxing user accounts: cPanel creates, per user, a new root filesystem for that user, and then <code>chroot</code> into that before running user code (shells, php, ...).</p>
<p>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.</p>
<p>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)</p>
<p>In the intervening years, isolation techniques like this have been becoming more mainstream - for example, my main use of docker (via my tool <a href="https://github.com/benclifford/cue">cue</a>) has been to prepare and use different root file systems.
</p>
<p>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 <code>mount</code> or <code>df</code> or <code>/proc/mounts</code> 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.</p>
<p>For example, I can see that <code>/home/virtfs/x/usr/sbin</code> goes to somewhere in the filesystem on <code>s_os-lv_root</code> but not where. (I can guess it's <code>/usr/sbin</code> in this case).
</p>
<pre>
/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
</pre>
<p>
Anyway, surely this can't be the way things are??
</p>
<p>
So along comes <code>findmnt</code>, which gives me this info:
</p>
<pre>
...
│ │ ├─/home/virtfs/x/usr/sbin /dev/mapper/vg_os-lv_root<b>[/usr/sbin]</b>
xfs ro,relatime,seclabel,attr2,inode64,sunit=512,swidth=512,usrquota
...
</pre>
<p>... which tells me that yes that really is mounted from <code>/usr/sbin</code>.</p>
<p>Anyway, a nice new command to discover, around since only util-linux v2.18 in mid 2010.</p>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-19903560018968151292017-09-29T12:38:00.000+01:002017-10-03T12:44:41.023+01:00Infrared Raspberry Pi<p>When I ordered my <a href="https://shop.pimoroni.com/products/raspberry-pi-zero-w">Pi Zero W</a> with a <a href="https://shop.pimoroni.com/products/raspberry-pi-zero-camera-module">no-IR-filter camera</a>, 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.</p>
<p>So, then I ordered 50 x £0.04 <a href="https://uk.rs-online.com/web/p/ir-leds/6997635P/">infrared LEDs from RS</a> (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.</p>
<p>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.</p>
<a href="http://www.hawaga.org.uk/ben/tech/pi-IR/scene1-light-and-45leds.jpeg"><img width="200" src="http://www.hawaga.org.uk/ben/tech/pi-IR/scene1-light-and-45leds.jpeg" /></a>
<a href="http://www.hawaga.org.uk/ben/tech/pi-IR/scene1-45leds-handhigh.jpeg"><img width="200" src="http://www.hawaga.org.uk/ben/tech/pi-IR/scene1-45leds-handhigh.jpeg" /></a>
<a href="http://www.hawaga.org.uk/ben/tech/pi-IR/scene1-45leds-backlight.jpeg"><img width="200" src="http://www.hawaga.org.uk/ben/tech/pi-IR/scene1-45leds-backlight.jpeg" /></a>
<p>And then I set it up overnight, with a timelapse video of myself sleeping:</p>
<iframe width="560" height="315" src="https://www.youtube.com/embed/TUgunqxl8bc?rel=0" frameborder="0" allowfullscreen></iframe>Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-83570629611595697702017-09-10T23:29:00.001+01:002017-09-12T15:02:48.949+01:00Unix exit codes as an indicator of tooling (im)maturity.<p>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.</p>
<p>I've hit this a couple of times at least in the last year. grr.</p>Unknownnoreply@blogger.com1tag:blogger.com,1999:blog-4983265076111025145.post-10743596405275229622017-09-01T17:36:00.002+01:002017-09-01T18:03:59.523+01:00Pattern matching in Idris `do` notation has surprising reliance on type checking the action.<p>Idris is syntactically quite Haskell-like, and especially it has <code>do</code> notation for sequencing "actions".</p>
<p>Like (traditional) Haskell, <code>do</code> blocks are desugared to a sequence of <code>>>=</code> (bind) operators. But,
unlike (traditional) Haskell, that <code>>>=</code> is not always the monadic <code>>>= : m a -> (a -> m b) -> m b</code>. (This can also happen in Haskell using <a href="https://ocharles.org.uk/blog/guest-posts/2014-12-06-rebindable-syntax.html">rebindable syntax</a>)</p>
<p>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.
<h3>Total parsing</h3>
In the case of Text.Parser (in the Idris <code>contrib/</code> package) the type signature of actions (<code>Grammar _ _ _</code> indicates whether a parser consumes any characters so that the compiler can tell if a parser might loop forever. (see <a href="http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.html">http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.html</a>)</p>
<p>I was trying to write a new JSON parser for <a href="https://github.com/benclifford/idris-todaybot">idris-todaybot</a> using Text.Parser. Previously JSON was parsed using lightyear, but Text.Parser has more gratuitous dependent types so was an obvious way to proceed.</p>
<h3>A problem.</h3>
<p>I ran into a surprising compile error which initially made no sense to me at all.</p>
<p>This code compiles:</p>
<pre><code>objectValuePair : Grammar Char True (List Char, ())
-- definition elided
jsonObject : Grammar Char True (List Char, ())
jsonObject = do
llll <- objectValuePair
pure llll
</code></pre>
<p>where <code>llll</code> is a tuple; but the following version of jsonObject, which desconstructs that tuple and reassembles it, does not compile:</p>
<pre><code>jsonObject : Grammar Char True (List Char, ())
jsonObject = do
(k,v) <- objectValuePair
pure (k,v)
</code></pre>
<p>It gives this error:</p>
<pre>
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
</pre>
<p>Another attempt to deconstruct <code>llll</code> also fails:
</p>
<pre><code> jsonObject : Grammar Char True (List Char, ())
jsonObject = do
llll <- objectValuePair
let (k,v) = llll
pure (k,v)
</code></pre>
<p>
but the following deconstruction by function application rather than pattern matching succeeds:
</p>
<pre><code>jsonObject : Grammar Char True (List Char, ())
jsonObject = do
llll <- objectValuePair
let k = fst llll
let v = snd llll
pure (k,v)
</code></pre>
<h3>That type error</h3>
<p>Let's dig into that type error:</p>
<pre>
Type mismatch between
Grammar Char False (List Char, ()) (Type of pure (k, v))
and
Grammar Char c2 (List Char, ()) (Expected type)
</pre>
<p><code>Grammer _ _ _</code> is the type of parser actions, where the first parameter <code>Char</code> is the type of symbols we're consuming, the final parameter <code>(List Char, ())</code> is the type that the parser will return on success, and the middle parameter (<code>False</code> or <code>c2</code>) represents whether the parser will definitely consume input (<code>True</code>) or might succeed without consuming anything (<code>False</code> - for example, a parser which removes whitespace, or <code>pure</code> which never even looks at the input stream).</p>
<p>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: <a href="https://github.com/idris-lang/Idris-dev/blob/v1.1.1/libs/contrib/Text/Parser.idr">the source</a>)</p>
<p>So what on earth has this parameter, manipulated by <code>>>=</code>, got to do with pattern matching pure
values after they've already been returned by an action?</p>
<h3>Desugaring</h3>
<p>It turns out we can forget that our troublesome tuple is being returned from an action; <code>let (a,b) = (1,2)</code> breaks in the same way when run inside a <code>Text.Parser</code> <code>do</code> block.</p>
<p>Let's (very roughly) desugar some of the examples above, and then look at the types involved:</p>
<pre><code>jsonObject : Grammar Char True (List Char, ())
jsonObject = do
llll <- objectValuePair
pure llll
-- becomes:
jsonObject = objectValuePair >>= (\v => pure v)
</code></pre>
<pre><code>
jsonObject = do
(k,v) <- objectValuePair
-- becomes:
objectValuePair >>= (\(k,v) => pure (k,v))
-- becomes:
objectValuePair >>= (\llll => case llll of
(k,v) => pure (k,v)
)
</code></pre>
<p>So in the second fragment, there's an extra <code>case</code> expression in there
to deconstruct <code>llll</code> using pattern matching.
</p>
<p>Apparently that gets in the way of type inference/checking:
<ul>
<li>On the one hand, that <code>pure</code> has type: <code>Grammar Char False (List Char, ())</code> - false because it may (actually, will always) succeed without consuming input.</li>
<li>On the other hand, <code>>>=</code> doesn't care whether the right hand side consumes or not - it will take either, as shown by the compile time variable <code>c2</code> appearing in the error message.</li>
</ul>
Idris doesn't manage to unify <code>c2 = False</code>.
</p>
<p>
With further pinning of types using <code>the</code>, an uglier form of pattern matching does work:
</p>
<pre><code>
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)
</code></pre>
<h3>Ugh</h3>
<h3>Thanks</h3>
<p>Thanks to Melvar on #idris for explaining this.</p>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-59644788491655367432017-09-01T14:22:00.001+01:002017-09-01T14:43:55.217+01:00highlight.js in blogger<p>Syntax highlighting is pretty. highlight.js can do it in a browser. I just added it to this blog.</p>
<ol>
<li>In Blogger, click "Theme" then "Edit HTML"</li>
<li>Find the <head> section of the theme.</li>
<li>Insert the following at the end, before the closing <head> tag:
<pre><code data-trim><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'/>
</code></pre>
</li>
<li>Add as many copies of the third line as you want, modifying <code>haskell</code> to the additional languages that you want to be able to highglight.</li>
<li>When writing code, wrap it in <code><pre><code class="haskell"> YOUR CODE </code><pre></code></li>
</ol>Unknownnoreply@blogger.com1tag:blogger.com,1999:blog-4983265076111025145.post-36078388604144862992017-08-31T16:17:00.001+01:002017-08-31T17:14:04.037+01:00Raspberry Pi Zero W + cam timelapse <p>I got a <a href="https://www.raspberrypi.org/products/raspberry-pi-zero-w/">Raspberry Pi Zero W</a> and a <a href="https://shop.pimoroni.com/products/raspberry-pi-zero-camera-module">camera module</a>.</p>
<p>I wanted a timelapse video.</p>
<p>This is how I did it:</p>
<h2>Capture a sequence of image frames</h2>
<p>This will capture a sequence of images (forever) approximately
every minute, with the filename being a unix timestamp.
<pre>
while true; do raspi-still -o $(date +%s).jpeg ; sleep 60s; done
</pre>
<p>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:</p>
<pre>
$ ls
1504014800.jpeg
1504014866.jpeg
1504014931.jpeg
...
</pre>
<h2>Combine the sequence of image frames into a jpeg</h2>
<p>After you've got all the frames you want, use <code>ffmpeg</code> 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.</p>
<p>First make a command file listing all the jpeg files:</p>
<pre>
ls *jpeg | while read a ; do echo file $a; done > e.cmd
</pre>
<p>Next, feed that command file into ffmpeg to generate
a video:</p>
<pre>
ffmpeg -f concat -i e.cmd -b:v 1500000 -r 24 -c:v libx264 e8.mp4
</pre>
<p>As a result, the output video should be in <code>e8.mpg</code> which is
in a form suitable for playing with vlc or uploading to YouTube.</p>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-13923707300984439452017-08-20T21:35:00.000+01:002017-08-20T22:03:36.723+01:00An income tax explorer, using R and Shiny<p>I got carried away with my R code for plotting income tax rates, and now it is an interactive webapp <a href="https://benc.shinyapps.io/r-income-tax/">https://benc.shinyapps.io/r-income-tax/</a> using <a href="https://shiny.rstudio.com/">Shiny</a>,
a web framework for turning your R code into a website. Thanks Tom Nielsen for convincing me <a href="https://www.meetup.com/London-Haskell/events/241810586/">(in this talk about making a Haskell port of Shiny)</a> to try it out.
</p>Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-6065053239774758812017-08-18T15:18:00.000+01:002017-08-18T15:41:43.819+01:00A first project in R / UK income tax graphs<p>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.</p>
<p>The code at <a href="https://github.com/benclifford/r-income-tax">https://github.com/benclifford/r-income-tax</a> can generate the following three graphs:</p>
<p>Marginal income tax rates, coloured by component, for varying income:<br/>
<img src="http://www.hawaga.org.uk/ben/tech/r-income-tax/marginal.png">
</p>
<p>Total tax, for varying income:<br/>
<img src="http://www.hawaga.org.uk/ben/tech/r-income-tax/total.png">
</p>
<p>Fraction of income taken as tax, for varying income:<br/>
<img src="http://www.hawaga.org.uk/ben/tech/r-income-tax/total-fraction.png">
</p>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-24170062571853243472017-07-24T13:42:00.001+01:002017-07-24T13:51:51.051+01:00WinTec GRays 2 GPS device feeding to NTP<h2>USB driver</h2>
<p>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.</p>
<p>Now, eight years later, I plugged it into one of my Raspberry Pis and it appears as /dev/ttyUSB1 by magic!</p>
<h2>Getting NMEA sentences in minicom</h2>
<p><code>minicom --device=/dev/ttyUSB1 --baud=4800</code> gives some garbled stuff every second, so I'm receiving the
NMEA sentences but at the wrong serial port settings.</p>
<p><a href="http://www.wintec-gps.de/download/wintec_wbt-201_manual.pdf">The manual didn't give any help</a> but a bit of fiddling reveals sensible looking output at 57600 baud, 8N1 (here you can see where I live).</p>
<pre>
$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
</pre>
<p>These lines are spewed out once a second without needing to send any start command to the GPS unit.</p>
<h2>Getting ntpd to pay attention</h2>
<p><code>$GPRMC</code> and <code>$GPGGA</code> are the relevant sentences for ntpd, <a href="https://www.eecis.udel.edu/~mills/ntp/html/drivers/driver20.html">according to the manual</a>.</p>
<p>I already have ntpd runnning on this Pi, with an MSF receiver configured already.</p>
<p>This gives a /dev/gps0 (at least until reboot):</p>
<pre>
cd /dev
sudo ln -s ttyUSB1 gps0
</pre>
<p>and this line in <code>/etc/ntpd.conf</code> makes ntpd look for NMEA time sentences on /dev/gps0:</p>
<pre>
server 127.127.20.0 mode 67
</pre>
<p>The mode, decimal 67, means hexadecimal 0x43: 0x01 listen for GPRMC, 0x02 listen for GPGGA, 0x40 use 57600 baud.
</p>
<p>And after a restart, tada! (although apparently a 160ms delay compared to all my other time sources. ick)
<pre>
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
<b>*GPS_NMEA(0) .GPS. 0 l 55 64 7 0.000 -5.660 0.819</b>
tyne.cqx.ltd.uk 81.2.122.172 2 u 46 64 17 0.674 157.858 0.759
</pre>
</p>
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-60592508616774907112017-07-03T10:48:00.000+01:002017-07-03T10:48:03.466+01:00/etc/hosts - the gift that keeps on giving<p><code>/etc/hosts</code></p>
<p>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" ... <a href="http://regex.info/blog/2006-09-15/247">now you have two problems</a>.</p>
<p>
<ul>
<li>You modify <code>/etc/hosts</code> because you want to override the global DNS view of name N.</li>
<li>Things works!</li>
<li>Because things work, you don't undo your change in <code>/etc/hosts</code>. After all, things work.</li>
<li>A year passes.</li>
<li>You forget that you made the change.</li>
<li>Suddenly on your machine only, but no one else's, you can't access the website at N any more.</li>
<li>Hours of debugging!</li>
</ul>
</p>
<p>Why modify <code>/etc/hosts</code>? 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.</p>
<p><code>/etc/hosts</code> 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. <code>/etc/hosts</code> will never converge.</p>
Unknownnoreply@blogger.com2tag:blogger.com,1999:blog-4983265076111025145.post-50024270501055187632017-06-26T20:18:00.000+01:002017-06-27T12:34:02.559+01:00ffmpeg animated gif custom palettes<p>I used ffmpeg to make the animated gifs for my <a href="http://www.hawaga.org.uk/ben/tech/goggles/">gallery of NeoPixel goggles patterns</a>.</p> In the process I discovered that as well as the expected fairly straightforward conversion mode, <code>ffmpeg -i mymovie.mov mymovie.gif</code>, there is another mode which can generate a custom palette. Because apparently by default, a default palette is used.</p>
<p>That is a slightly more awkward two step process, <a href="http://blog.pkh.me/p/21-high-quality-gif-with-ffmpeg.html">described for example here</a>, but at least for my goggles GIFs looks way better (to me) although turning out to be four times the size:</p>
<p>
<img src="http://www.hawaga.org.uk/ben/tech/goggles/rainbow.gif">
<img src="http://www.hawaga.org.uk/ben/tech/goggles/rainbow-lowquality.gif">
</p>Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-58979109803633767972017-06-17T11:35:00.000+01:002017-06-27T12:34:40.064+01:00Galois LFSR PRNG in NeoPixel goggles<p>I've been playing with software to run on my Adafruit Neopixel Goggles. The software gets to make pretty patterns on
32 x 24-bit RGB LEDs arranged in two rings.</p>
<p><img src="http://www.hawaga.org.uk/ben/tech/goggles/prng.gif"></img></p>
<p>One of the modes picks random colours to change each ring to. The Arduino stack supplies a <code>random()</code> function to do this, but it seemed to take up about 600 bytes of the limited 5kb flash program memory on the <a href="https://www.adafruit.com/product/1501">in-goggles microcontroller</a>.</p>
<p>I wondered if I could make a smaller-but-less-random generator. After all, the colour pattern does not need to be cryptographically secure. I'm just trying to avoid getting the same sequence of colours every time.</p>
<p>Someone pointed me at Linear Feedback Shift Register PRNGs and I implemented one based around a description in Wikipedia. I chose the Galois one because <a href="https://en.wikipedia.org/wiki/%C3%89variste_Galois#Final_days">pistols at dawn</a>.</p>
<p>That seemed to work well for the basic generation of random numbers, but the Arduino always started up with the same seed, and so gave the same sequence of colours each time. Luckily, there are 512 bytes of EEPROM on this microcontroller and so I used two other those to generate and store a seed to be used next time.</p>
<p>Initially, I generated two random bytes at power-on, and stored those into the EEPROM. However, this rapidly proved to have a really short period: there were only two different patterns being displayed by the goggles in this mode!</p>
<p>So, next, which seems to work better, the code now initialises the PRNG from EEPROM, takes a single bit from it (and discards it) and then writes out the PRNG state into the EEPROM. That means that the start state advances by one bit every boot.</p>
<p>Code for the goggles is here on github: <a href="https://github.com/benclifford/goggles">https://github.com/benclifford/goggles</a>.
Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-74710730146301907432017-06-14T14:17:00.000+01:002017-09-01T14:06:30.164+01:00An Idris implementation of a reddit bot.<p>I wrote and host <a href="https://github.com/benclifford/lsc-todaybot">lsc-todaybot</a>, a bot that moves the [TODAY] flair around on reddit.com/r/LondonSocialClub, a subreddit dedicated to social activities in London. I wrote it in Haskell, and over the last year or so have used it as a simple application for experimenting with different Haskell libraries and techniques. For example, I used it to learn about extensible effects (and gave <a href="www.hawaga.org.uk/ben/tech/london-hug-exteff/">a talk about it at the London Haskell meetup</a>).</p>
<p>I've been interested in the dependently typed programming language <a href="https://www.idris-lang.org/">Idris</a> and someone claimed it was pacman-complete - that is, you can write Pacman in it. So rather than playing round with proofs and all that dependent-type gubbins, I set out to rewrite todaybot in Idris.
</p>
<p>It's here: <a href="https://github.com/benclifford/idris-todaybot">https://github.com/benclifford/idris-todaybot</a></p>
<p>It's not beautiful. But it works well enough to be running alongside the Haskell implementation.</p>
<p>I've littered the source with <code>QUESTION/DISCUSSION</code> blocks, but basically I had to patch up an existing JSON library, interface an HTTP library (I chose <a href="https://curl.haxx.se/libcurl/">libcurl</a>), and struggle with a whole new style of error message (possibly the hardest bit as I'm used to error messages really leading you to the right answer).</p>
<p>
There's almost no use of dependent types, but I did find a straightforward place to make use of them, in the parameters to this libcurl function:
<pre>
CURLcode <a href="https://curl.haxx.se/libcurl/c/curl_easy_setopt.html">curl_easy_setopt</a>(CURL *handle, CURLoption option, parameter);
</pre>
</p>
<p>where the type of the supplied <code>parameter</code> <em>depends on</em> the particular <code>option</code> chosen: for example a pointer to a callback function, or a boolean verbosity level.</p>Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-28153016727249690052017-06-07T14:15:00.000+01:002017-06-07T14:16:15.577+01:00Fixing up my MSF radio clock<p>One of the first hardware things I did with a Raspberry Pi (<a href="https://github.com/benclifford/msf/commit/795e6304723cb60df87fef92942c5173396bdfa1">sometime around March 2013</a>) was interface it to a cheap 60kHz radio clock board, and write some driver software to interface it to ntpd. That was in one house, then in another, and then got dismantled, put in a box, and smashed up a bit. Based on the </p>
<p>I spent a few hours yesterday fixing it up: resoldering the antenna onto the circuit board, getting rid of the dodgy soldering and putting it on a prototype board, putting a capacitor across the power supply because I heard rumour that might make it receive better (it doesn't seem to), and implementing parity checking in the decoder.
</p>
<p>
It's still terribly awkward to position: I have it velcroed up on top of a curtain rail to try to get it high and away from all my other electronics and it is still very sensitive to antenna positioning; and it is still estimated by ntpd to be less accurate than getting time off the internet; and even with parity checking it is still fairly common for it to decode a time that is wrong.
</p>
<p>
But it has a nice flashing red LED.
</p>
<p>Software: https://github.com/benclifford/msf
</p>Unknownnoreply@blogger.com0tag:blogger.com,1999:blog-4983265076111025145.post-52495933220043874672017-03-05T16:14:00.003+00:002017-03-05T16:45:08.476+00:00toad.com open mail server<p>So there was some controversy decades ago the past about <a href="https://en.wikipedia.org/wiki/John_Gilmore_%28activist%29#Activism">John Gilmore</a>'s public open SMTP relay server. I wondered if it still existed.</p>
<p>It does!</p>
<p>
<pre>
benc@dogger:~$ telnet new.toad.com 25
Trying 209.237.225.253...
Connected to new.toad.com.
Escape character is '^]'.
220 new.toad.com ESMTP Sendmail 8.12.9/8.12.9; Sun, 5 Mar 2017 08:12:44 -0800
EHLO dogger.cqx.ltd.uk
250-new.toad.com Hello dynamic-91.hawaga.org.uk [90.155.94.91] (may be forged), pleased to meet you
250-ENHANCEDSTATUSCODES
250-PIPELINING
250-8BITMIME
250-SIZE 89000000
250-DSN
250-ETRN
250-AUTH GSSAPI
250-STARTTLS
250-DELIVERBY
250 HELP
MAIL FROM:benc@hawaga.org.uk
250 2.1.0 benc@hawaga.org.uk... Sender ok
RCPT TO:benc@hawaga.org.uk
250 2.1.5 benc@hawaga.org.uk... Recipient ok
DATA
354 Enter mail, end with "." on a line by itself
Subject: test 1
test
.
250 2.0.0 v25GCiXw019546 Message accepted for delivery
221 2.0.0 new.toad.com closing connection
</pre>
</p>
<p>
<pre>
Return-Path: <benc@hawaga.org.uk>
Received: from new.toad.com (new.toad.com [209.237.225.253])
by smtp-in.biscay.cqx.ltd.uk (8.14.4/8.14.4/Debian-2ubuntu2.1) with ESMTP id v25F9dpo009917
for <benc@hawaga.org.uk>; Sun, 5 Mar 2017 15:09:40 GMT
Received: from dogger.cqx.ltd.uk (dynamic-91.hawaga.org.uk [90.155.94.91] (may be forged))
by new.toad.com (8.12.9/8.12.9) with ESMTP id v25F96Xw016104
for benc@hawaga.org.uk; Sun, 5 Mar 2017 07:09:28 -0800
Date: Sun, 5 Mar 2017 07:09:06 -0800
From: benc@hawaga.org.uk
Message-Id: <201703051509.v25F96Xw016104@new.toad.com>
Subject: test 1
</pre>
</p>
Unknownnoreply@blogger.com1