Posted on

Allow Leslie Lamport to explain to you what TLA+ is

Sat down with a good friend who’s in math + economic history.

He’d taken me to school at the gym, introducing the Thai boxing exercise “kick the heavy bag” 45-seconds-per-leg. Brutal. Loud. I can perhaps recommend it. Afterwards at Nobes, enjoying a traditional meal of potatoes, gravy and vegan kålpudding, he asked me whether math is any use to career programmers.

I hemmed, I hawed. Most programmer activity is not about math. Statistics? Algorithms? Graph theory?

And then I tried to explain TLA+. I failed hard at that, so this short note is a link to better material than I was able to mumble up during eating.

TLA+ is:

a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems.

the TLA+ wikipedia article

The wikipedia article is good. Turns out, Lamport did us one better, he put together a full video course:

“This is the first lecture of the TLA+ video course”, a sun-kissed Lamport intones in the first few seconds. Excellent!

Then, he warns the viewer, that they should consume this course together with the multimedia he has created, at his website. TLA+ Course Lecture 1.

He’s right.

Having watched a few of these caring, teaching, and (mildly) funny videos, I’m becoming a fan. Well-made timed multimedia cues are great. Being told when to stop watching, and downloading a paper, or learning something else – it works well.

(The material is darn interesting.)

Resources made by Lamport on TLA+ abound, and I’m not doing you a service by trying recommend anything less than the real video thing. Any other code repository or tooling he’ll tell you about. He’ll tell you about it while dressed in clown clothes and corny outfits.

For the very interested, and text-oriented, there’s also the hyperbook. A series of interlinked PDF resources, which one can peruse to learn about TLA+. I read a bit of that first, and then switched over to the video presentation. Both are good.

Now, I hope this small note has alerted you to the existence of tons of TLA+ material online, and that you enjoy a whiff of that at some point.

Posted on

Ruby feature: Regular Expression replace once

About a year ago, programmer Tony Arcieri posed a question on the Ruby language bug tracker:  Why was Thread.exclusive deprecated?

Among the answers to this question, Shyouhei Urabe’s one of the tersest feature descriptions yet: “we already have such thing, to some extent at least”:

/#{@mutex=Mutex.new}/o
  1. The pair of slashes are Regular Expression delimiters.
  2. A Regular Expression in Ruby allows String interpolation, just like the double-quoted String does. The #{} contains interpolated Ruby code.
  3. The modifier o at the end of the Regular Expression stands for “once”. So, the regex engine would keep track of this replacement, and do it just once.

