Larry Diehl larrytheliquid

Various blog posts related to Nix and NixOS

General

https://nixos.org/wiki/Main_Page Nix wiki. Awesome resource containing huge amount of manuals and documentation with examples.
http://aflatter.de/nixos/ Alexander Flatter - NixOS. Installing NixOS inside a VirtualBox with a real-world configuration.nix example.
http://lethalman.blogspot.it/search/label/nixpills Luca Bruno - Nix Pills. Series of posts describing how to install nix into some environment and how to use it.
http://looprecur.com/blog/from-ubuntu-to-nixos/ Tim Sears - From Ubuntu to NixOS. Talk about experience migrating from Ubuntu to NixOS.

Git Submodules basic explanation

Why submodules?

In Git you can add a submodule to a repository. This is basically a repository embedded in your main repository. This can be very useful. A couple of usecases of submodules:

Separate big codebases into multiple repositories.

	// I'm tired of extensions that automatically:
	// - show welcome pages / walkthroughs
	// - show release notes
	// - send telemetry
	// - recommend things
	//
	// This disables all of that stuff.
	// If you have more config, leave a comment so I can add it!!

	{

	project=$(basename "$(pwd)")

	# build dependencies
	build_deps="stack build $project --fast --pedantic --dependencies-only --interleaved-output"

	# restart on changes in other packages
	restarts=$(find ../. -maxdepth 1 -type d \
	-not -name "$project" \
	-not -name .stack-work \
	-not -name . \

	-- Problem 3 of @Hillelogram's Great Theorem Prover Showdown.
	-- https://www.hillelwayne.com/post/theorem-prover-showdown
	--
	-- Implemented using current stable-2.5 branch of Agda
	-- (https://github.com/agda/agda/tree/08664ac) and the agda-prelude
	-- library (https://github.com/UlfNorell/agda-prelude/tree/d193a94).

	module Fulcrum where

	open import Prelude hiding (_≤?_)

	{-# OPTIONS --copatterns #-}
	module CoList where

	{- High-level intuition:

	codata CoList (A : Set) : Set where
	nil : CoList A
	cons : A → CoList A → CoList A

	append : ∀{A} → CoList A → CoList A → CoList A

	module Main

	%default total

	data Format
	= FInt -- %d
	\| FString -- %s
	\| FOther Char -- [a-zA-Z0-9]

	format : List Char -> List Format

	{-# LANGUAGE FlexibleContexts #-}
	module PickRandom where
	import Data.List (group, sort)
	import Control.Monad
	import Control.Monad.Random (MonadRandom, getRandomR)
	import qualified Control.Foldl as F

	-- Pick a value uniformly from a fold
	pickRandom :: MonadRandom m => a -> F.FoldM m a a
	pickRandom a = F.FoldM choose (return (a, 0 :: Int)) (return . fst)

	data FakeChar = A \| B \| C

	data ValidMyString : List Char -> Type where
	VA : ValidMyString xs -> ValidMyString ('a' :: xs)
	VB : ValidMyString xs -> ValidMyString ('b' :: xs)
	VC : ValidMyString xs -> ValidMyString ('c' :: xs)
	VNil : ValidMyString []

	implicit fromString : (x : String) -> {auto p : ValidMyString (unpack x)}
	-> List FakeChar

	module RuntimeTypes where

	open import Function
	open import Data.Unit
	open import Data.Bool
	open import Data.Integer
	open import Data.String as String
	open import Data.Maybe hiding (All)
	open import Data.List
	open import Data.List.All