technical experiments [uts-0010]
technical experiments [uts-0010]
The following are technical experiments on what kind of rich content I can include in my forester notes. See my post on this for more background. Some of my technical notes (draft) might have additional information.
Lean 4 code highlighting [uts-0003]
Lean 4 code highlighting [uts-0003]
The following code is taken from pygments to test Lean 4 code highlighting, with only wrapped strings removed because it confuses forester.
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
-/
import Mathlib.Order.Chain
#align_import order.zorn from "leanprover-community/mathlib"@"46a64b5b4268c594af770c44d9e502afc6a515cb"
/-!
# Zorn's lemmas
This file proves several formulations of Zorn's Lemma.
## Variants
The primary statement of Zorn's lemma is `exists_maximal_of_chains_bounded`. Then it is specialized
to particular relations:
* `(≤)` with `zorn_partialOrder`
* `(⊆)` with `zorn_subset`
* `(⊇)` with `zorn_superset`
Lemma names carry modifiers:
* `₀`: Quantifies over a set, as opposed to over a type.
* `_nonempty`: Doesn't ask to prove that the empty chain is bounded and lets you give an element
that will be smaller than the maximal element found (the maximal element is no smaller than any
other element, but it can also be incomparable to some).
## How-to
This file comes across as confusing to those who haven't yet used it, so here is a detailed
walkthrough:
1. Know what relation on which type/set you're looking for. See Variants above. You can discharge
some conditions to Zorn's lemma directly using a `_nonempty` variant.
2. Write down the definition of your type/set, put a `suffices : ∃ m, ∀ a, m ≺ a → a ≺ m, { ... },`
(or whatever you actually need) followed by an `apply some_version_of_zorn`.
3. Fill in the details. This is where you start talking about chains.
A typical proof using Zorn could look like this (TODO: update to mathlib4)
```lean
lemma zorny_lemma : zorny_statement :=
begin
let s : Set α := {x | whatever x},
suffices : ∃ x ∈ s, ∀ y ∈ s, y ⊆ x → y = x, -- or with another operator
{ exact proof_post_zorn },
apply zorn_subset, -- or another variant
rintro c hcs hc,
obtain rfl | hcnemp := c.eq_empty_or_nonempty, -- you might need to disjunct on c empty or not
{ exact ⟨edge_case_construction,
proof_that_edge_case_construction_respects_whatever,
proof_that_edge_case_construction_contains_all_stuff_in_c⟩ },
exact ⟨construction,
proof_that_construction_respects_whatever,
proof_that_construction_contains_all_stuff_in_c⟩,
end
```
## Notes
Originally ported from Isabelle/HOL. The
[original file](https://isabelle.in.tum.de/dist/library/HOL/HOL/Zorn.html) was written by Jacques D.
Fleuriot, Tobias Nipkow, Christian Sternagel.
-/
open Classical Set
variable {α β : Type*} {r : α → α → Prop} {c : Set α}
/-- Local notation for the relation being considered. -/
local infixl:50 " ≺ " => r
/-- **Zorn's lemma**
If every chain has an upper bound, then there exists a maximal element. -/
theorem exists_maximal_of_chains_bounded (h : ∀ c, IsChain r c → ∃ ub, ∀ a ∈ c, a ≺ ub)
(trans : ∀ {a b c}, a ≺ b → b ≺ c → a ≺ c) : ∃ m, ∀ a, m ≺ a → a ≺ m :=
have : ∃ ub, ∀ a ∈ maxChain r, a ≺ ub := h _ <| maxChain_spec.left
let ⟨ub, (hub : ∀ a ∈ maxChain r, a ≺ ub)⟩ := this
⟨ub, fun a ha =>
have : IsChain r (insert a <| maxChain r) :=
maxChain_spec.1.insert fun b hb _ => Or.inr <| trans (hub b hb) ha
hub a <| by
rw [maxChain_spec.right this (subset_insert _ _)]
exact mem_insert _ _⟩
#align exists_maximal_of_chains_bounded exists_maximal_of_chains_bounded
/-- A variant of Zorn's lemma. If every nonempty chain of a nonempty type has an upper bound, then
there is a maximal element.
-/
theorem exists_maximal_of_nonempty_chains_bounded [Nonempty α]
(h : ∀ c, IsChain r c → c.Nonempty → ∃ ub, ∀ a ∈ c, a ≺ ub)
(trans : ∀ {a b c}, a ≺ b → b ≺ c → a ≺ c) : ∃ m, ∀ a, m ≺ a → a ≺ m :=
exists_maximal_of_chains_bounded
(fun c hc =>
(eq_empty_or_nonempty c).elim
(fun h => ⟨Classical.arbitrary α, fun x hx => (h ▸ hx : x ∈ (∅ : Set α)).elim⟩) (h c hc))
trans
#align exists_maximal_of_nonempty_chains_bounded exists_maximal_of_nonempty_chains_bounded
section Preorder
variable [Preorder α]
theorem zorn_preorder (h : ∀ c : Set α, IsChain (· ≤ ·) c → BddAbove c) :
∃ m : α, ∀ a, m ≤ a → a ≤ m :=
exists_maximal_of_chains_bounded h le_trans
#align zorn_preorder zorn_preorder
theorem zorn_nonempty_preorder [Nonempty α]
(h : ∀ c : Set α, IsChain (· ≤ ·) c → c.Nonempty → BddAbove c) : ∃ m : α, ∀ a, m ≤ a → a ≤ m :=
exists_maximal_of_nonempty_chains_bounded h le_trans
#align zorn_nonempty_preorder zorn_nonempty_preorder
theorem zorn_preorder₀ (s : Set α)
(ih : ∀ c ⊆ s, IsChain (· ≤ ·) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) :
∃ m ∈ s, ∀ z ∈ s, m ≤ z → z ≤ m :=
let ⟨⟨m, hms⟩, h⟩ :=
@zorn_preorder s _ fun c hc =>
let ⟨ub, hubs, hub⟩ :=
ih (Subtype.val '' c) (fun _ ⟨⟨_, hx⟩, _, h⟩ => h ▸ hx)
(by
rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq
refine' hc hpc hqc fun t => hpq (Subtype.ext_iff.1 t))
⟨⟨ub, hubs⟩, fun ⟨y, hy⟩ hc => hub _ ⟨_, hc, rfl⟩⟩
⟨m, hms, fun z hzs hmz => h ⟨z, hzs⟩ hmz⟩
#align zorn_preorder₀ zorn_preorder₀
theorem zorn_nonempty_preorder₀ (s : Set α)
(ih : ∀ c ⊆ s, IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) (x : α)
(hxs : x ∈ s) : ∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z ≤ m := by
-- Porting note: the first three lines replace the following two lines in mathlib3.
-- The mathlib3 `rcases` supports holes for proof obligations, this is not yet implemented in 4.
-- rcases zorn_preorder₀ ({ y ∈ s | x ≤ y }) fun c hcs hc => ?_ with ⟨m, ⟨hms, hxm⟩, hm⟩
-- · exact ⟨m, hms, hxm, fun z hzs hmz => hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩
have H := zorn_preorder₀ ({ y ∈ s | x ≤ y }) fun c hcs hc => ?_
· rcases H with ⟨m, ⟨hms, hxm⟩, hm⟩
exact ⟨m, hms, hxm, fun z hzs hmz => hm _ ⟨hzs, hxm.trans hmz⟩ hmz⟩
· rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
· exact ⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩
· rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩
exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩
#align zorn_nonempty_preorder₀ zorn_nonempty_preorder₀
theorem zorn_nonempty_Ici₀ (a : α)
(ih : ∀ c ⊆ Ici a, IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub)
(x : α) (hax : a ≤ x) : ∃ m, x ≤ m ∧ ∀ z, m ≤ z → z ≤ m := by
let ⟨m, _, hxm, hm⟩ := zorn_nonempty_preorder₀ (Ici a) (fun c hca hc y hy ↦ ?_) x hax
· exact ⟨m, hxm, fun z hmz => hm _ (hax.trans <| hxm.trans hmz) hmz⟩
· have ⟨ub, hub⟩ := ih c hca hc y hy; exact ⟨ub, (hca hy).trans (hub y hy), hub⟩
#align zorn_nonempty_Ici₀ zorn_nonempty_Ici₀
end Preorder
section PartialOrder
variable [PartialOrder α]
theorem zorn_partialOrder (h : ∀ c : Set α, IsChain (· ≤ ·) c → BddAbove c) :
∃ m : α, ∀ a, m ≤ a → a = m :=
let ⟨m, hm⟩ := zorn_preorder h
⟨m, fun a ha => le_antisymm (hm a ha) ha⟩
#align zorn_partial_order zorn_partialOrder
theorem zorn_nonempty_partialOrder [Nonempty α]
(h : ∀ c : Set α, IsChain (· ≤ ·) c → c.Nonempty → BddAbove c) : ∃ m : α, ∀ a, m ≤ a → a = m :=
let ⟨m, hm⟩ := zorn_nonempty_preorder h
⟨m, fun a ha => le_antisymm (hm a ha) ha⟩
#align zorn_nonempty_partial_order zorn_nonempty_partialOrder
theorem zorn_partialOrder₀ (s : Set α)
(ih : ∀ c ⊆ s, IsChain (· ≤ ·) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) :
∃ m ∈ s, ∀ z ∈ s, m ≤ z → z = m :=
let ⟨m, hms, hm⟩ := zorn_preorder₀ s ih
⟨m, hms, fun z hzs hmz => (hm z hzs hmz).antisymm hmz⟩
#align zorn_partial_order₀ zorn_partialOrder₀
theorem zorn_nonempty_partialOrder₀ (s : Set α)
(ih : ∀ c ⊆ s, IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) (x : α)
(hxs : x ∈ s) : ∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z = m :=
let ⟨m, hms, hxm, hm⟩ := zorn_nonempty_preorder₀ s ih x hxs
⟨m, hms, hxm, fun z hzs hmz => (hm z hzs hmz).antisymm hmz⟩
#align zorn_nonempty_partial_order₀ zorn_nonempty_partialOrder₀
end PartialOrder
theorem zorn_subset (S : Set (Set α))
(h : ∀ c ⊆ S, IsChain (· ⊆ ·) c → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub) :
∃ m ∈ S, ∀ a ∈ S, m ⊆ a → a = m :=
zorn_partialOrder₀ S h
#align zorn_subset zorn_subset
theorem zorn_subset_nonempty (S : Set (Set α))
(H : ∀ c ⊆ S, IsChain (· ⊆ ·) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub) (x)
(hx : x ∈ S) : ∃ m ∈ S, x ⊆ m ∧ ∀ a ∈ S, m ⊆ a → a = m :=
zorn_nonempty_partialOrder₀ _ (fun _ cS hc y yc => H _ cS hc ⟨y, yc⟩) _ hx
#align zorn_subset_nonempty zorn_subset_nonempty
theorem zorn_superset (S : Set (Set α))
(h : ∀ c ⊆ S, IsChain (· ⊆ ·) c → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s) :
∃ m ∈ S, ∀ a ∈ S, a ⊆ m → a = m :=
(@zorn_partialOrder₀ (Set α)ᵒᵈ _ S) fun c cS hc => h c cS hc.symm
#align zorn_superset zorn_superset
theorem zorn_superset_nonempty (S : Set (Set α))
(H : ∀ c ⊆ S, IsChain (· ⊆ ·) c → c.Nonempty → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s) (x)
(hx : x ∈ S) : ∃ m ∈ S, m ⊆ x ∧ ∀ a ∈ S, a ⊆ m → a = m :=
@zorn_nonempty_partialOrder₀ (Set α)ᵒᵈ _ S (fun _ cS hc y yc => H _ cS hc.symm ⟨y, yc⟩) _ hx
#align zorn_superset_nonempty zorn_superset_nonempty
/-- Every chain is contained in a maximal chain. This generalizes Hausdorff's maximality principle.
-/
theorem IsChain.exists_maxChain (hc : IsChain r c) : ∃ M, @IsMaxChain _ r M ∧ c ⊆ M := by
-- Porting note: the first three lines replace the following two lines in mathlib3.
-- The mathlib3 `obtain` supports holes for proof obligations, this is not yet implemented in 4.
-- obtain ⟨M, ⟨_, hM₀⟩, hM₁, hM₂⟩ :=
-- zorn_subset_nonempty { s | c ⊆ s ∧ IsChain r s } _ c ⟨Subset.rfl, hc⟩
have H := zorn_subset_nonempty { s | c ⊆ s ∧ IsChain r s } ?_ c ⟨Subset.rfl, hc⟩
· obtain ⟨M, ⟨_, hM₀⟩, hM₁, hM₂⟩ := H
exact ⟨M, ⟨hM₀, fun d hd hMd => (hM₂ _ ⟨hM₁.trans hMd, hd⟩ hMd).symm⟩, hM₁⟩
rintro cs hcs₀ hcs₁ ⟨s, hs⟩
refine'
⟨⋃₀cs, ⟨fun _ ha => Set.mem_sUnion_of_mem ((hcs₀ hs).left ha) hs, _⟩, fun _ =>
Set.subset_sUnion_of_mem⟩
rintro y ⟨sy, hsy, hysy⟩ z ⟨sz, hsz, hzsz⟩ hyz
obtain rfl | hsseq := eq_or_ne sy sz
· exact (hcs₀ hsy).right hysy hzsz hyz
cases' hcs₁ hsy hsz hsseq with h h
· exact (hcs₀ hsz).right (h hysy) hzsz hyz
· exact (hcs₀ hsy).right hysy (h hzsz) hyz
#align is_chain.exists_max_chain IsChain.exists_maxChain
-- other bits of tricky syntax
variable {ι A B : Type*} (𝒜 : ι → A) (ℬ : ι → B)
#check `𝒜.a
#check ``𝒜
#check List.get!
#check 1.0 + 2. + 0.3e1
#check "\
This is\na \
wrapped string."
@[to_additive "See note [foo]"]
lemma mul_one : sorry := sorry
Test TwistySim [uts-016I]
Test TwistySim [uts-016I]
For docs, see TwistySim.
TwistySim is the work of Conrad Rider, licensed under the Creative Commons Attribution-ShareAlike 4.0 International License (CC BY-SA 4.0).
Test Twizzle [uts-016H]
R U2' R2 U' R2 U' R2 U2' R
y'
M2' U M U2 M' U M2
Test Twizzle [uts-016H]
- API: cubing.js and full API reference - available options for TwistyPlayer: twisty-player-config - demo for TwistyAlgVier: twisty-alg-viewer demo for use of alg viewer, inspired by A supplement to "Commutators in the Rubik's Cube Group"
test 3D Bifurcation Diagram [uts-001C]
test 3D Bifurcation Diagram [uts-001C]
2025-06-06 UPDATE: Known to be broken for now. Errors: ``` Uncaught (in promise) JsValue(OperationError: Failed to execute 'requestDevice' on 'GPUAdapter': The limit "maxInterStageShaderComponents" with a non-undefined value is not recognized. OperationError: Failed to execute 'requestDevice' on 'GPUAdapter': The limit "maxInterStageShaderComponents" with a non-undefined value is not recognized. ```
Adapted from ⧉:
#storage atomic_storage array<atomic<i32>> const MaxSamples = 256.0; const FOV = 0.6; const PI = 3.14159265; const TWO_PI = 6.28318530718; const STEP = 0.01; const LARGENUM = 1e10; const ATOMIC_SCALE = 1024.0; struct Camera { pos: float3, cam: float3x3, fov: float, size: float2 } struct Ray { ro: float3, rd: float3, } var<private> camera : Camera; var<private> state : uint4; fn pcg4d(a: uint4) -> uint4 { var v = a * 1664525u + 1013904223u; v.x += v.y*v.w; v.y += v.z*v.x; v.z += v.x*v.y; v.w += v.y*v.z; v = v ^ ( v >> uint4(16u) ); v.x += v.y*v.w; v.y += v.z*v.x; v.z += v.x*v.y; v.w += v.y*v.z; return v; } fn rand4() -> float4 { state = pcg4d(state); return float4(state)/float(0xffffffffu); } fn nrand4(sigma: float, mean: float4) -> float4 { let Z = rand4(); return mean + sigma * sqrt(-2.0 * log(Z.xxyy)) * float4(cos(TWO_PI * Z.z),sin(TWO_PI * Z.z),cos(TWO_PI * Z.w),sin(TWO_PI * Z.w)); } fn udir(rng: float2) -> float3 { let r = float2(2.*PI*rng.x, acos(2.*rng.y - 1.0)); let c = cos(r); let s = sin(r); return float3(c.x*s.y, s.x*s.y, c.y); } fn disk(rng: float2) -> float2 { return float2(sin(TWO_PI*rng.x), cos(TWO_PI*rng.x))*sqrt(rng.y); } fn Rotate(t: float) -> float2x2 { return float2x2( cos(t), sin(t), - sin(t), cos(t), ); } fn RotXY(x: float3, t: float) -> float3 { return float3(Rotate(t)*x.xy, x.z); } fn GetCameraMatrix(ang: float2) -> float3x3 { let x_dir = float3(cos(ang.x)*sin(ang.y), cos(ang.y), sin(ang.x)*sin(ang.y)); let y_dir = normalize(cross(x_dir, float3(0.0,1.0,0.0))); let z_dir = normalize(cross(y_dir, x_dir)); return float3x3(-x_dir, y_dir, z_dir); } fn SetCamera() { let screen_size = int2(textureDimensions(screen)); let screen_size_f = float2(screen_size); let ang = float2(mouse.pos.xy)*float2(-TWO_PI, PI)/screen_size_f + float2(0.4, 0.4); camera.fov = FOV; camera.cam = GetCameraMatrix(ang); camera.pos = - (camera.cam*float3(8.0*custom.Radius+0.5,0.0,0.0)); camera.size = screen_size_f; } //project to clip space fn Project(cam: Camera, p: float3) -> float3 { let td = distance(cam.pos, p); let dir = (p - cam.pos)/td; let screen = dir*cam.cam; return float3(screen.yz*cam.size.y/(cam.fov*screen.x) + 0.5*cam.size,screen.x*td); } const max_iterations = 256; const color_thresholds = float4(255.0, 130.0, 80.0, 255.0); fn AdditiveBlend(color: float3, depth: float, index: int) { let scaledColor = int3(floor(ATOMIC_SCALE*color/(depth*depth + 0.2) + rand4().xyz)); if(scaledColor.x>0) { atomicAdd(&atomic_storage[index*4+0], scaledColor.x); } if(scaledColor.y>0) { atomicAdd(&atomic_storage[index*4+1], scaledColor.y); } if(scaledColor.z>0) { atomicAdd(&atomic_storage[index*4+2], scaledColor.z); } } fn RasterizePoint(pos: float3, color: float3) { let screen_size = int2(camera.size); let projectedPos = Project(camera, pos); let screenCoord = int2(projectedPos.xy+0.5*rand4().xy); //outside of our view if(screenCoord.x < 0 || screenCoord.x >= screen_size.x || screenCoord.y < 0 || screenCoord.y >= screen_size.y || projectedPos.z < 0.0) { return; } let idx = screenCoord.x + screen_size.x * screenCoord.y; AdditiveBlend(color, projectedPos.z, idx); } fn saturate(x: f32) -> f32 { return min(1.0, max(0.0, x)); } fn saturate_vec3(x: vec3<f32>) -> vec3<f32> { return min(vec3<f32>(1.0, 1.0, 1.0), max(vec3<f32>(0.0, 0.0, 0.0), x)); } fn bump3y(x: vec3<f32>, yoffset: vec3<f32>) -> vec3<f32> { var y: vec3<f32> = vec3<f32>(1.0, 1.0, 1.0) - x * x; y = saturate_vec3(y - yoffset); return y; } fn spectral_zucconi(w: f32) -> vec3<f32> { let x: f32 = saturate((w - 400.0) / 300.0); let cs: vec3<f32> = vec3<f32>(3.54541723, 2.86670055, 2.29421995); let xs: vec3<f32> = vec3<f32>(0.69548916, 0.49416934, 0.28269708); let ys: vec3<f32> = vec3<f32>(0.02320775, 0.15936245, 0.53520021); return bump3y(cs * (x - xs), ys); } fn hue(v: float) -> float3 { return .6 + .6 * cos(6.3 * v + float3(0.,23.,21.)); } fn bifurcation(iters: i32) { var p = rand4().xyz * float3(4.0, 4.0, 5.0) - float3(2.0, 2.0, -0.25); let s = rand4().x; let alpha = custom.Alpha; let beta = custom.Beta + custom.BetaAnim*(0.5 * sin(time.elapsed) + 0.5) + custom.BetaS*s; for (var j: i32 = 0; j <= iters; j = j + 1) { let p0 = p; p.x = p.z - p0.y*(beta * p0.x + (1.0 - beta) * p0.y); p.y = p0.x + p0.y * p0.y * alpha; if(j < iters - int(custom.Samples*MaxSamples + 1.0)) {continue;} var color = spectral_zucconi(350 + 350.0*s); color = pow(color, vec3(1.0)); RasterizePoint(float3(1,1,2.5)*(p - float3(0.5, 0.5, 1.5)), 32.0*color/(custom.Samples*MaxSamples + 1.0)); } } @compute @workgroup_size(16, 16) fn Clear(@builtin(global_invocation_id) id: uint3) { let screen_size = int2(textureDimensions(screen)); let idx0 = int(id.x) + int(screen_size.x * int(id.y)); atomicStore(&atomic_storage[idx0*4+0], 0); atomicStore(&atomic_storage[idx0*4+1], 0); atomicStore(&atomic_storage[idx0*4+2], 0); atomicStore(&atomic_storage[idx0*4+3], 0); } @compute @workgroup_size(16, 16) fn Rasterize(@builtin(global_invocation_id) id: uint3) { SetCamera(); //RNG state state = uint4(id.x, id.y, id.z, uint(custom.NoiseAnimation)*time.frame); bifurcation(int(MaxSamples*2.0)); } fn Sample(pos: int2) -> float3 { let screen_size = int2(textureDimensions(screen)); let idx = pos.x + screen_size.x * pos.y; var color: float3; let x = float(atomicLoad(&atomic_storage[idx*4+0])); let y = float(atomicLoad(&atomic_storage[idx*4+1])); let z = float(atomicLoad(&atomic_storage[idx*4+2])); color = float3(x,y,z)/ATOMIC_SCALE; return abs(color); } @compute @workgroup_size(16, 16) fn FinalPass(@builtin(global_invocation_id) id: uint3) { let screen_size = uint2(textureDimensions(screen)); // Prevent overdraw for workgroups on the edge of the viewport if (id.x >= screen_size.x || id.y >= screen_size.y) { return; } // Pixel coordinates (centre of pixel, origin at bottom left) let fragCoord = float2(float(id.x) + .5, float(id.y) + .5); let oldColor = textureLoad(pass_in, int2(id.xy), 0, 0); var color = float4(Sample(int2(id.xy)), 1.0); if(mouse.click != 1) { color += oldColor * custom.Accumulation; } let exposed = 1.0 - exp(-5.0*custom.Exposure*color.xyz/color.w); // Output to buffer textureStore(pass_out, int2(id.xy), 0, color); textureStore(screen, int2(id.xy), float4(exposed, 1.)); }
test GiNaC (WASM) [uts-001H]
test GiNaC (WASM) [uts-001H]
For now, open the console to see the output.
test Keenan Crane's style for rendering edge and shade [uts-001D]
test Keenan Crane's style for rendering edge and shade [uts-001D]
Adapted from ⧉:
#define EDGE_WIDTH 0.12 #define RAYMARCH_ITERATIONS 35 #define SHADOW_ITERATIONS 40 #define SHADOW_STEP 1.0 #define SHADOW_SMOOTHNESS 256.0 #define SHADOW_DARKNESS 0.75 // Distance functions from iquilezles.org float fSubtraction(float a, float b) {return max(-a,b);} float fIntersection(float d1, float d2) {return max(d1,d2);} void fUnion(inout float d1, float d2) {d1 = min(d1,d2);} float pSphere(vec3 p, float s) {return length(p)-s;} float pRoundBox(vec3 p, vec3 b, float r) {return length(max(abs(p)-b,0.0))-r;} float pTorus(vec3 p, vec2 t) {vec2 q = vec2(length(p.xz)-t.x,p.y); return length(q)-t.y;} float pTorus2(vec3 p, vec2 t) {vec2 q = vec2(length(p.xy)-t.x,p.z); return length(q)-t.y;} float pCapsule(vec3 p, vec3 a, vec3 b, float r) {vec3 pa = p - a, ba = b - a; float h = clamp( dot(pa,ba)/dot(ba,ba), 0.0, 1.0 ); return length( pa - ba*h ) - r;} float mySDF(vec3 p) { float x = p.x; float y = p.y; float z = p.z; float x2 = pow(x, 2.); float y2 = pow(y, 2.); float z2 = pow(z, 2.); float x3 = pow(x, 3.); float y3 = pow(y, 3.); float z3 = pow(z, 3.); float x4 = pow(x, 4.); float y4 = pow(y, 4.); float z4 = pow(z, 4.); // return (y-x2)*(z-x3); // return 5.*(z2+y3-y4-x2*y2); // return (y2-x2-z2); return (x2-z2*y2+y3); } float distf(vec3 p) { float d = 100000.0; fUnion(d, pRoundBox(vec3(0,0,10) + p, vec3(21,21,1), 1.0)); fUnion(d, pSphere(vec3(10,10,0) + p, 8.0)); fUnion(d, pSphere(vec3(16,0,4) + p, 4.0)); fUnion(d, pCapsule(p, vec3(10,10,12), vec3(15,15,-6.5), 1.5)); fUnion(d, pCapsule(p, vec3(10,10,12), vec3(5,15,-6.5), 1.5)); fUnion(d, pCapsule(p, vec3(10,10,12), vec3(10,5,-6.5), 1.5)); fUnion(d, pTorus(vec3(15,-15,0) + p, vec2(6,2))); fUnion(d, pTorus2(vec3(10,-15,0) + p, vec2(6,2))); fUnion(d, pRoundBox(vec3(-10,10,-2) + p, vec3(1,1,9), 1.0)); fUnion(d, pRoundBox(vec3(-10,10,-4) + p, vec3(0.5,6,0.5), 1.0)); fUnion(d, pRoundBox(vec3(-10,10,2) + p, vec3(6,0.5,0.5), 1.0)); // d = mySDF(p); // d = fIntersection(d, pSphere(p,15.0)); return d; } vec3 grad(vec3 p) { const float eps = 0.01; float m; vec3 d_distf = vec3( (distf(vec3(p.x-eps,p.y,p.z)) - distf(vec3(p.x+eps,p.y,p.z))), (distf(vec3(p.x,p.y-eps,p.z)) - distf(vec3(p.x,p.y+eps,p.z))), (distf(vec3(p.x,p.y,p.z-eps)) - distf(vec3(p.x,p.y,p.z+eps))) ); return d_distf / (2.*eps); } vec3 grad2(vec3 p) { const float eps = 0.01; float m; vec3 d_grad = vec3( (grad(vec3(p.x-eps,p.y,p.z)) - grad(vec3(p.x+eps,p.y,p.z))).x, (grad(vec3(p.x,p.y-eps,p.z)) - grad(vec3(p.x,p.y+eps,p.z))).y, (grad(vec3(p.x,p.y,p.z-eps)) - grad(vec3(p.x,p.y,p.z+eps)).z) ); return d_grad / (2.*eps); } vec3 normal(vec3 p) { return normalize(grad(p)); } vec4 raymarch(vec3 from, vec3 increment) { const float maxDist = 200.0; const float minDist = 0.001; const int maxIter = RAYMARCH_ITERATIONS; float dist = 0.0; float lastDistEval = 1e10; float edge = 0.0; for(int i = 0; i < maxIter; i++) { vec3 pos = (from + increment * dist); float distEval = distf(pos); if (lastDistEval < EDGE_WIDTH && distEval > lastDistEval + 0.001) { edge = 1.0; } if (distEval < minDist) { break; } dist += distEval; if (distEval < lastDistEval) lastDistEval = distEval; } float mat = 1.0; if (dist >= maxDist) mat = 0.0; return vec4(dist, mat, edge, 0); } float shadow(vec3 from, vec3 increment) { const float minDist = 1.0; float res = 1.0; float t = 1.0; for(int i = 0; i < SHADOW_ITERATIONS; i++) { float h = distf(from + increment * t); if(h < minDist) return 0.0; res = min(res, SHADOW_SMOOTHNESS * h / t); t += SHADOW_STEP; } return res; } float rand(float x) { return fract(sin(x) * 43758.5453); } float triangle(float x) { return abs(1.0 - mod(abs(x), 2.0)) * 2.0 - 1.0; } // Camera localized normal vec3 campos, camup; vec3 localNormal(vec3 p, vec3 rd) { vec3 n = normal(p), ln; vec3 side = cross(campos, camup); return vec3(dot(n, side), dot(n, camup), dot(n, -rd)); } float time; vec4 getPixel(vec2 p, vec3 from, vec3 increment, vec3 light) { vec4 c = raymarch(from, increment); vec3 hitPos = from + increment * c.x; vec3 normalDir = normal(hitPos); float diffuse = 1.0 + min(0.0, dot(normalDir, -light)); float inshadow = (1.0 - shadow(hitPos, -light)) * SHADOW_DARKNESS; // diffuse = max(diffuse, inshadow); // if it's not edge, and no contact if (c.z != 1.0 && c.y == 0.0) return vec4(0.96, 0.94, 0.87,1); float low = 0.05; float high = 0.95; diffuse = diffuse > high ? 1.0 : (diffuse > low ? low : diffuse); vec4 mCol = mix(vec4(vec3(0.78, 0.76, 0.78) * 1.15,1), vec4(0.70, 0.68, 0.75,1), diffuse); float gridStep = 1.0; // optional chess style grid // mCol = mix(mCol,vec4(0.,0.,0.,1.0),0.1*mod(floor(hitPos.x/gridStep)+floor(hitPos.y/gridStep)+floor(hitPos.z/gridStep),2.)); float dt = dot(vec3(0., 0., 1.), normalDir); float eps_high = 0.02; float eps_low = 0.00000; //1; // vec3 n = vec4(normalDir, 0.).xyz; vec3 n = localNormal(hitPos, increment); // grad(hitPos); // localNormal(hitPos, increment); vec3 ez = vec3(0.,0.,0.1); // https://www.shadertoy.com/view/fsGXzc const float MAX_DIST = 200.0; float depth = distance(from, hitPos); // /MAX_DIST; // I've mostly just copied and pasted Evan's code. //~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ // Compute curvature vec3 dx = dFdx(n); vec3 dy = dFdy(n); vec3 xneg = n - dx; vec3 xpos = n + dx; vec3 yneg = n - dy; vec3 ypos = n + dy; float curvature = (cross(xneg, xpos).y - cross(yneg, ypos).x) * 4.0 / (depth); // curvature debug // return vec4(vec3(1,0.9,0.8) * 0.7 * (abs(curvature) * 500.),1); ; vec4 curve_color = vec4(mix(vec3(1,0.9,0.8) * 0.5, vec3(1.), 0.5), 1.); // * length(grad(hitPos).xy) // * abs(curvature) * 200. float curvature_eps = 0.0001; if(c.z != 1. && abs(curvature) > curvature_eps && length(grad(hitPos).z) > eps_low && ( length(grad(hitPos).z) < eps_high * abs(curvature) * 100. ) ) { return curve_color; } if(c.z != 1. && abs(curvature) > curvature_eps && length(grad(hitPos).y) > eps_low && ( length(grad(hitPos).y) < eps_high * abs(curvature) * 100.) ) { return curve_color; } if(c.z != 1. && abs(curvature) > curvature_eps && length(grad(hitPos).x) > eps_low && ( length(grad(hitPos).x) < eps_high * abs(curvature) * 100.) ) { return curve_color; } if(c.z != 1. && length(grad(hitPos).z) > eps_low && ( length(grad(hitPos).z) < eps_high) ) { // return vec4(mix(vec3(1,0.9,0.8) * 0.5, vec3(1.), 0.5), 1.); // * (abs(curvature) * 1000.),1); } // .z is edge mCol = mix(mCol,vec4(vec3(1,0.9,0.8) * 0.5,1),c.z); return mCol; } void mainImage( out vec4 fragColor, in vec2 fragCoord ) { time = floor(iTime * 16.0) / 16.0; // pixel position vec2 q = fragCoord.xy / iResolution.xy; vec2 p = -1.0+2.0*q; p.x *= -iResolution.x/iResolution.y; // mouse vec2 mo = iMouse.xy/iResolution.xy; vec2 m = iMouse.xy / iResolution.xy; if (iMouse.x == 0.0 && iMouse.y == 0.0) { m = vec2(time * 0.06 + 1.67, 0.78); } m = -1.0 + 2.0 * m; m *= vec2(4.0,-0.75); m.y += 0.75; // camera position float dist = 65.0; vec3 ta = vec3(0,0,0); vec3 ro = vec3(cos(m.x) * cos(m.y) * dist, sin(m.x) * cos(m.y) * dist, sin(m.y) * dist); vec3 light = vec3(cos(m.x - 2.27) * 50.0, sin(m.x - 2.27) * 50.0, -20.0); // camera direction vec3 cw = normalize( ta-ro ); vec3 cp = vec3( 0.0, 0.0, 1.0 ); vec3 cu = normalize( cross(cw,cp) ); vec3 cv = normalize( cross(cu,cw) ); vec3 rd = normalize( p.x*cu + p.y*cv + 2.5*cw ); campos = -cw, camup = cv; // calculate color vec4 col = getPixel(p, ro, rd, normalize(light)); col = pow(col, vec4(1.0 / 2.2)); col = col * 1.8 - 0.8; fragColor = col; }
Color extracted with the help of ⧉.
See also: - toon shader - GLSL Fragment Shader: Sobel Edge Detection - Cross hatching WebGL shader - Penumbra Maps: Approximate Soft Shadows in Real-Time - stackgl/glsl-lighting-walkthrough
test Rhai scripting [uts-001P]
test Rhai scripting [uts-001P]
For now, open the console to see the output.
test Three.js and shaders [uts-0015]
test Three.js and shaders [uts-0015]
test compute shaders [uts-001E]
test compute shaders [uts-001E]
test d3-graphviz [uts-001Q]
test d3-graphviz [uts-001Q]
Same as test graphviz, but with d3-graphviz. There is no obvious difference as zooming and panning are disabled to avoid distraction.
Adapted from ⧉:
Adapted from ⧉:
Adapted from ⧉:
The same, but randomly choose a layout from one of 'circo', 'dot', 'fdp', 'sfdp', 'neato', 'osage', 'patchwork', 'twopi':
test egglog [uts-001I]
test egglog [uts-001I]
For now, open the console to see the output.
test graphviz [uts-001L]
test graphviz [uts-001L]
Adapted from ⧉:
Adapted from ⧉:
Adapted from ⧉:
The same, but randomly choose a layout from one of 'circo', 'dot', 'fdp', 'sfdp', 'neato', 'osage', 'patchwork', 'twopi':
test markdownit [uts-000M]
test markdownit [uts-000M]
We test hybrid markdown with forester markup:
We wish to use - external link: markdown-it demo - wiki link: test tikz drawing - citations: [nakahira2023diagrammatic] - cross-references: § [uts-000E]
The following tests a raw markdown-it renderer with no plugins, adapted from markdown-it demo:
# h1 Heading 8-) ## h2 Heading ### h3 Heading #### h4 Heading ##### h5 Heading ###### h6 Heading ## Horizontal Rules ___ --- *** ## Typographic replacements Enable typographer option to see result. (c) (C) (r) (R) (tm) (TM) (p) (P) +- test.. test... test..... test?..... test!.... !!!!!! ???? ,, -- --- "Smartypants, double quotes" and 'single quotes' ## Emphasis **This is bold text** __This is bold text__ *This is italic text* _This is italic text_ ~~Strikethrough~~ ## Blockquotes > Blockquotes can also be nested... >> ...by using additional greater-than signs right next to each other... > > > ...or with spaces between arrows. ## Lists Unordered + Create a list by starting a line with `+`, `-`, or `*` + Sub-lists are made by indenting 2 spaces: - Marker character change forces new list start: * Ac tristique libero volutpat at + Facilisis in pretium nisl aliquet - Nulla volutpat aliquam velit + Very easy! Ordered 1. Lorem ipsum dolor sit amet 2. Consectetur adipiscing elit 3. Integer molestie lorem at massa 1. You can use sequential numbers... 1. ...or keep all the numbers as `1.` Start numbering with offset: 57. foo 1. bar ## Code Inline `code` Indented code // Some comments line 1 of code line 2 of code line 3 of code Block code "fences" ``` Sample text here... ``` Syntax highlighting ``` js var foo = function (bar) { return bar++; }; console.log(foo(5)); ``` ## Tables | Option | Description | | ------ | ----------- | | data | path to data files to supply the data that will be passed into templates. | | engine | engine to be used for processing templates. Handlebars is the default. | | ext | extension to be used for dest files. | Right aligned columns | Option | Description | | ------:| -----------:| | data | path to data files to supply the data that will be passed into templates. | | engine | engine to be used for processing templates. Handlebars is the default. | | ext | extension to be used for dest files. | ## Links [link text](http://dev.nodeca.com) [link with title](http://nodeca.github.io/pica/demo/ "title text!") Autoconverted link https://github.com/nodeca/pica (enable linkify to see) ## Images   Like links, Images also have a footnote style syntax ![Alt text][id] With a reference later in the document defining the URL location: [id]: https://octodex.github.com/images/dojocat.jpg "The Dojocat" ## Plugins The killer feature of `markdown-it` is very effective support of [syntax plugins](https://www.npmjs.org/browse/keyword/markdown-it-plugin). ### [Emojies](https://github.com/markdown-it/markdown-it-emoji) > Classic markup: :wink: :cry: :laughing: :yum: > > Shortcuts (emoticons): :-) :-( 8-) ;) see [how to change output](https://github.com/markdown-it/markdown-it-emoji#change-output) with twemoji. ### [Subscript](https://github.com/markdown-it/markdown-it-sub) / [Superscript](https://github.com/markdown-it/markdown-it-sup) - 19^th^ - H~2~O ### [\<ins>](https://github.com/markdown-it/markdown-it-ins) ++Inserted text++ ### [\<mark>](https://github.com/markdown-it/markdown-it-mark) ==Marked text== ### [Footnotes](https://github.com/markdown-it/markdown-it-footnote) Footnote 1 link[^first]. Footnote 2 link[^second]. Inline footnote^[Text of inline footnote] definition. Duplicated footnote reference[^second]. [^first]: Footnote **can have markup** and multiple paragraphs. [^second]: Footnote text. ### [Definition lists](https://github.com/markdown-it/markdown-it-deflist) Term 1 : Definition 1 with lazy continuation. Term 2 with *inline markup* : Definition 2 { some code, part of Definition 2 } Third paragraph of definition 2. _Compact style:_ Term 1 ~ Definition 1 Term 2 ~ Definition 2a ~ Definition 2b ### [Abbreviations](https://github.com/markdown-it/markdown-it-abbr) This is HTML abbreviation example. It converts "HTML", but keep intact partial entries like "xxxHTMLyyy" and so on. *[HTML]: Hyper Text Markup Language ### [Custom containers](https://github.com/markdown-it/markdown-it-container) ::: warning *here be dragons* :::
test markmap [uts-016G]
test markmap [uts-016G]
The following example is adapted from markmap: Try it out.
test mermaid [uts-016F]
test mermaid [uts-016F]
We test hybrid markdown with forester markup and mermaid diagrams.
They should render to a mermaid diagram or fail gracefully as the mermaid source code.
The following examples are taken from various DeepWiki generated by AI or official Mermaid examples.
graph TD RaftNode["raftNode"] --> WAL["Write-Ahead Log (WAL)"] RaftNode --> MemoryStorage["raft.MemoryStorage"] MemoryStorage --> Snapshot["snap.Snapshotter"] WAL --> DiskStorage["Storage on Disk"] Snapshot --> DiskStorage subgraph "Log Compaction" Snapshot -->|"Creates"| SnapshotFile["Snapshot File"] SnapshotFile -->|"Allows truncation of"| WAL end
sequenceDiagram participant App as "Your Application" participant Config as "embed.Config" participant Etcd as "embed.Etcd" participant Server as "etcdserver.EtcdServer" App->>Config: NewConfig() Note over Config: Configure options App->>Config: Customize configuration App->>Etcd: StartEtcd(config) Etcd->>Config: Validate() Etcd->>Server: NewServer(serverConfig) Etcd->>Server: Start() Etcd-->>App: Return Etcd instance App->>Etcd: Server.ReadyNotify() Note over App,Etcd: Wait for server to be ready App->>Etcd: Use etcd server
classDiagram class Config { +Name string +Dir string +WalDir string +ListenPeerUrls []url.URL +ListenClientUrls []url.URL +AdvertisePeerUrls []url.URL +AdvertiseClientUrls []url.URL +ClientTLSInfo transport.TLSInfo +PeerTLSInfo transport.TLSInfo +ClusterState string +InitialCluster string +InitialClusterToken string +LogOutput[] string +LogLevel string +Logger *zap.Logger +AuthToken string +ServerFeatureGate featuregate.FeatureGate +...other fields } Config --> ServerConfig Config --> ClientConfig Config --> SecurityConfig class ServerConfig { +Name string +DataDir string +...other fields } class ClientConfig { +ConnectionType ClientConnType +CertAuthority bool +AutoTLS bool +...other fields } class SecurityConfig { +CertFile string +KeyFile string +TrustedCAFile string +...other fields }
stateDiagram-v2 [*] --> Still Still --> [*] Still --> Moving Moving --> Still Moving --> Crash Crash --> [*]
erDiagram CUSTOMER }|..|{ DELIVERY-ADDRESS : has CUSTOMER ||--o{ ORDER : places CUSTOMER ||--o{ INVOICE : "liable for" DELIVERY-ADDRESS ||--o{ ORDER : receives INVOICE ||--|{ ORDER : covers ORDER ||--|{ ORDER-ITEM : includes PRODUCT-CATEGORY ||--|{ PRODUCT : contains PRODUCT ||--o{ ORDER-ITEM : "ordered in"
%%{init: { 'logLevel': 'debug', 'timeline': {'disableMulticolor': true}}}%% timeline title History of Social Media Platform 2002 : LinkedIn 2004 : Facebook : Google 2005 : YouTube 2006 : Twitter
sankey-beta %% source,target,value Electricity grid,Over generation / exports,104.453 Electricity grid,Heating and cooling - homes,113.726 Electricity grid,H2 conversion,27.14
journey title My working day section Go to work Make tea: 5: Me Go upstairs: 3: Me Do work: 1: Me, Cat section Go home Go downstairs: 5: Me Sit down: 3: Me
gantt title A Gantt Diagram dateFormat MM-DD section sec 1 task1 : a1, 2014-01-01, 3d task2 : after a1, 2d section sec 2 task3 : 2014-01-02, 2d task4 : 4d
test penrose [uts-000Q]
test penrose [uts-000Q]
The following combines Penrose examples walk-on-spheres/laplace-estimator and curve-examples/blobs:
test pikchr [uts-000W]
test pikchr [uts-000W]
The following example is from ⧉:
The following is from my blog post Transformers: from self-attention to performance optimizations:
test syntax highlighting [uts-000Y]
test syntax highlighting [uts-000Y]
This is an additional test to Lean 4 code highlighting, which should load language highlighting syntax from CDN on demand to avoid a huge bundle of all languages.
test tikz drawing [uts-000E]
test tikz drawing [uts-000E]
This is a series of experiments with TikZ drawing to ensure my `diagrams.tex` has sufficient preambles to render them. Most of them are adapted to minimize dependencies, and fix wierd render issues.
test typst [uts-000R]
test typst [uts-000R]
Note: The Typst files and their imports must be placed under typst
, as it's set up as the root directory for Typst imports.
test uwal [uts-001J]
test uwal [uts-001J]
For now, open the console to see the output.