The Malmo.rb named this expression (//o) the face-palm operator.

Posted on

Malmö Coders’ Book Club

Quick report on Malmö coders’ book club: This was the initial sitting, and we were 7 people around the table. One academic, two leads, and four software engineers. We spoke English, since we were an international crowd.

At least three physical notebooks full of written notes were out, and the conversation was started based on questions people had during their reading. The conversations were personal, kind, and focused. It brings more perspective, to have people of different backgrounds, of different roles.

This was one of the peer groups I’d been looking for. 5 out of 5 thumbs.

PS: We had been reading Michael Feathers’ Working Effectively With Legacy Code. 

Posted on

Automate finding misspellings in source code

Typos and misspellings in code can be difficult.

Finding them and keeping them out takes vigilance. Lots of mental energy wasted.

The misspellings tool written in Python can be installed using pip install misspellings.

This tool looks for commonly misspelled words in source code. It has a built-in list of common spelling mistakes.

Example: List all Ruby files and pass each of them to the misspellings tool, with the -f option (file list) set to - for standard input.

$ find . -name '*.rb' | misspellings -f -
./lib/celluloid/exceptions.rb:12: occured -> "occurred"
./spec/celluloid/calls_spec.rb:12: wasnt -> "wasn't"
./spec/shared/actor_examples.rb:950: slighly -> "slightly"
./spec/support/configure_rspec.rb:44: occured -> "occurred"

(As a courtesy, I edited those misspellings in the Celluloid project. It wouldn’t do to let it be made an example of and then not fixing it.)

Posted on

How to use very latest Bundler in Travis

TL;DR: When Bundler has fixes in master that you need, use the specific_install Rubygems plugin to install and use Bundler directly from a git branch. Example Travis YAML configuration excerpt:

before_install:
  - gem update --system
  - gem install specific_install
  - gem specific_install https://github.com/bundler/bundler.git
Picture: taken at Cambridge U Library. This is a CC0 free stock photo. But those are nice columns surrounding and wrapping the body of the page. Also: note the shadows of the supporting lines still visible in the finished book.

I will spend the rest of this post unpacking what the above means.

In Ruby, there is a package manager called Bundler. It’s continuously developed, and like all software, can have bugs.

When a Bundler bug gets fixed, the code changes are “merged to master branch”. Then we all wait for the next release. The workarounds are about sticking to an older, non-broken version: use the -v option to choose an exact release. Example: gem install bundler -v'1.13.7'

The Rubygems system does not have a way to install gems “from a Git source URI”, but it does have a plugin system. And luckily, one of the plugins available (but not on that page) is specific_install.

allows you to install an “edge” gem straight from its github repository, or install one from an arbitrary url

In order to work around the “we all wait for the next release” step, we can install the latest and greatest using this plugin.

The plugin’s has also aliased its specific_install action to git_install. The manual claims:

This alias is shorter and is more intention-revealing
of the gem's behavior.

Source: The above Travis configuration snippet comes from a PR to the releaf project.

Posted on

IndieWeb clubbery

Tonight, I made it to Homebrew Website Club hosted at inUse in Malmö. I was greeted by three kind souls, among them a proprietor of a Lego fan website with a 176 contributors – and Pelle and Emil.

The club format is the same every time: first an hour of social or at-your-computer time. Then an hour of show-and-tell explanations, demoing and showing stuff.

Emil showed us CSS and SVG techniques, some of them brilliant. SVG is a deep well to drink from. Read more at Sara Soueidan’s website.

Pelle made a very nice hands-on demo of a system of services he’s built, which involved commenting on any page using his telephone.

We had talked about Node.js a fair bit, and I showed what the private caching npm server sinopia looks like when installed. Its claim to fame is its file-based caching – don’t fetch packages from the central repository more than you need.

When I had showed that, we had used up our time, and it was time to put the crisps down and go home. How kind, to have time limit, so that people on tight schedules won’t miss stuff.

On the way out, I asked: “Pelle, do you have a exercise for me to take home?” He responded immediately: “Make your site receive or send WebMentions.”

I look forward to next time.

Aiga forward and left arrow, an example of a random SVG
Posted on

Git Pre-commit hooks!

Not even once!

Run relevant code-checking tools on your code, before it is even checked in locally. Using the Ruby project Overcommit, you can set this up on your own machine in a jiffy. Or, read more about git hooks.

I took these steps:

  1. Install the overcommit gem in your active Ruby. gem i overcommit
  2. Install overcommit in your system Ruby, using this neat trick:PATH=/usr/bin:/bin:/usr/sbin:/sbin sudo gem install overcommit – This makes it available to tools like SourceTree! (On committing, it opens a bare shell, without your cool settings.)
  3. In your project directory, where you wish to begin using Overcommit to run Git hooks: overcommit --init
  4. Configure the resulting .overcommit.yml to enable/disable the checks you want run.
  5. Try committing a file which would fail a check.
  6. Profit!

PS: Here is an example .overcommit.yml:

PreCommit:
  ALL:
    problem_on_unmodified_line: warn
  CoffeeLint:
    enabled: true
  RuboCop:
    enabled: true
Posted on

Looking forward to PolyConf 2015

On Wednesday, I once again journey south, to Poznan in Central Europe, to participate in the PolyConf programming conference.

Poznan Glowny

As every year, it is about getting new perspective on things, from happy and grumpy people in the field. The field of computering.

I’m lucky to see some familiar faces in the list of people going there, and I’m travelling with qerub, a good friend. (Now, by visiting his website, I saw this wonderfully Acme-hacking project: an S-expression interface to his iTunes library. It’s a year old. I feel like a bad friend for not having seen it before. And, his casing utility camel-snake-kebab has a nicely communicative README.)

Last year, some major themes that stayed with me were property-based testing, functional everything and formal verification (software proofs).

People I met were curious about things, curious about history, curious about sub-fields near their own special field of interest.

To be able to catch the ideas and whims of this three-day madness festival, I will bring a Leuchtturm note-taking book. I’m pretty excited about using it. You may see photos of it on here. Update: inspiration from Bocoups blog, which is covering CSSConf using art.

You’ll hear more from me.

Posted on

Child themes and repairing them

Meta-blogging, again. It took quite a long time, and had some fits and starts, but now this blog runs on a so-called Child Theme of a freely available WordPress theme.

The trick is that I get to fiddle with small necessary things (like repairing the missing link to jQuery and some Twitter-needed meta tag) in files that are not updated and outdated when the theme gets an update.


.
|-- functions.php
|-- screenshot.png
`-- style.css

Something like that is enough. The automatically-included functions.php file makes it easy to do things the WordPress way, using their hooks-and-actions concept.

All this, and I really only wanted to install Known, the Indieweb blogging engine that supports webmentions.

Posted on

Install ruby-2.0.0-p195 using rbenv, ruby-build and pkg-config

Ruby, Rails, news of new versions. Your computer’s Homebrew and ruby-build installation does not work. Something’s borked. It worked on the other people’s Debian machines. Your Homebrew system gave you… output. Some obscure error about openssl?

You search. You whine. You arrive here. Breathe.

Requirements: rbenv, ruby-build, a Ruby 2.0.0-p195 refuses to install on account of missing header files for openssl, since the Apple-bundled version is outdated.

TL;DR:

Add this at the end of your shell startup file (such as ~/.bash_profile or ~/.zshrc). Then run the installation again.

export PKG_CONFIG_PATH=/usr/local/opt/openssl/lib/pkgconfig:/usr/local/lib/pkgconfig

Learn how!

In order to share more of the fact-finding process, here is some narrative. All credit is due to Stuge. He told me to read, it would work. Thanks! He was right, too. It did work.

First of all, pkg-config is a neat little program. It’s the hero of this narrative. Does all the heavy archiving, noting things down, so you don’t have to.


pkg-config --debug

This lists everything that pkg-config knows about header file locations, libraries, compilation configuration settings about the libs on your system.

Begin by ensuring there is a PKG_CONFIG_PATH on your system, that points to where the currently-symlinked Homebrew packages are. Add this to your shell startup:

export PKG_CONFIG_PATH=/usr/local/lib/pkgconfig

Well, this is half-way, pkgconfig can now find most of its .pc files.

The specific complaint was about openssl. Let’s go to its folder, using brew:


$ cd `brew --prefix openssl`

Now, are there any pkg-config files around? Use find:


$ find . -name '*.pc'
./lib/pkgconfig/libcrypto.pc
./lib/pkgconfig/libssl.pc
./lib/pkgconfig/openssl.pc

Ah-hah!


$ cd lib/pkgconfig
$ pwd
/usr/local/opt/openssl/lib/pkgconfig

This is the path where our pkg-config descriptions sit. Pre-pend it to its path!


export PKG_CONFIG_PATH=/usr/local/opt/openssl/lib/pkgconfig:/usr/local/lib/pkgconfig

Thusly, the desired result:


$ ruby-build 2.0.0-p195 ~/.rbenv/versions/2.0.0-p195
Downloading ruby-2.0.0-p195.tar.gz...
-> http://ftp.ruby-lang.org/pub/ruby/2.0/ruby-2.0.0-p195.tar.gz
Installing ruby-2.0.0-p195...
Installed ruby-2.0.0-p195 to /Users/olle/.rbenv/versions/2.0.0-p195

The end.

Addendum for web-crawling robots

(The obscure error mentioned at the start included here for searchability.)


rbenv install 2.0.0-p0
Downloading ruby-2.0.0-p0.tar.gz...
-> http://ftp.ruby-lang.org/pub/ruby/2.0/ruby-2.0.0-p0.tar.gz
Installing ruby-2.0.0-p0...

BUILD FAILED
Inspect or clean up the working tree at /tmp/ruby-build.20130506102349.2564
Results logged to /tmp/ruby-build.20130506102349.2564.log
Last 10 log lines:
installing default gems: /home/shivin/.rbenv/versions/2.0.0-p0/lib/ruby/gems/2.0.0 (build_info, cache, doc, gems, specifications)
bigdecimal 1.2.0
io-console 0.4.2
json 1.7.7
minitest 4.3.2
psych 2.0.0
rake 0.9.6
rdoc 4.0.0
test-unit 2.0.0.0
The Ruby openssl extension was not compiled. Missing the OpenSSL lib?