Skip to content

Instantly share code, notes, and snippets.

Mostly unresponsive these days

Daniel Peebles copumpkin

Mostly unresponsive these days
View GitHub Profile
#!/usr/bin/env python
from os import listdir
from os.path import isfile, join
import re
import json
from bs4 import BeautifulSoup
shortjared / list.txt
Last active Jul 23, 2021
List of AWS Service Principals
View list.txt

General notes

  • nix-channel and ~/.nix-defexpr are gone. We'll use $NIX_PATH (or user environment specific overrides configured via nix set-path) to look up packages. Since $NIX_PATH supports URLs nowadays, this removes the need for channels: you can just set $NIX_PATH to e.g. and stay up to date automatically.

  • By default, packages are selected by attribute name, rather than the name attribute. Thus nix install hello is basically equivalent to nix-env -iA hello. The attribute name is recorded in the user environment manifest and used in upgrades. Thus (at least by default) hello won't be upgraded to helloVariant.

    @vcunat suggested making this an arbitrary Nix expression rather than an attrpath, e.g. firefox.override { enableFoo = true; }. However, such an expression would not have a key in the user environment, unlike an attrpath. Better to require an explicit flag for this.

    TBD: How to deal with search path clashes.

andrejbauer / topology.v
Last active May 24, 2021
How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.
View topology.v
(* How do to topology in Coq if you are secretly an HOL fan.
We will not use type classes or canonical structures because they
count as "advanced" technology. But we will use notations.
(* We think of subsets as propositional functions.
Thus, if [A] is a type [x : A] and [U] is a subset of [A],
[U x] means "[x] is an element of [U]".
Definition P (A : Type) := A -> Prop.
View Mat.idr
module Matrices
-- Vector stuff ~ maybe put Prelude.Vect
||| Dot product between numerical vectors
dot : Num a => Vect n a -> Vect n a -> a
dot w v = sum (zipWith (*) w v)
||| Numerical vector times a scalar of the appropriate type
copumpkin / Prickler.hs
Last active Aug 29, 2015
Reasonably painless bidirectional serialization of sums of products
View Prickler.hs
{-# LANGUAGE TemplateHaskell, ExistentialQuantification, RankNTypes, GADTs, ImplicitParams, TypeFamilies, DataKinds, TypeOperators, DeriveGeneric, PolyKinds #-}
module Prickler where
Main goals:
# Minimal indirection, so I didn't want big n-tuples of stuff getting curried into constructors or shit like that
# Magical constructor/eliminator pairing, so I don't have to write ugly unsafe pattern matches or constructor -> Int mappings (unlike the alt combinator in the pickler paper)
# Minimize the amount of metadata traversal that happens during serialization (not 100% there yet)
# Not be ugly to use
sjoerdvisscher / skewbintree.hs
Last active Dec 23, 2015
Skew binary tree with the invariants enforced by the type system, using a nested data type.
View skewbintree.hs
type Id = Int
data Path a where
P :: P a -> Path a
Two :: b -> b -> P (Br b) -> (P (Br b) -> P a) -> Path a
data Br a = Br a Id a
data P a = Nil | Zero (P (Br a)) | One a (P (Br a))
twanvl / Sorting.agda
Created May 23, 2013
Correctness and runtime of mergesort, insertion sort and selection sort.
View Sorting.agda
module Sorting where
open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Relation.Nullary