Skip to content

Instantly share code, notes, and snippets.

Give me back my sanity

One of the many things I do for my group at work is to take care of automating as many things as possible. It usually brings me a lot of satisfaction, mostly because I get a kick out of making people's lives easier.

But sometimes, maybe too often, I end up in drawn-out struggles with machines and programs. And sometimes, these struggles bring me to the edge of despair, so much so that I regularly consider living on a computer-less island growing vegetables for a living.

This is the story of how I had to install Pandoc in a CentOS 6 Docker container. But more generally, this is the story of how I think computing is inherently broken, how programmers (myself included) tend to think that their way is the way, how we're ultimately replicating what most of us think is wrong with society, building upon layers and layers of (best-case scenario) obscure and/or weak foundations.

*I would like to extend my gratitude to Google, StackOverflow, GitHub issues but mostly, the people who make the

@mnot
mnot / snowden-ietf93.md
Last active September 12, 2023 13:40
Transcript of Edward Snowden's comments at IETF93.
#!/bin/bash
set -e
CONTENTS=$(tesseract -c language_model_penalty_non_dict_word=0.8 --tessdata-dir /usr/local/share/tessdata/ "$1" stdout -l eng | xml esc)
hex=$((cat <<EOF
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
<plist version="1.0">
@bobatkey
bobatkey / cont-cwf.agda
Last active June 16, 2023 21:23
Construction of the Containers / Polynomials CwF in Agda, showing that function extensionality is refuted
{-# OPTIONS --rewriting #-}
module cont-cwf where
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq
@minrk
minrk / nbstripout
Last active June 6, 2023 06:23
git pre-commit hook for stripping output from IPython notebooks
#!/usr/bin/env python
"""strip outputs from an IPython Notebook
Opens a notebook, strips its output, and writes the outputless version to the original file.
Useful mainly as a git filter or pre-commit hook for users who don't want to track output in VCS.
This does mostly the same thing as the `Clear All Output` command in the notebook UI.
LICENSE: Public Domain
@andrejbauer
andrejbauer / Epimorphism.agda
Last active January 26, 2023 20:44
A setoid satisfies choice if, and only if its equivalence relation is equality.
open import Level
open import Relation.Binary
open import Data.Product
open import Data.Unit
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality renaming (refl to ≡-refl; trans to ≡-trans; sym to ≡-sym; cong to ≡-cong)
open import Relation.Binary.PropositionalEquality.Properties
open import Function.Equality hiding (setoid)
module Epimorphism where
@mckamey
mckamey / bezier.js
Created September 25, 2012 16:35
JavaScript port of Webkit CSS cubic-bezier(p1x.p1y,p2x,p2y) and various approximations
/*
* Copyright (C) 2008 Apple Inc. All Rights Reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions
* are met:
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
@twanvl
twanvl / Sorting.agda
Last active December 2, 2022 16:44
Correctness and runtime of mergesort, insertion sort and selection sort.
module Sorting where
-- See https://www.twanvl.nl/blog/agda/sorting
open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List hiding (merge)
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans)
open import Data.Nat.Logarithm
open import Data.Nat.Induction
@malarkey
malarkey / Three Wise Monkeys.md
Created December 2, 2012 14:26
Three Wise Monkeys (NDA)

Date: [date]

Between us [company name] and you [customer name].

Summary:

In short; neither of us will share any confidential information about each-other, by any means, with anyone else.

What’s confidential information?

@TOTBWF
TOTBWF / CartesianNbE.agda
Last active February 5, 2022 23:24
NbE for Cartesian Categories
{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core
open import Categories.Category.Cartesian
module Categories.Tactic.Cartesian.Solver {o ℓ e} {𝒞 : Category o ℓ e} (cartesian : Cartesian 𝒞) where
open import Level
open import Categories.Category.BinaryProducts