Skip to content

Instantly share code, notes, and snippets.

View utensil's full-sized avatar

Utensil utensil

  • 18:27 (UTC +08:00)
View GitHub Profile
@fpvandoorn
fpvandoorn / MessyCode.lean
Last active October 9, 2023 17:45
Some experiments using type class graphs in Lean 4
import Mathlib
open Lean Meta Elab Command
-- generalized
/-- Write an import graph, represented as a an array of `NameMap`s to the ".dot" graph format.
If `("style1", graph1)` is in `graphs`, then the edges in `graph1` will be labeled with `[style1]`.
Example: `asStyledDotGraph #[("", graph1), ("style=dashed", graph2)]` -/
def asStyledDotGraph [ForIn Id α Name] (graphs : Array (String × NameMap α))
(header := "import_graph") : String := Id.run do
#!/bin/bash
#
# Container source: https://github.com/OpenAccess-AI-Collective/axolotl/blob/main/docker/Dockerfile-runpod
#
#
# To run this in RunPod with `winglian/axolotl-runpod:main-cu118-2.0.0`, set
# Expose HTTP Ports (Max 10): 7860,8888
# docker command: `bash -c "curl -H 'Cache-Control: no-cache' https://raw.githubusercontent.com/utensil/llm-playground/main/scripts/entry/prepare_ax.sh -sSf | bash"`
# JUPYTER_PASSWORD change to your secret
# HUGGINGFACE_TOKEN change to your token from https://huggingface.co/settings/tokens
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@munrocket
munrocket / wgsl_3d_sdf.md
Last active May 12, 2025 12:37
WGSL 3D SDF Primitives

WGSL 3D SDF Primitives

Revision: 06.08.2023, https://compute.toys/view/407

Sphere - exact

fn sdSphere(p: vec3f, r: f32) -> f32 {
  return length(p) - r;
}
@azu
azu / README.md
Created June 6, 2021 07:13
Decrypt and restore iOS backup(`Manifest.db` is encrypted) for restoring my iOS photos.

Setup

Use https://github.com/jfarley248/iTunes_Backup_Reader

git clone https://github.com/jfarley248/iTunes_Backup_Reader
cd iTunes_Backup_Reader
# apply https://github.com/jfarley248/iTunes_Backup_Reader/pull/12
gh pr checkout https://github.com/jfarley248/iTunes_Backup_Reader/pull/12
@davidteren
davidteren / nerd_fonts.md
Last active August 9, 2025 22:12
Install Nerd Fonts via Homebrew [updated & fixed]
@eric-wieser
eric-wieser / finsupp_prod_equiv.lean
Last active July 25, 2020 09:41
An alternative formulation of finsupp.finsupp_prod_equiv
import data.finsupp
namespace finsupp.eric
#check finset.sigma
universes u v w
def bind_prod {α : Type u} {β : Type v} (sa : finset α) (fb : α → finset β) : finset (α × β)
:= (sa.sigma fb).map (equiv.sigma_equiv_prod _ _).to_embedding
import data.dfinsupp
import tactic
universes u v w
variables {ii : Type u} {jj : Type v} [decidable_eq ii] [decidable_eq jj]
variables (β : ii → jj → Type w) [Π i j, decidable_eq (β i j)]
variables [Π i j, has_zero (β i j)]
def to_fun (x : Π₀ (ij : ii × jj), β ij.1 ij.2) : Π₀ i, Π₀ j, β i j :=
-- A One-Line Proof of the Infinitude of Primes
-- [The American Mathematical Monthly, Vol. 122, No. 5 (May 2015), p. 466]
-- https://twitter.com/pickover/status/1281229359349719043
import data.finset.basic -- for finset, finset.insert_erase
import data.nat.prime -- for nat.{prime,min_fac} and related lemmas
import data.real.basic -- for real.nontrivial, real.domain
import analysis.special_functions.trigonometric -- for real.sin and related identities
import algebra.big_operators -- for notation `∏`, finset.prod_*
import algebra.ring -- for domain.to_no_zero_divisors

Github to Discord Webhook Tutorial

In this tutorial I'll show you how to create a Github webhook that will post updates from your Github account to a channel in Discord. The steps are simple so follow along!

Create a Webhook in a Discord Channel

First you need to create a webhook in a text channel. We're assuming you have both Manage Channel and Manage Webhooks permissions!

  • Go in a channel properties (Alternatively, Server Settings, Webhooks works too)