Skip to content

Instantly share code, notes, and snippets.

Sam Elliott lenary

Block or report user

Report or block lenary

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@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
View filter.agda
{-# OPTIONS --copatterns #-}
open import Agda.Builtin.Nat
data Vec (A : Set) : Nat -> Set where
[] : Vec A zero
_::_ : {n : Nat} A Vec A n Vec A (suc n)
record Stream (A : Set) : Set where
coinductive
You can’t perform that action at this time.