cbiffle

Arch Linux is a rolling-release system that expects users to update regularly.

This can be a problem if you find yourself in possession of an older Arch Linux machine that hasn't been kept up to date. In particular, if you'd like to back up the contents of the system and reinstall, you may want certain tools available to do it (in my case it was pigz).

However, if they tools aren't already installed, you're out of luck: Arch's package repositories store only very recent versions of every package.

cbiffle

||| Church numerals using explicit lambdas, vs. equational style.  This is
||| a somewhat contrived example to demonstrate how proofs of function
||| equality can succeed for lambdas and fail for equational functions, even
||| though (to a casual observer) there isn't really a difference between the
||| two.
module ChurchLambda

-- Because I like the same names as the Prelude.  I admit I don't really
-- understand why names defined in this module don't just "win", but that's
-- not the point of this gist.  Keep scrolling.

cbiffle

module ProofWith

--------------------------------------------------------------------------------
-- Some lemmas used in the proofs below.  I've proposed these for inclusion in
-- the prelude, with cases like this in mind.
--
-- Together, these prove that we can predict the shape of the output of `decEq`
-- if we can either demonstrate propositional equality of its arguments, or
-- show that such equality is ridiculous.

cbiffle

||| Demonstration of length preservation during vector concatenation.
||| Derived from Guillaume Allais's Agda original.
|||
||| Ignore the fact that functions here are named "reverse" -- they are really
||| concatenation.
module ConcatVec

import Data.Vect

%default total

cbiffle

%default total

data KnownSet : Type where
  Control : KnownSet
  Data : KnownSet

dataNotControl : Not (Data = Control)
dataNotControl Refl impossible

data RState : Type where

cbiffle

-- This is a reduction of code that I wrote last night.
-- I can use this code to produce a `Void`.

-- Because I'm new to Idris I may have simply misinterpreted
-- what's going on here, so I've tried to specify my
-- understanding in comments.

%default total

data Color = Red | Blue

cbiffle

   Compiling warn v0.1.0 (file:///home/cbiffle/proj/rs/warn)
src/lib.rs:2:3: 2:31 warning: function is never used: `tested`, #[warn(dead_code)] on by default
src/lib.rs:2   pub fn tested() -> i32 { 0 }
               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
src/lib.rs:5:3: 5:33 warning: function is never used: `untested`, #[warn(dead_code)] on by default
src/lib.rs:5   pub fn untested() -> i32 { 0 }
               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
     Running target/debug/warn-fef74f9367799b2e

running 1 test

cbiffle

// A simple program to help me learn Rust.  This is a functional clone
// of cat circa 6th Edition Unix, before it grew all the options and
// stuff.

use std::env;
use std::io;
use std::fs::File;
use std::io::Write;
use std::io::BufRead;

cbiffle

#!/usr/bin/env coffee
#
# This simulates a common pattern for deriving encryption keys
# from passwords.  It's somewhat alarming how fast computers
# have become.  You may have to try round counts over 100k to
# get a useful measurement!
#
# To use:
#  coffee hash-benchmark.coffee <algo> <rounds>
#

cbiffle

crypto = require 'crypto'

hash = crypto.createHash('sha256')

x = hash.update
x("foo")