lenary

precmd_functions=("_exit_status" ${precmd_functions[@]})
function _exit_status() {
  local last_exit_status=$?

  export last_exit=""
  if [ -z "${last_exit_status}" ]; then
    last_exit=""
  elif (( last_exit_status != 0 )); then
    local description

lenary

$ git clone github:lenary/guides.git
Cloning into guides...
remote: Counting objects: 255, done.
remote: Compressing objects: 100% (216/216), done.
remote: Total 255 (delta 111), reused 163 (delta 35)
Receiving objects: 100% (255/255), 1.49 MiB | 564 KiB/s, done.
Resolving deltas: 100% (111/111), done.

$ cd guides
$ git remote -v

lenary

# stolen from http://github.com/cschneid/irclogger/blob/master/lib/partials.rb
#   and made a lot more robust by me
# this implementation uses erb by default. if you want to use any other template mechanism
#   then replace `erb` on line 13 and line 17 with `haml` or whatever 
module Sinatra::Partials
  def partial(template, *args)
    template_array = template.to_s.split('/')
    template = template_array[0..-2].join('/') + "/_#{template_array[-1]}"
    options = args.last.is_a?(Hash) ? args.pop : {}
    options.merge!(:layout => false)

lenary

RISC-V Registers Cheatsheet

Numeric	ABI Name	Calling Convention	RVC?	RVE?
x0	zero	Immutable	No	Yes
x1	ra	Return Address	No	Yes
x2	sp	Callee-Saved	No*	Yes
x3	gp	Unallocatable	No	Yes
x4	tp	Unallocatable	No	Yes
x5-x7	t0-t2	Caller-Saved	No	Yes

lenary

          _Complex float	size:  8	align:  4	atomic-size:  8	atomic-align:  4
         _Complex double	size: 16	align:  8	atomic-size: 16	atomic-align:  8
 struct { char buf[0]; }	size:  0	align:  1	atomic-size:  1	atomic-align:  1
 struct { char buf[1]; }	size:  1	align:  1	atomic-size:  1	atomic-align:  1
 struct { char buf[2]; }	size:  2	align:  1	atomic-size:  2	atomic-align:  2
 struct { char buf[3]; }	size:  3	align:  1	atomic-size:  4	atomic-align:  4
 struct { char buf[4]; }	size:  4	align:  1	atomic-size:  4	atomic-align:  4
 struct { char buf[5]; }	size:  5	align:  1	atomic-size:  5	atomic-align:  1
 struct { char buf[6]; }	size:  6	align:  1	atomic-size:  6	atomic-align:  1
 struct { char buf[7]; }	size:  7	align:  1	atomic-size:  7	atomic-align:  1

lenary

You should read my dissertation here: http://lenary.co.uk/publications/dissertation/ it gives enough of an overview that you should see what is doable and what isn't. Of course the writing isn't super great, sorry about that.

Then, of course, realise that this is about 1/3 finished, but pretty much abandoned right now. Here are some jumping off points to taking it forwards:

Some ideas for jumping off points:

• look at the effects system in Idris, how this might work with the models of concurrency seen in erlang
• how do the different trade-offs that idris makes affect how good this will be at distribution. Concurrency is a slightly different problem, where I assumed a lack of failures (ie if one thing failed, it's fine for everything to fail).
• Better types for behaviours should be doable. I touched on this in my dissertation.
• There's a haskell library for generating core erlang. That could be a better backend than escripts.

lenary

Two formatters i made, just for fun, both heavily based of the specdoc format.

The dragon_formatter.rb just says "HERE BE DRAGONS" after pending tests, and tells you the count in the summary.

the boss_formatter.rb just adds "LIKE A BOSS!" after passing tests, and when it says how long it took.

lenary

Sooo, CRDTs.

They broadly fall into two groups, Commutative and Convergent.

• Commutative Replicated Data Types (aka CmRDTs): These are also referred to as op-based CRDTs. Essentially, updates cause commutative operations to be broadcast. However, this broadcast channel is required to be reliable and have an order (see §2.2.2 of [1] below).
• Convergent Replicated Data Types (aka CvRDTs): These are also referred to as state-based CRDTs. Essentially they consist of a data structure with a commutative merge operation which will deterministically take two of these structures and merge them into one, preserving updates. These don't require a reliable broadcast system, instead can rely on the liveness properties of an Eventually Consistent (EC) system normally.

Why is the reliable broadcast thing an issue? To have it you require strong consistency. CRDTs are supposed to be designed for Highly Available, EC systems, which by definition (and CAP theorem) can't have strong consistency[+].

lenary

#lang rosette

(require rosette/lib/synthax
         (only-in rosette/base/util/array reshape))

(provide generate-symbolic define-synthax-rule
         (all-from-out rosette/lib/synthax))

;; Fundamental. If you want bitvectors, use the bv explicit types
(current-bitwidth #f)

lenary

module UTLC

-- This is a terrible implementation of the Untyped Lambda Calculus,
-- using the semantics from Fig 5-3 in TAPL, amended using the changes
-- proposed in Chapter 6 of TAPL, associated with the deBruijn
-- indices.

-- This gives us the `Fin n` datatype, which is the numbers from 0 up
-- to (but not including) n. So, `Fin 0` has no inhabitants; `Fin 1`
-- has one inhabitant, namely 0; and `Fin 2` has two inhabitants,