AndrasKovacs

{-
At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:

    "A simple and efficient implementation of strong call by need by an abstract machine"
    https://dl.acm.org/doi/10.1145/3549822

This is right up my alley since I've implemented strong call-by-need evaluation
quite a few times (without ever doing more formal analysis of it) and I'm also
interested in performance improvements. Such evaluation is required in
conversion checking in dependently typed languages.

atennapel

{-# OPTIONS --type-in-type #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product

data Ty : Set where
  U : Ty
  Pi : (A : Set) -> (A -> Ty) -> Ty
  PiInd : Ty -> Ty

yunqu

First, add the ubuntu-toolchain-r/test PPA to your system with:

sudo apt install software-properties-common
sudo add-apt-repository ppa:ubuntu-toolchain-r/test

Install the desired GCC and G++ versions by typing:

sudo apt install gcc-7 g++-7 gcc-8 g++-8 gcc-9 g++-9

JARVIS-AI

sudo apt install gcc gcc-4.8 gcc-5 gcc-6 gcc-7 gcc-8 gcc-9
sudo apt install g++ g++-4.8 g++-5 g++-6 g++-7 g++-8 g++-9
sudo apt install build-essential
sudo apt install manpages-dev

sudo apt install software-properties-common
sudo add-apt-repository ppa:ubuntu-toolchain-r/test


sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-4.8 48 --slave /usr/bin/g++ g++ /usr/bin/g++-4.8 --slave /usr/bin/gcov gcov /usr/bin/gcov-4.8 --slave /usr/bin/gcc-ar gcc-ar /usr/bin/gcc-ar-4.8 --slave /usr/bin/gcc-nm gcc-nm /usr/bin/gcc-nm-4.8

AndrasKovacs

{-
Inductive-recursive universes, indexed by levels which are below an arbitrary type-theoretic ordinal number (see HoTT book 10.3). This includes all kinds of transfinite levels as well.

Checked with: Agda 2.6.1, stdlib 1.3

My original motivation was to give inductive-recursive (or equivalently: large inductive)
semantics to to Jon Sterling's cumulative algebraic TT paper:

cartazio

// #include <emmintrin.h>
#include <immintrin.h>
// #if defined (__SSE4_2__) || defined (__SSE4_1__)
// for some reason i can't get anything newer than sse4.2 work with both gcc-clang and clang
 // #include <smmintrin.h>
// #endif

#include <memory.h>

ChristopherKing42

{-# LANGUAGE Rank2Types, GADTs, LambdaCase #-}

data Stream a res where
    Head :: Stream a a
    Tail :: Stream a (CoData (Stream a))

newtype CoData con = CoD {unCoD :: forall r. con r -> r}

appendList :: [a] -> CoData (Stream a) -> CoData (Stream a)
appendList [] s = s

chrismdp

# You don't need Fog in Ruby or some other library to upload to S3 -- shell works perfectly fine
# This is how I upload my new Sol Trader builds (http://soltrader.net)
# Based on a modified script from here: http://tmont.com/blargh/2014/1/uploading-to-s3-in-bash

S3KEY="my aws key"
S3SECRET="my aws secret" # pass these in

function putS3
{
  path=$1

acowley

{-# LANGUAGE ScopedTypeVariables #-}
module Rendering.CLGLBuffer where
import Control.Parallel.CLUtil
import Foreign.Ptr (nullPtr)
import Foreign.Storable (Storable(sizeOf))
import Graphics.GLUtil.BufferObjects
import Graphics.Rendering.OpenGL (deleteObjectName, BufferObject, BufferTarget(..))
import Rendering.CLGLInterop

data CLGLBuffer a = CLGLBuffer { asVBO      :: BufferObject

cartazio

class (Ord (Key table)) => OrderedKV table where 
     type  Key table :: * 
     type Value table ::*
     type Address table :: * 

     keyRange :: table -> (Key table, Key table)
     key2Address :: table -> (Key table) -> Maybe (Address table)
     address2Key :: table -> (Address table) -> Key Table
     nextAddress :: table -> Address table -> Maybe (Address table)
     nextKey :: table -> Key table -> Maybe (Address table) ->Maybe (Key table, Address table  )