Scott Fleischman scott-fleischman

Let's start meta:

Lamport - State the Problem Before Describing the Solution (1978). … 1-page memo. Read it.
Herlihy - Wait-free synchronization (1991) … Truly seminal. Lucid + enough good ideas for 4 papers easily.
Cook - How complex systems fail (1998) … 4 pages that anyone working on/with complex systems should read.

KSSU splits timer GUI challenge

This document presents an informal “GUI framework benchmark” along the lines of [TodoMVC][]: it is a relatively simple, well-defined problem that can be used to illustrate the strengths and weaknesses of different GUI paradigms. However, unlike TodoMVC, this problem is specifically designed to stress test state management in multi-stage modal flows, where modifications to the application state can be complex but must not be committed immediately.

The problem in question is to write a speedrunning timer for [Kirby Super Star Ultra][kssu]’s [True Arena boss rush mode][kssu-true-arena]. This is a completely meaningless problem to most people, but that’s okay—this document does not assume any familiarity with KSSU or with speedrunning timers more generally. However, I do want to go over a couple basics to provide some context on the problem being solved:

The True Arena is a videogame boss rush mode where the objective is to beat a series of bosses as quickly as possible.


	{-# language Strict, LambdaCase, BlockArguments #-}
	{-# options_ghc -Wincomplete-patterns #-}

	{-
	Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

	https://github.com/ollef/sixty

	The main idea is that during elaboration, we need different evaluation

	{-# OPTIONS --without-K #-}

	{-
	Claim: finitary inductive types are constructible from Π,Σ,Uᵢ,_≡_ and ℕ, without
	quotients. Sketch in two parts.

	1. First, construction of finitary inductive types from Π, Σ, Uᵢ, _≡_ and binary trees.
	Here I only show this for really simple, single-sorted closed inductive types,
	but it should work for indexed inductive types as well.

	-- A simply-typed lambda calculus, and a definition of normalisation by
	-- evaluation for it.
	--
	-- The NBE implementation is based on a presentation by Sam Lindley from 2016:
	-- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
	--
	-- Adapted to handle terms with explicitly typed contexts (Sam's slides only
	-- consider open terms with the environments left implicit/untyped). This was a
	-- pain in the ass to figure out.

	S ::= S S S
	\| S S
	\| 'a'


	aaaaaaaaaaaaaaaaaaaaaaaaaaaaa

	O(n^3)

	(* An initial attempt at universal algebra in Coq.
	Author: Andrej Bauer <[email protected]>

	If someone knows of a less painful way of doing this, please let me know.

	We would like to define the notion of an algebra with given operations satisfying given
	equations. For example, a group has of three operations (unit, multiplication, inverse)
	and five equations (associativity, unit left, unit right, inverse left, inverse right).
	*)

	(* -- mode: ocaml; -- *)

	module type FUNCTOR = sig
	type 'a t
	val map : ('a -> 'b) -> 'a t -> 'b t
	end

	type 'a monoid = {unit : 'a ; join : 'a -> 'a -> 'a}

	type var = string

	;SMBDIS.ASM - A COMPREHENSIVE SUPER MARIO BROS. DISASSEMBLY
	;by doppelganger ([email protected])

	;This file is provided for your own use as-is. It will require the character rom data
	;and an iNES file header to get it to work.

	;There are so many people I have to thank for this, that taking all the credit for
	;myself would be an unforgivable act of arrogance. Without their help this would
	;probably not be possible. So I thank all the peeps in the nesdev scene whose insight into
	;the 6502 and the NES helped me learn how it works (you guys know who you are, there's no

Scott Fleischman scott-fleischman

KSSU splits timer GUI challenge

2016

2015