J-Bob from the Little Prover

The Little Prover book references a companion proof assistant tool called J-Bob. I had a hard time getting it running using Racket’s Dracula package, here’s how to do it:

  1. Install Racket.
  2. Install the Dracula package for Racket. On macOS, I did:
    cd /Applications/Racket\ v6.10.1/bin
    sudo ./raco pkg install dracula
  3. Download ACL2. I ended up grabbing a pre-built binary gzipped tarball which was for 7.1, but the latest is 7.4 if you want to build from source.
  4. Unzip the ACL2 tarball somewhere, I put it in my home directory, so it ended up as ~/acl2-image-7.1-macosx.x86_64
  5. Launch the DrRacket IDE
  6. Menu: Language -> Choose Language -> Other Languages -> Dracula -> ACL2
  7. Menu: Dracula -> Change ACL2 Executable Path… -> Point it at the run_acl2 binary in the directory where you installed ACL2.
  8. In the top-left window, paste the following:
    (include-book "j-bob-lang" :dir :teachpacks)
    (include-book "j-bob" :dir :teachpacks)
    (include-book "little-prover" :dir :teachpacks)

    Note: Running these commands  in the REPL in the bottom-left window didn’t work for me.

  9. Click the “Run” button at the top-right of the Dr. Racket window.

You’re now set up to use J-Bob. Verify it worked by typing the following in the interpreter in the bottom-left window of Dr. Racket.

(J-Bob/step (prelude) '(car (cons 'ham '(cheese))) '())

The output should be:

(car (cons 'ham '(cheese)))

 

Advertisements
Posted in Uncategorized | Tagged , , , | Leave a comment

Generating Dash cheat sheets

I’m a big fan of the Dash documentation tool for macOS. In particular, I often create my own Dash cheat sheets to help me remember commands I frequently forget.

I make enough of these that I created a simple Go app named cheat to generate a skeleton cheat sheet. I also created an UltiSnips snippet to make it easier to generate categories and entries in cheat sheets.

