shhyou

Fix ACM Digital Library Loading Times in Firefox

Problem

The ACM Digital Library currently loads very slow in Firefox. This seems to stem from a lot of :has() selectors used in their CSS stylesheet.

Fix (uBlock Origin)

If you have uBlock Origin installed, you can add the following filter under the "My filters" tab:

shhyou

module ErrorReflectionDemo

import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils

%language ErrorReflection

data Col = BOOL | STRING | INT

shhyou

#!/usr/bin/env bash

set -euo pipefail

# just some sanity checks to make sure the arguments make sense
if ! test -f "${1}"; then
  echo "usage: ${0} <file>"
  exit 1
fi
file="${1}"

shhyou

{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}

{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

  https://github.com/ollef/sixty

The main idea is that during elaboration, we need different evaluation

shhyou

#lang racket/base

(require racket/include
         racket/stxparam
         (for-syntax racket/base syntax/parse/pre))

(provide
 quote
 #%datum
 (rename-out [include |#include|]

shhyou

AGDA_FILES=$(wildcard *.agda)
TEX_FILES=${AGDA_FILES:.agda=.tex}
PDF_FILES=${AGDA_FILES:.agda=.pdf}
MONO_FONT=DejaVu Sans Mono # FreeMono is another choice
PYGMENTS_STYLE=tango

GRADED_XOPP_FILES=$(wildcard *-graded.xopp)
GRADED_PDF_FILES=${GRADED_XOPP_FILES:.xopp=.pdf}

.PHONY: all

shhyou

This pull request adds a set of combinators for equational reasoning about vector equality of the form cast eq xs ≡ ys and a few properties demonstrating its application. In particular, the new combinators deal with the threading of index equality proofs, greatly reducing the boilerplate that manipulates casts to make writing equational proofs about vectors more or less feasible.

(Sorry for the piles of PR and the mess of the commit history. I promise this is the last one I have in hand. The first commit is the content of #2041 and #2045. After these two PRs get in, I'll rebase to remove the first commit. To see the code of this PR, please check https://github.com/agda/agda-stdlib/commit/f8971193dce2620cdabf4c7f1d8319c2aa8fb0ed.)

Motivation

Index arithmetic is notably troublesome when it comes to proving vector properties (#942). Existing solutions include stating and proving cast-equality by induction, proving [pointwise equality](https://github.com/agda/agda-stdlib/blob/104125c62d88ebe91274ebd

shhyou

{-# OPTIONS --without-K --safe #-}

module VecCastReason where

open import Data.Nat.Base
open import Data.Nat.Properties using (+-comm; +-suc; +-assoc)
open import Data.List.Base as List using (List; []; _∷_)
import Data.List.Properties as Listₚ
open import Data.Vec.Base
open import Data.Vec.Properties hiding (reverse-++; cast-reverse)

shhyou

#!/usr/bin/env racket
#lang racket/base

(require racket/file)

(provide cleanup-pref-keys)

(define cleanup-pref-keys
  '((plt:framework-pref:drracket:recently-closed-tabs ())
    (plt:framework-pref:drracket:console-previous-exprs ())

shhyou

#lang racket

(module DynCtc racket
  ;; the blames of dyn1/c and dyn2/c are different
  (provide dyn1/c
           dyn2/c
           (struct-out RuntimeError))
  (struct RuntimeError (message) #:transparent)

  (define dyn1/c