Skip to content

Instantly share code, notes, and snippets.

💭
Mostly unresponsive these days

Daniel Peebles copumpkin

💭
Mostly unresponsive these days
Block or report user

Report or block copumpkin

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View extract.py
#!/usr/bin/env python
from os import listdir
from os.path import isfile, join
import re
import json
from bs4 import BeautifulSoup
"""
@shortjared
shortjared / list.txt
Last active Oct 9, 2019
List of AWS Service Principals
View list.txt
acm.amazonaws.com
alexa-appkit.amazon.com
apigateway.amazonaws.com
application-autoscaling.amazonaws.com
appstream.application-autoscaling.amazonaws.com
appsync.amazonaws.com
athena.amazonaws.com
autoscaling.amazonaws.com
batch.amazonaws.com
channels.lex.amazonaws.com
View nix-ui.md

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. https://nixos.org/channels/nixos-15.09/nixexprs.tar.xz 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
andrejbauer / topology.v
Last active Mar 14, 2019
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
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
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
{-# LANGUAGE GADTs #-}
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
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
You can’t perform that action at this time.