dramforever

This is a link to something, which is cleaner.

dramforever

Ltac detect :=
  match goal with
  | [ |- context G [ forall x : ?T, _ (* ?E *) ] ] =>
      idtac G T; fail
  end.

Theorem test : (forall x, x = 1) = (forall x, x = 2).
Proof.
  try detect.
  (* As shown above: _ matches inside binders expectedly

dramforever

This is a description of the mirroring script at tuna/tunasync-scripts#49 (and other related things)

Links:

• NixOS/nixpkgs#32659 (Asking about how to create a mirror)
• tuna/issues#323 (TUNA mirror request)
• tuna/tunasync-scripts#49 (PR with script to TUNA mirror)
• ustclug/mirrorrequest#165 (USTC mirror request)
• ustclug/ustcmirror-images#57 (PR with script to USTC mirror)
• http://www.shlug.org/discuss/2020/01/11/nixos_mirror.html (Discussion by @yuchangyuan, in Chinese)

dramforever

module Hs8b.Register where

import Clash.Prelude

type Reg = Unsigned 4
type Value = Unsigned 8

{-# ANN registerFileMono Synthesize
    { t_name = "register_file"
    , t_inputs = PortName <$> words "clk rst write read"

dramforever

class AccModule extends Module {
    val io = IO(new Bundle{
        val in = Input(UInt(32.W))
        val out = Output(UInt(32.W))
    })
    
    val reg = RegInit(0.U(32.W))
    reg := reg + io.in
    io.out := reg
}

dramforever

clash-prelude   > configure
clash-prelude   > Configuring clash-prelude-0.9999...
clash-prelude   > build
clash-prelude   > Preprocessing library for clash-prelude-0.9999..
clash-prelude   > Building library for clash-prelude-0.9999..
clash-prelude   > [ 1 of 88] Compiling Clash.Annotations.BitRepresentation
clash-prelude   > [ 2 of 88] Compiling Clash.Annotations.BitRepresentation.Internal
clash-prelude   > [ 3 of 88] Compiling Clash.Annotations.BitRepresentation.Util
clash-prelude   > [ 4 of 88] Compiling Clash.Annotations.Primitive
clash-prelude   > [ 5 of 88] Compiling Clash.Annotations.SynthesisAttributes

dramforever

From 622543203c56845f5ad3e0f358b242736b33001e Mon Sep 17 00:00:00 2001
From: dramforever <[email protected]>
Date: Fri, 24 May 2019 20:06:31 +0800
Subject: [PATCH] Fix scaling

---
 trunk/PKGBUILD       |  2 +-
 trunk/tdesktop.patch | 10 ----------
 2 files changed, 1 insertion(+), 11 deletions(-)

dramforever

dramforever

#include <iostream>
#include <memory>
#include <cmath>

struct Expr {
	double grad, value;
	void propagate(double delt) {
		grad += delt;
	}
	Expr(double value_): value(value_) {}

dramforever

# Based on https://gist.github.com/LnL7/570349866bb69467d0caf5cb175faa74

self: super:

{
  dramPackages = (super.dramPackages or {}) // self.recurseIntoAttrs {
    inherit (self)
      chromium
      # ... omitted
      ;