Skip to content

Instantly share code, notes, and snippets.

@jcreedcmu
jcreedcmu / PredArith.agda
Created November 10, 2024 23:09
Predicative Arithmetic
module PredArith where
data void : Set where
abort : {A : Set} → void → A
abort ()
postulate
ι : Set
@jcreedcmu
jcreedcmu / firefox-hg-query.txt
Created July 30, 2024 17:13
firefox hg query.txt
hg log -r 'FIREFOX_BETA_127_END::FIREFOX_128_0b1_RELEASE' --template "{rev}: {node|short} {date|isodate} {author|person} {desc|firstline}\n"
820035: 2738f5657419 2024-06-03 14:51 +0000 Mozilla Releng Treescript No bug - tagging 5d25cb332db85c8bb2cda40840be406437ec5e98 with FIREFOX_RELEASE_127_BASE a=release DONTBUILD CLOSED TREE
823723: f0900bab4570 2024-06-10 14:49 +0000 Mozilla Releng Treescript Merge old head via |hg debugsetparents af9948205327480d29bfcb960d5308ad4a2d0ce7 2738f5657419fba3ece0bc829732f8dfdce7c70a| CLOSED TREE DONTBUILD a=release
823724: 326824a2c3a7 2024-06-10 14:49 +0000 Mozilla Releng Treescript Preserve old tags after debugsetparents. CLOSED TREE DONTBUILD a=release
823725: 4926489e7390 2024-06-10 14:49 +0000 Mozilla Releng Treescript No bug - tagging 2738f5657419fba3ece0bc829732f8dfdce7c70a with FIREFOX_BETA_127_END a=release DONTBUILD CLOSED TREE
823726: 15a675544fcb 2024-06-10 14:49 +0000 Mozilla Releng Treescript no bug - Bumping Firefox l10n changesets r=release a=l10n-bump CLOSED
@jcreedcmu
jcreedcmu / cvm.js
Last active July 17, 2024 23:06
cvm.js
// A quick and dirty lil implementation of the CVM algorithm
// (https://arxiv.org/pdf/2301.10191)
//
// I put Moby Dick (https://www.gutenberg.org/cache/epub/2701/pg2701.txt)
// into /tmp/mb.txt
const fs = require('fs');
const mb = fs.readFileSync('/tmp/mb.txt', 'utf8')
.replace(/[^a-zA-Z-’]/g, ' ')
.split(/\s+/);
@jcreedcmu
jcreedcmu / puzzle.md
Last active April 26, 2024 18:27
puzzle.md

Puzzle

There is a party with 37 people. Every pair of them is either friends or not friends. Alice and Bob are the only two people at the party with the same number of friends. Alice and Bob are not friends with each other.

How many people are:

  • friends with both Alice and Bob?
  • friends with Alice and not Bob?
@jcreedcmu
jcreedcmu / parametricity.txt
Last active April 14, 2024 13:19
parametricity.txt
If I have
𝔹 : ∀X. X → X → X
then parametricity tells me
(b : 𝔹)(f : X → Y)(x₁ x₂ : X) → f (b x₁ x₂) = b (f x₁) (f x₂).
From this I want to prove
@jcreedcmu
jcreedcmu / fixpoint.txt
Last active March 19, 2024 21:28
lil fixpoint lemma
Suppose ℂ is a ω-cocomplete category: it has colimits of any
diagram that is a functor ω → ℂ. Suppose ℂ has an initial object ⊥.
Suppose F is a functor ℂ → ℂ that preserves all ω-colimits.
Let U : ω → ℂ be the diagram
! F! F²
⊥ → F(⊥) → F²(⊥) → ⋯
Lemma: If we have a map m : FA → A, then we can construct a map colim U → A.
@jcreedcmu
jcreedcmu / chaotic.agda
Last active March 18, 2024 00:09
proof of correctness of chaotic iteration
open import Agda.Primitive
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
constructor _,_
field
fst : A
Lemma 2: ("Real Induction") Let A be a subset of real numbers.
If
(0) α ∈ A
(1) ∀x ∈ A. ∃y. [x,y) ⊆ A
(2) ∀xy. [x, y) ⊆ A ⇒ y ∈ A
then [α,∞) ⊆ A.
Proof:
Suppose towards a contradiction that [α,∞) ∖ A is nonempty. Set β = inf ([α,∞) ∖ A).
(1) means we can't have β ∈ A, because it would collide with the infimum.
@jcreedcmu
jcreedcmu / self-modify.ts
Created March 17, 2023 22:35
Snippet of typescript that modifies itself in an emacs buffer
/***
* A little bit of research into what would be needed for a "direct manipulation" toy in emacs.
* - NodeJS allows replacing `Error.prepareStackStrace` with a custom handler that can obtain
* first-class stack trace data.
* - An arbitrary function call (see below, `knob(1429)` for example) can obtain a stack
* trace and inspect it to find out where in the file the actual call to knob(1429) took place.
* - Since we're in typescript, we can also find the sourcemap and use it to map this into
* a location into the original `.ts` file.
* - We can shell out to emacsclient to evaluate arbitrary elisp
* - It can in turn go to the appropriate place in the active buffer viewing the `.ts` file,
@jcreedcmu
jcreedcmu / b.cc
Last active December 28, 2022 16:49
minimal sdl2/opengl example
// g++ -I/usr/local/include/SDL2 -I/usr/include/GL b.cc -lSDL2 -lGL -lGLU -o b
#include <SDL2/SDL.h>
#include <SDL2/SDL_opengl.h>
#include <gl.h>
static SDL_Window *window;
static SDL_Renderer *renderer;
#define width 640