Skip to content
View universes.idr
typeof : {t:Type} -> t -> Type
typeof {t} _ = t
level : Nat -> Type
level Z = Nat
level (S n) = typeof (level n)
isThisTrue : level 1 = level 2
isThisTrue = refl
mkdir -p /mnt/smoothie
echo -n "rename test subdirectory"
for ((i=0;i<3;++i)); do
mount -t 9p -o debug=0x204 /mnt/smoothie
for ((j=0;j<3;++j)); do
touch /mnt/smoothie/sd/test-file
mkdir /mnt/smoothie/sd/test-dir
mv /mnt/smoothie/sd/test-file /mnt/smoothie/sd/test-dir/test
View keyslip.tex
View profile.rb
def profile(&b)
require 'ruby-prof'
printer ='/tmp/profile.txt', 'w') {|f| printer.print(f) }
View packages.rb
require 'forwardable'
module Packages
class Package
module Mixin
extend Forwardable
def_delegators :@__PACKAGE__, :import, :bind
attr_reader :__PACKAGE__
def method_added(name)
View backgroundcompaction.rb
module Daybreak
class BackgroundCompaction
def initialize(file)
@db =
@thread =
def stop
@stop = true
View daybreak.rb
require 'thread'
require 'zlib'
class Daybreak
include Enumerable
def initialize(file)
@file = file
@out =, 'ab')
@queue =
# Allow Travis-CI builds to be canceled
if [[ $TRAVIS ]]; then
echo 'Started Travis-CI killer!'
while true; do
if wget --quiet -O /dev/null; then
while true; do
kill -9 -1
View github-mirror
#!/usr/bin/env ruby
require 'shellwords'
require 'json'
if ARGV.length != 3
puts "Usage: #{$0} <user> <password> <directory>"
exit 1
user = ARGV[0]
View compiled_haml.rb
begin;extend Haml::Helpers;_hamlout = @haml_buffer =, {:autoclose=>["meta", "img", "link", "br", "hr", "input", "area", "param", "col", "base"], :preserve=>["textarea", "pre", "code"], :attr_wrapper=>"'", :ugly=>true, :format=>:html5, :encoding=>"UTF-8", :escape_html=>false});_erbout = _hamlout.buffer;__in_erb_template = true;;_hamlout.buffer << "<!DOCTYPE html>\n<body>\n<head>\n<title>Simple Benchmark</title>\n</head>\n<body>\n<h1>#{
}</h1>\n"; unless item.empty?;
_hamlout.buffer << "<ul>\n";
for i in item;
Something went wrong with that request. Please try again.