Skip to content

Instantly share code, notes, and snippets.

View stedolan's full-sized avatar

Stephen Dolan stedolan

1.2k followers · 13 following
View GitHub Profile
@stedolan
stedolan / perf.c
Last active October 29, 2025 16:41
#include <linux/perf_event.h>
#include <linux/hw_breakpoint.h>
#include <sys/syscall.h>
#include <unistd.h>
#include <stdio.h>
#include <errno.h>
#include <sys/mman.h>
#include <stdint.h>
#include <assert.h>
#include <x86intrin.h>
@stedolan
stedolan / laziness.ml
Last active October 18, 2025 04:13
(* An implementation of (part of) the lazy data structure of:
First-Order Laziness
Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley
ICFP 2025
Requires OCaml 5.2+ / OxCaml *)
module type LazyS = sig
type _ repr
@stedolan
stedolan / hugebench.ml
Created September 18, 2025 19:35
let enable_hugepages () =
let ch = open_in "/proc/self/maps" in
let module Syscall = struct
external madvise : (int64[@unboxed]) -> (int64[@unboxed]) -> (int[@untagged]) -> (int[@untagged]) =
"unimplemented" "madvise"
end in
try
while true do
Scanf.sscanf (input_line ch) "%Lx-%Lx %s %Lx %x:%x %Ld %s"
(fun start_addr end_addr perms offset devmaj devmin inode path ->
@stedolan
stedolan / window.md
Last active August 20, 2025 15:33

Generating good code for bitfields

Here's a definition of the packed 16-bit RGB565 pixel format as a C struct:

typedef struct { unsigned r : 5, g : 6, b : 5; } pixel;

and a couple of functions that operate on it:

@stedolan
stedolan / darkening.ml
Created February 11, 2025 11:33
let table = Array.init 10_000 (fun _ -> Bytes.make 1_000 'a')
let writes =
Option.map bool_of_string (Sys.getenv_opt "WRITES")
|> Option.value ~default:false
let[@inline never] f () =
List.init (Array.length table) (fun i ->
let buf = table.(i) in
if writes then table.(i) <- buf;
@stedolan
stedolan / Injective.hs
Last active March 26, 2024 17:44
{-# LANGUAGE GADTs #-}
-- nontermination without any recursion, even in types
-- possible because of impredicativity + injectivity
-- based on https://gist.github.com/leodemoura/0c88341bb585bf9a72e6
-- see also https://github.com/idris-lang/Idris-dev/issues/3687
data False
data I (f :: * -> *) where
@stedolan
stedolan / prombench.ml
Last active April 2, 2024 09:44
let promotion_rate = 50
let collection_rate = 30
let ballast_mb = 100
let iters_m = 50
let rand =
let counter = ref 43928071 in
fun () ->
let n = !counter in
counter := n * 454339144066433781 + 1;
@stedolan
stedolan / GenericTrees.agda
Created September 3, 2022 09:32
module GenericTrees where
open import Agda.Builtin.String
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Primitive
variable l : Level
-- Products and sums
@stedolan
stedolan / emftaps.sh
Created June 3, 2022 17:14
while :; do clear; curl -skL https://bar.emf.camp/api/on-tap.json | jq -r 'keys[] as $k | ("--", ("\($k):"), (.[$k][] | "\(.manufacturer) \(.name) (\(.abv)%)@\(.price)\(if .remaining_pct|tonumber<5 then " (running out)" else "" end)"))' | column -t -s '@'; sleep 10; done
@stedolan
stedolan / VarBug.agda
Created May 29, 2022 06:14
-- Is this a bug in Agda?
-- Try repro with latest agda sometime
module VarBug where
open import Agda.Builtin.Equality
open import Agda.Primitive
data Unit : Set where
tt : Unit