jcreedcmu

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

// 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

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

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

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

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

jcreedcmu

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

/***
 * 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

// 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

jcreedcmu

const W = 52;
const H = 30;
const MAX_ITER = 1000;

function iters(cr, ci) {
  let zi = 0;
  let zr = 0;
  for (let i = 0; i < MAX_ITER; i++) {
    [zr, zi] = [zr * zr - zi * zi + cr,  2 * zr * zi + ci];
    if (zr * zr + zi * zi > 16.0) return i;