hwayne

-- Put this in after/plugins

local api = vim.api

local function chunk(text)
  local sections = {}

  for line in vim.gsplit(text, "@@@") do
      if line:find("^s") then
          table.insert(sections, {role = "system", content = line:sub(3)})

hwayne

People who take my TLA+ Class get a free specification review. Cory Myers asked for a review of his Reply.tla spec, reproduced from the PR below, and has graciously agreed to let me make it public. The review itself is here.

Note this is a "light" review: I'm looking for general TLA+ antipatterns and techniques that don't require me to deeply understand the problem domain. This represents about an hour of review.

hwayne

# This is running on an aws lambda instance with a CloudWatch trigger:
# Trigger is cron(0 17 * * ? *)
# CSV is from https://www.mlb.com/cubs/schedule/downloadable-schedule

import json
from urllib.request import urlopen, Request
from urllib.parse import urlencode
from os import getenv
from csv import DictReader
from datetime import datetime

hwayne

enum Val {On, Off}

sig P {} //"Permutation"
abstract sig Input {
  val: Val one -> P
}

sig Source extends Input {}

abstract sig Gate extends Input {

hwayne

I forget I added it to the firefox store so hopefully you're smarter than I am srry

Also you'll need a "border-48.png" icon which is in the manifest file

hwayne

---- MODULE Filters ----
EXTENDS TLC, Integers
VARIABLE push_msgs, emails, i, filtered, pushed
vars == <<push_msgs, emails, i, filtered, pushed>>

set ++ x == set \union {x}
set -- x == set \ {x}

TypeInv ==
    /\ emails \subseteq (1..3)

hwayne

---- MODULE BubbleSort ----
EXTENDS Integers, TLC, Sequences, FiniteSets

Counter(seq) == 
  LET
   Range == {seq[x] : x \in DOMAIN seq}
   CountOf(x) == Cardinality({i \in 1..Len(seq): seq[i] = x})
  IN
    [val \in Range |-> CountOf(val)]

hwayne

" TODO: MAKE THIS ALL USE AUTOLOAD
" Macro Handling {{{

let s:macro_file = g:exo . 'macros.json'

function! s:macro_list(ArgLead, CmdLine, CursorPos)
  let macros = json_decode(readfile(s:macro_file))
  return join(keys(macros), "\n")
endfunction

hwayne

How the J Script Works

Going line by line:

b =: >: i. 9 9 9

This generates a 9 by 9 by 9 array with all values from 1 to 729. We can choose what each axis represents: I decided that each table is all of the boolean variables for one number, and the rows and columns map to sudoku rows and columns. For example:

hwayne

A while back I complained on Twitter about how Ada Lovelace is used as an example of "an important woman in CS", because she's a pretty terrible example (thread in comments), and listed some better choices. In response, somebody said that public people get why Lovelace is interesting, whereas it's hard to explain why, like, Barbara Liskov matters so much. That got me interested in explaining the contributions to CS in ways that are understandable to people with no tech background. Here's my attempt to explain Frances E Allen, who did foundational work in optimizing compilers:

---

Without Frances Allen, our videogames would be stuck in the SNES era.

So at a fundamental level, a computer is just a bag of buckets of data (memory addresses), and a program is just instructions ot move data between the buckets. Like mov edx, [ebp + 8] means "take the data in the 8th bucket after the ebp bucket and move it to the edx bucket." All programs eventually become this "assembly" language that the computer execut