Richard Mongler rplacd

Enabling Optimus support for your desktop GPU

Windows 10 users: you won't need this guide. NVidia has made signed drivers available with the modifications outlined here, although it's been said you'll have to get them from third-party vendors - distributing them like they do with notebook GPU drivers. I use drivers bundled with the Razer Core enclosure.

 module Micro
 import Data.String

Another implementation of λ_Π

An implementation of the dependently-typed language λ_Π in Idris - up to (but not including) a REPL, since Idris lacks quick support for parsing. You should be able to follow it if

you have read "A tutorial implementation of a dependently typed lambda calculus", and now understand how to use a dependently-typed language, if not implement it;

The CoqIDE bundle (8.5pl1, OS X) with ssreflect preinstalled.

coqide-8.5pl1-ssreflect.7z - around 75 MB. (Smaller than the standard CoqIDE bundle!)

A great big caveat: the app bundle is no longer codesigned. If you wish to keep CoqIDE*.app codesigned, install a clean CoqIDE*.app, and replace the Resource/bin and Resources/lib/coq/user-contrib with the ones here.

Sanity testing the installation

I’m sure the reference manual is out of date - instead, I use test cases from the mathcomp/ssrtest folder. Note the new, extended library import paths. Try this, for example:

Bookbinding, with a few gotchas covered

or: How I printed and bound a 600 page book in less than one day

Dylan McNamee

This guide is a result of following Dylan McNamee’s own: it adds in missing details (stack trimming included), and covers a few hiccups to avoid. What is here wouldn’t have been possible without his guide.

What’s covered, and what isn’t

	; Setup packaging...
	(require 'package)
	(add-to-list 'package-archives
	'("marmalade" .
	"http://marmalade-repo.org/packages/"))
	(add-to-list 'package-archives
	'("melpa" .
	"http://melpa.milkbox.net/packages/"))
	(package-initialize)

	By “world generation” we mean natural landscapes - not because we’re not interested in urban landscapes, but because we have a larger margin of error with the former. It’s not the “cities aren’t actually that interesting” effect - isn’t raw nature just as repeating? It’s the problem of simulating, in a way that isn’t trivial, all the possible ways humanity can both inhabit an environment, and shape it to its structures - determinism in both directions.

	A high-level view. We’ll use Dwarf Fortress, Minecraft, Sir, You are Being Hunted, and The Witcher 3 (that is, the REDengine 3) as our prototypical examples. Be familiar with the first two. (TW3 isn’t meaningfully procedural - but substantially procedural enough to work on, and high-detail.)

	We also refer to Morrowind as a source world we intend to model.

	We begin with concrete analyses, work out the design space, and then try to locate ourselves within it - although you can read it backwards if you want to see choices before justifications.

	A concrete exam

	#!/usr/bin/env stack
	-- stack runghc --package text --package turtle

	{-# LANGUAGE OverloadedStrings #-}

	{-
	lxx2md.hs (-l\|--lang LANG)
	A filter that converts Bird-style lhs in Markdown ``` blocks.
	Combines consecutive Bird-tracked lines into single blocks.

	> module Micro
	> import Data.String

	Another implementation of λ_Π
	=============================

	An implementation of the dependently-typed language λ_Π in Idris - up to (but not including) a REPL, since Idris lacks quick support for parsing. You should be able to follow it if
	- you have read "A tutorial implementation of a dependently typed lambda calculus", and now understand how to use a dependently-typed language, if not implement it;
	- you can write a Scheme metacircular interpreter;
	- understand how to write the usual suspects in an expressive type system like Idris';

	"use strict";

	/*
	tumblr-downloader.js - a Node.js script to download all media files posted in
	a Tumblr blog, most recent first.

	Usage:
	node tumblr-downloader.js

	Options - domain to download from, API key, and so on - are exposed below.

	<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
	"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
	<html xmlns="http://www.w3.org/1999/xhtml">
	<head>
	<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
	<style type="text/css">
	body { padding: 0px 0px;
	margin: 0px 0px;
	background-color: white }