Steven Shaw steshaw

Remote, Office Not Required

The office during the day has become the last place people want to be when then really want to get work done.

Offices have become interruption factories: it's just one interruption after

This simple script will take a picture of a whiteboard and use parts of the ImageMagick library with sane defaults to clean it up tremendously.

The script is here:

#!/bin/bash
convert "$1" -morphology Convolve DoG:15,100,0 -negate -normalize -blur 0x1 -channel RBG -level 60%,91%,0.1 "$2"

	record Person : Nat -> Type where
	MkPerson : (name : String) ->
	(age : Nat) ->
	Person age

	record Event : Type where
	MkEvent : (name : String) -> (organiser : Person a) -> Event

	record Meeting : Int -> Type where
	MkMeeting : (event : Event) ->

	(* Here is some client code that needs to
	construct a proof about fac. Because it doesn't
	rely on any particular representation of
	nats, it imports the abstract nat interface;
	thus it could be linked against Peano, binary,
	and other implementations of the nat interface. *)

	(* Assume 'Nat' refers to the abstract spec, NatSpec. *)
	Import Nat

	// Quasiquoted excerpt

	def cdef = q"""
	class $ClassName[..$classTypeParams](..$primaryParams) extends ..$classParents {
	..$primaryAccessors

	def get = this
	def isEmpty = ${quasi.isEmpty}
	def copy(..$primaryWithDefaults) = $ObjectName(..$primaryNames)

	-- Working through the Yorgey lectures on Applicatives for Haskell and trying to work out the homework...

	-- A parser for a value of type a is a function which takes a String
	-- represnting the input to be parsed, and succeeds or fails; if it
	-- succeeds, it returns the parsed value along with the remainder of
	-- the input.
	newtype Parser a = Parser { runParser :: String -> Maybe (a, String) }

	-- For example, 'satisfy' takes a predicate on Char, and constructs a
	-- parser which succeeds only if it sees a Char that satisfies the

	$ cabal sandbox init
	$ cabal install idris
	$ echo 'main : IO () ; main = print "hello"' >hello.idr
	$ ./.cabal-sandbox/bin/idris --mvn --codegen Java -o hello hello.idr
	$ cd hello
	$ mvn -DmainClass=hello package shade:shade
	$ java -jar target/hello.jar
	"hello"