Skip to content

Instantly share code, notes, and snippets.

@shhyou
shhyou / solver.rkt
Created July 20, 2021 13:41
A tiny example for launching the Z3 process and interact with S-expression in SMTLIB syntax
#lang racket/base
(require racket/match)
(provide current-solver-path
call-with-solver
solve)
(define current-solver-path (make-parameter (find-executable-path "z3")))
@soegaard
soegaard / uniq.rkt
Created August 18, 2019 16:26
Uniq for Racket lists
#lang racket/base
(provide uniq)
;;;
;;; Uniq
;;;
; The function uniq takes a list as input and returns a new list:
; adjacent elements are compared and omits any repeated elements.
; In other words, uniq works like the Unix utility uniq, but on list.
@swatson555
swatson555 / compile.ss
Created June 22, 2022 13:13
nanopass compiler for r0 language
#!/usr/bin/env scheme --script
(import (nanopass))
(define unique-var
(let ()
(define count 0)
(lambda (name)
(let ([c count])
(set! count (+ count 1))
@soegaard
soegaard / sicp-concurrency.rkt
Created December 16, 2018 16:48
Concurrency primitives for SICP for Racket 7
#lang racket
;; adapted from:
;; https://planet.racket-lang.org/package-source/dyoo/sicp-concurrency.plt/1/2/sicp-concurrency.ss
;; concurrency: SICP concurrency primitives
;; adapted from http://list.cs.brown.edu/pipermail/plt-scheme/2002-September/000620.html
;;; Sources:
;;; Dorai Sitaram, "Learn Scheme in a Fixnum of Dayes", chapter 15
;;; Dyvig, http://www.scheme.com/tspl2d/examples.html#g2433
type expr =
| Var of string
| Int of int
| Add of (expr * expr)
| Mult of (expr * expr)
| Let of (string * expr * expr)
| IfZero of (expr * expr * expr)
| Pair of (expr * expr)
| Zro of expr
| Fst of expr

ffmpeg Cheatsheet

-loglevel debug
  • Join TS Files
  • Convert TS to MP4
  • Download Online AES-128 Encrypted HLS video
  • Convert Video to GIF
@paulcadman
paulcadman / idris_hands_on.md
Last active September 25, 2025 11:32
Curry-Howard in Idris

Types are theorems, programs are proofs.

(The code examples here use idris https://www.idris-lang.org)

To augment testing with a finite number of inputs we write mathematical proofs that demonstrate their correctness on all possible inputs.

The programmer writes the proofs and the compiler checks the proofs as it builds the software.

@MattPD
MattPD / analysis.draft.md
Last active November 29, 2025 20:13
Program Analysis Resources (WIP draft)
@nauhygon
nauhygon / Build Emacs for Windows 64bit with Native Compilation.md
Last active December 30, 2025 17:10
Step-by-step instructions to build Emacs for Windows 64 bit with MSYS2 and MinGW-w64. Now `native-comp` supported.

Build Emacs-w64 with MSYS2/MinGW-w64 with Native Compilation

Instructions are modified from emacs-w64 Wiki page by zklhp. Many thanks for sharing!

  1. Download the latest MSYS2 from this download page.

  2. Install MSYS2 to, for example, C:\msys2 (make sure no space in path to avoid unwanted problems).

  3. Optionally prettify the MSYS2 console mintty with ~/.minttyrc to make it more pleasing to eyes. Thanks to this awesome theme!