Skip to content

Instantly share code, notes, and snippets.

View jaykru's full-sized avatar

Jay Kruer jaykru

View GitHub Profile
#include <Adafruit_CC3000.h>
#include <Adafruit_CC3000_Server.h>
#include <ccspi.h>
#include <string.h>
#include <SPI.h> // spi bus support
#include <OneWire.h> // general serial communications library
#include <DallasTemperature.h> // for temperature sensor
// Constants: IFTTT key/triggers for temperature reporting and alarm
#define IFTTT_KEY "b9_YqwnM9KIUiQG-dPXQMGgvcfc1vAAJTd4Kiz3j4uo"
### Keybase proof
I hereby claim:
* I am jaykru on github.
* I am jaykru (https://keybase.io/jaykru) on keybase.
* I have a public key whose fingerprint is 26E4 EFBD 7E46 D915 444C 79D7 8EA8 679E BE63 8186
To claim this, I am signing this object:
@jaykru
jaykru / riscv-cross-shell.nix
Created July 26, 2019 05:12
riscv-cross-shell
with import ~/nixpkgs {
crossSystem = (import ~/nixpkgs {}).lib.systems.examples.riscv64-embedded; # TODO: do this in a less clunky way?
};
mkShell {
RISCV_PREFIX = "riscv64-none-elf-";
stdenv = multiStdenv; # multilib compilers?
buildInputs = [];
}
Definition time := nat.
Section Theft.
Context (Person Object: Set).
(* In this meme we model monopolistic ownership of objects as follows:
A person owns /with monopoly/ an object at time t if
they were consensually given the object by someone who owned the object at time t-1.
Retainment of an object over time is modeled as reflexive giving. *)
acpi
agda
bc
bogofilter
cmatrix
coq
coreutils
diffutils
dmenu
emacs
@jaykru
jaykru / hasse.py
Created February 10, 2021 16:41
quick and dirty script to generate hasse diagrams (under set inclusion) for all the topologies of a finite set
### usage notes:
# the graphviz `dot` program on my machine didn't like the output for some reason. no time to investigate.
# instead use https://rsms.me/graphviz/
# if the diagrams are too vertically squished, try ranksep=k as a property on the generated digraph
from gvgen import *
import more_itertools
two = [1,2]
three = [1,2,3]
@jaykru
jaykru / regexp_subset.ml
Created March 22, 2021 21:03
a little ocaml program to decide set inclusion for regular languages
type alphabet
type regexp =
| Empty (* empty string! *)
| Atom of alphabet
| Star of regexp
| Concat of regexp * regexp
| Union of regexp * regexp
let rec core = function
| Star r -> core r
#!/usr/bin/env python3
import torch
import torch.nn.functional as F
device = torch.device("cuda" if torch.cuda.is_available() else "cpu")
words = open('names.txt', 'r').read().splitlines()
chars = sorted(list(set(''.join(words))))
stoi = {s:i+1 for i,s in enumerate(chars)}
stoi['.'] = 0
itos = {i:s for s,i in stoi.items()}
@jaykru
jaykru / energy_mlp.ipynb
Last active February 5, 2023 23:59
Attempt at an energy minimization network for quadgrams
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@jaykru
jaykru / mc.lean
Last active March 19, 2023 19:56
McLean
import tactic.omega
import tactic
inductive LTL (T: Type) : Type
| injp : (T -> Prop) -> LTL
| false : LTL
| true : LTL
| imp : LTL -> LTL -> LTL
| until : LTL -> LTL -> LTL
| next : LTL -> LTL.