Hillel Wayne hwayne

Bsky spinner

Spins your avatar like a clock

Disclaimer: I set this up locally half a year ago and forgot all the steps, so the steps below may be wrong.

For the newsletter at: FILL IN

Run with Dafny 4.6.0, with the flag --standard-libraries.

	# Associated newsletter: https://buttondown.com/hillelwayne/archive/solving-linkedin-queens-with-smt/
	# See also: https://ryanberger.me/posts/queens/
	# And: https://github.com/ryan-berger/queens/blob/master/main.py

	from z3 import * # type: ignore
	from itertools import combinations, chain, product
	solver = Solver()
	size = 9

	# queens[n] = col of queen on row n

	-- Drop this in /after or /after/plugin/
	-- explanation at commands (at end of file)

	vim.g.exo = "where you store your data files"
	local filelinks_file = vim.g.exo .. 'filelinks.json'

	local function get_filelinks()
	return vim.fn.json_decode(vim.fn.readfile(filelinks_file))
	end

	local function moduleline() -- can't be a global as line can move
	local lines = vim.api.nvim_buf_get_lines(0, 0, -1, false)
	for idx, line in ipairs(lines) do
	if string.match(line, "%-+ MODULE [%w_]+ %-") then
	return idx, line
	end
	end
	end

	local function fix_module_string()

	SPECIFICATION Spec
	\* Add statements after this line.
	CONSTANTS
	Threads = {t1}
	NULL = NULL
	Keys = {k1}
	MaxId = 1
	BUGMODE = TRUE

	PROPERTY LockProp

	import xml.etree.ElementTree as ET
	from xml.etree.ElementTree import Element
	from copy import deepcopy
	from argparse import ArgumentParser
	from dataclasses import dataclass
	from string import Template
	from pathlib import Path
	import typing as t

	#Common issue is that I need to have multiple slightly different versions of the same spec, this is a helper to do that.

	function Ask {
	Param (
	[PSDefaultValue(Help="*")]
	[switch]$Fast,
	[Parameter(Position=1)]
	[Alias("M")]
	[int]$Tokens=256,
	[Alias("n")]
	[int]$Results=1,
	[Parameter(Mandatory=$true, Position=0)]