Skip to content

Instantly share code, notes, and snippets.

View hoelzro's full-sized avatar

Rob Hoelz hoelzro

View GitHub Profile
@hoelzro
hoelzro / Dockerfile
Last active May 18, 2019 17:52
Docker file for Sputnik wiki
FROM ubuntu
RUN apt-get update && apt-get install -y lua5.1 unzip build-essential luarocks
ADD sputnik-galaxy-12-07-12-all-in-one.zip /
WORKDIR /tmp
RUN unzip /sputnik-galaxy-12-07-12-all-in-one.zip
WORKDIR /tmp/sputnik-galaxy-12-07-12-all-in-one
RUN ./install.sh --lua-suffix=5.1 --without-readline
package main
import (
"bufio"
"bytes"
"encoding/binary"
"fmt"
"io"
"os"
"path"
$ xinput list
⎣ Virtual core keyboard id=3 [master keyboard (2)]
↳ Virtual core XTEST keyboard id=5 [slave keyboard (3)]
↳ Metadot - Das Keyboard Das Keyboard id=10 [slave keyboard (3)]
↳ Metadot - Das Keyboard Das Keyboard id=11 [slave keyboard (3)]
xkb_keymap {
xkb_keycodes { include "evdev+aliases(qwerty)" };
xkb_types { include "complete" };
xkb_compat { include "complete" };
xkb_symbols { include "pc+us+inet(evdev)+ctrl(swapcaps)" };
xkb_geometry { include "pc(pc104)" };
};
import sys
from wikiXMLDump import WikiXMLDumpFile
for filename in sys.argv[1:]:
dump = WikiXMLDumpFile(filename)
for doc in dump.getWikiDocuments():
print(doc.title)
data Even : (n : Nat) -> Type where
MkEven : (half_n : Nat) -> Even (half_n + half_n)
oddIsOdd : Even (S (n + n)) -> Void
oddIsOdd _ impossible
{-
Type checking ./Even.idr
Even.idr:5:12-21:
package Local::Twitter::API::RateLimiting {
use Moo::Role;
use HTTP::Status qw(HTTP_TOO_MANY_REQUESTS);
use namespace::clean;
around send_request => sub {
my $orig = shift;
my $self = shift;
browser.webNavigation.onCommitted.addListener(details => {
console.log(details);
});
import Data.Vect
import Data.Nat.DivMod
-- rotates a vector's elements. Note that from the type signature,
-- you can't rotate more than the length of the vector
rotate : (n : Nat) -> Vect (n + m) a -> Vect (n + m) a
-- {m} captures m, which is an implicit parameter - we'll need it for a proof below
rotate {m} n xs =
let newSuffix = take n xs
newPrefix = drop n xs
/*\
title: $:/modules/yyyymm.js
type: application/javascript
module-type: macro
Macro to return a the current year and month in YYYY-MM format.
\*/
(function(){
/*jslint node: true, browser: true */