Skip to content

Instantly share code, notes, and snippets.

Avatar

Sam Elliott lenary

View GitHub Profile
View riscv-registers.md

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
lenary / alignment-clang-ilp32.txt
Created Aug 16, 2019
Comparing GCC and Clang's Atomic Alignments for RISC-V ABIs (see diffs). Clang alignment generated after applying https://reviews.llvm.org/D57450
View alignment-clang-ilp32.txt
_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
View Idris-Erlang.md

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.
View common.rkt
#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
lenary / dlfind.c
Last active Oct 24, 2017
Simple Utility to find the path to a dynamic library on your system (by name)
View dlfind.c
#include <dlfcn.h>
#include <stdio.h>
#include <stdbool.h>
#include <string.h>
#ifdef __APPLE__
#include <mach-o/dyld.h>
#else // Linux
#include <link.h>
#endif
@lenary
lenary / test.hs
Last active Oct 10, 2017 — forked from elliotdavies/test.hs
Haskell pattern question
View test.hs
-- In `f` we want to keep piping (part of) the result of one function into
-- another, and stop as soon as something fails
f :: [A] -> Either String (B, [A])
f xs =
case f1 xs of
Left s -> Left s
Right (res1, xs') ->
case f2 xs' of
Left s -> Left s
Right (res2, xs'') ->
View listing-label.sty
%% Source Code Notes
\ProvidesPackage{listing-label}
% We use tikz for drawing the circles around the letters. Dumb, probably.
\RequirePackage{tikz}
% Counter, numbered by section
\newcounter{lstlistinglabel}[section]
% Length for left out-dent
\newlength{\lstlabelleftoutdent}
View test.c
#include <stdio.h>
// The file with the unchecked interface
#include <stdlib.h>
// The Redeclaration with the correct type
void *calloc(size_t nmemb, size_t size) : byte_count(nmemb * size);
#pragma BOUNDS_CHECKED ON
@lenary
lenary / exit-status.plugin.zsh
Last active Jan 8, 2019
Last command's exit status, for your prompt. Put ${last_exit} into your prompt somewhere. It uses zsh's prompt escapes.
View exit-status.plugin.zsh
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
View filter.agda
{-# OPTIONS --copatterns #-}
open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
trans : {A : Set} {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
trans refl refl = refl