noamsdahan

0xdabbad00

#!/usr/bin/env python

from os import listdir
from os.path import isfile, join
import re
import json

from bs4 import BeautifulSoup

"""

shortjared

a4b.amazonaws.com
access-analyzer.amazonaws.com
account.amazonaws.com
acm-pca.amazonaws.com
acm.amazonaws.com
airflow-env.amazonaws.com
airflow.amazonaws.com
alexa-appkit.amazon.com
alexa-connectedhome.amazon.com
amazonmq.amazonaws.com

edolstra

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

(* 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.

fieldstrength

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

{-# 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

{-# 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

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