snippet entry "cheatsheet entry"
entry do
    name '$1'
    notes <<-'END'
    \`\`\`
    $2
    \`\`\`
    END
end
endsnippet

snippet category "cheatsheet category"
category do
    id '$1'
end
endsnippet

On Neovim, this would go in ~/.config/nvim/UltiSnips/ruby.snippets

Posted in dash | Leave a comment

Paste as plain text with Quicksilver

I used to use Plain Clip for converting clipboard contents to plain text before pasting, but now I do it in one step with Quicksilver.

I created the following custom trigger:

Item: Clipbord Contents
Action: Paste as Plain Text
Shortcut: alt-v

Now if I do alt-v instead of cmd-v for pasting, it pastes as plain text.

Posted in quicksilver | Leave a comment

Lock screen or sleep from Quicksilver

I recently got a new laptop, and I’ve been transferring over all of my settings. I often use Quicksilver to trigger a screen lock or put my laptop to sleep. Here’s how I do it.

I use a shell script to put my machine to sleep:

sleep.sh

#!/bin/bash
pmset sleepnow

In order to be able to trigger the shell script from Quicksilver, you’ll need the “Terminal Plugin” installed.

I use an AppleScript script to lock my screen:

lockscreen.scpt

tell application "System Events"
    set ss to screen saver "Flurry"
    start ss
end tell

 

I use the QuickSilver “Add to Catalog” action to add sleep.sh and lockscreen.scpt to the catalog. That action isn’t enabled by default, to enable it, you need to open QuickSilver preferences, click “General”, choose “Actions”, search for “Add to Catalog”, and enable it.

By default, the “Open” action has a higher precedence than the “Run” action for shell scripts. You can change the precedence order of actions by dragging, I dragged the “Run […]” action (Run a Shell Script [with optional arguments]) above the “Open” action.

 

Posted in Uncategorized | Leave a comment

Spinnaker & Kubernetes on macOS

Recently I was playing with the open-source release of Spinnaker, the continuous delivery tool that we use inside of Netflix. Spinnaker is designed for deploying apps on cloud backends (e.g., AWS, GCE), but I wanted to run everything entirely on my MacBook Pro.

Here’s how I set it up.

Prereqs

This uses Docker for running Spinnaker, and Kubernetes for the backend. The simplest way to get Docker and Kubernetes running on your local machine is:

  1. Install Docker for Mac
  2. Install corectl.app
  3. Install Kubernetes Solo cluster for macOS

Once all of these apps have been installed and running, you should have a Docker icon, Corectl icon, and Kube-Solo icon in your menu bar.

Verify that Kubernetes is running by clicking on the Kube-Solo icon and choosing “Kubernetes Dashboard”

Increase Docker memory

I had to increase the amount of memory in the Docker configuration to get Spinnaker working properly. I set mine to 8GB.

  1. Click on the Docker app in the menu bar
  2. Click the “Preferences” menu option
  3. Choose the amount of memory (8GB worked for me).
  4. Click “Apply & Restart”

Docker hub account

You will also need an account on Docker Hub, since we will configure Spinnaker to use Docker Hub as our image registry, and Spinnaker needs to know what your Docker Hub credentials are to download container images.

Grab the Spinnaker source

We will run Spinnaker from containers that have been previously uploaded to the Quay container registry, but we need the local code because it contains the Docker compose config files that we will use to run Spinnaker.

$ git clone https://github.com/spinnaker/spinnaker.git
$ cd spinnaker

Copy your kubeconfig file to config directory

Spinnaker requires your kubeconfig file which tells it how to connect to your Kubernetes deployment.

$ cp ~/kube-solo/kube/kubeconfig config/kubeconfig

The experimental/docker-compose/docker-compose.override.yml file is configured by default to mount the config directory into the clouddriver container as /opt/spinnaker/config.

Edit config/clouddriver.yml

In the Spinnaker repository that you just checked out, the config/clouddriver.yml file contains configuration for the backend cloud providers that Spinnaker uses. We need to configure it for Kubernetes and for the Docker registry.

Here’s how I configured mine, by modifying the kubernetes and dockerRegistry fields.

kubernetes:
  enabled: true
  accounts:
      - name: kubesolo
        kubeconfigFile: /opt/spinnaker/config/kubeconfig
        dockerRegistries:
            - accountName: docker-hub

dockerRegistry:
    enabled: true
    accounts:
        - name: docker-hub
          address: https://index.docker.io
          username: your-docker-hub-username-goes-here
          password: your-docker-hub-password-goes-here
          repositories:
               - library/nginx

The example above will only allow you to run containers from the nginx repository. In a real deployment, you’d add more repositories, but nginx containers are just fine for local testing.

Start up Spinnaker using Docker Compose

Switch to the directory that contains the Docker Compose config files and start up all of the Spinnaker containers:

$ cd experimental/docker-compose
$ DOCKER_IP=localhost docker-compose up -d

It will take a few minutes for Spinnaker to come up.

Open Spinnaker in your browser

Docker Compose is configured to expose the Spinnaker web UI at http://localhost:9000.

Next, you can check out the Kubernetes Source To Prod code lab on the Spinnaker website for how to launch an app.

Posted in Uncategorized | Tagged , , | 1 Comment

Go: Pointer to methods

Go: Pointer to methods

Sometimes I need a pointer to a method that is not bound to an explicit object.

Method pointers are just function pointers where the first argument is the type.

Imagine we have a Pet type with a Speak method:

type Pet interface {
    Speak() string
}

Here’s how we would declare, assign, and invoke the pointer

var fp func(Pet) string
fp = Pet.Speak

pet := GetPetFromSomewhere()
fmt.Sprintf("The pet says: %s\n", fp(pet))
Posted in Uncategorized | Tagged | Leave a comment

Getting timestamp from v1 uuid

Getting timestamp from v1 uuid

Translated from J.B. Langston’s Converting TimeUUID Strings to Dates Java version to Python:

import arrow
import fileinput
import uuid

def main():
    for line in fileinput.input():
        line = line.rstrip()
        value = uuid.UUID(line)
        epoch_millis = (value.time - 0x01b21dd213814000) / 10000
        epoch = epoch_millis / 1000
        ts = arrow.get(epoch)
        print(ts)

if __name__ == "__main__":
    main()
Posted in Uncategorized | Leave a comment