samdphillips

#lang racket/base

(require ffi/unsafe
         ffi/unsafe/custodian
         ffi/unsafe/define
         ffi/unsafe/schedule
         racket/struct)

(provide evdev-open
         evdev-read

wilbowma

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit.Base using (⊤; tt)
open import Agda.Primitive
open import Data.Product
open import Data.Fin
open import Data.Vec

shhyou

Comparing PDF files in git diff commands

The typical approach to comparing PDF files in git diff outputs amounts to converting PDF files into texts through pdftotext and show the diff of conversion.

1. Install the utility pdftotext from the project poppler
2. Enable the handler pdffiles in diff for PDF files and instruct the handler to call the pdf-astextplain script:

shhyou

#lang racket/base

(require racket/list
         racket/vector
         racket/bytes
         racket/match)

(provide
 ;; plain implementation of the Burrows-Wheeler transformation
 (struct-out bwencode)

sorawee

#lang racket/base

(provide hash hash*)

(require racket/match
         (only-in racket/base [hash racket:hash])
         (for-syntax racket/base
                     racket/list))

(define undef (gensym))

veekaybee

ChatGPT Resources

Context

ChatGPT appeared like an explosion on all my social media timelines in early December 2022. While I keep up with machine learning as an industry, I wasn't focused so much on this particular corner, and all the screenshots seemed like they came out of nowhere. What was this model? How did the chat prompting work? What was the context of OpenAI doing this work and collecting my prompts for training data?

I decided to do a quick investigation. Here's all the information I've found so far. I'm aggregating and synthesizing it as I go, so it's currently changing pretty frequently.

Model Architecture

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.

Metaxal

#lang racket/gui
(require plot
         pict)

;;; Author: Laurent Orseau
;;; License: [Apache License, Version 2.0](http://www.apache.org/licenses/LICENSE-2.0) or
;;;          [MIT license](http://opensource.org/licenses/MIT) at your option.

;;; See in particular this blog bost:
;;; https://alex-hhh.github.io/2019/09/map-snip.html#2019-09-08-map-snip-footnote-2-return

Gabriella439

{-# LANGUAGE ApplicativeDo               #-}
{-# LANGUAGE BlockArguments             #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances       #-}

module HasCal where

import Control.Applicative (Alternative(..), liftA2)

andrejbauer

open import Level
open import Relation.Binary
open import Data.Product
open import Data.Unit
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality renaming (refl to ≡-refl; trans to ≡-trans; sym to ≡-sym; cong to ≡-cong)
open import Relation.Binary.PropositionalEquality.Properties
open import Function.Equality hiding (setoid)

module Epimorphism where