#✍️
- finish Notes on modern C++ programming

#benchmark #formal #rust #tui
- work on native-land
    - trying to make GA and math benchmark work, also evaluating the feasibility of benchmarking C++ libraries from Rust
    - pass CI on runpod
- work on formal-land, make Verso work
- debug various TUI tools

#formal #gpu #lean #neovim #rust
- work on native-land, trying to make rust-gpu fully work
- work on formal-land, trying to establish the infrastructure to explore multiple Lean 4 projects with independent toolchains and dependencies
- switching to Neovim, make it work for Rust, Lean, and forester
- write some useful key mappings in Neovim
- skim The Lean Language Reference
- start reading Modern C++ Programming Course (C++03/11/14/17/20/23/26)

#citation #haskell #physics #render #shader #vulkan #web #webgl
- initial citation trace for Gravitational lensing by spinning black holes in astrophysics, and in the movie interstellar[james2015gravitational] and Visualizing interstellar’s wormhole[james2015visualizing]
- Custom vulkan engine to render black holes in real time using ray-marching[meseguer2023custom] (Vulkan, Ray-marching, Kerr black hole) lrogerorrit/narwhalEngine
- Real-time high-quality rendering of non-rotating black holes[bruneton2020real] (CPU precal, WebGL2, Schwarzschild black hole) ebruneton/black_hole_shader
- skimmed Identifying black holes through space telescopes and deep learning[fang2024identifying]
- learn about Haskell-style type classes with isabelle/isar[haftmann2013haskell]: the type class for Isabelle, but its expressiveness is limited, see discussions in A construction of the lie algebra of a lie group in isabelle/HOL[schmoetten2024construction]

#benchmark #gpu #os
- Automatic differentiation: Inverse accumulation mode[siskind2019automatic] and A matrix-free exact newton method[naumann2024matrix], seems limited, but have some good references
- skim Gafro: Geometric algebra for robotics[low2023gafro] (good library and benchmark) and Developing GA-FuL: A generic wide-purpose library for computing with geometric algebra[eid2024developing] (good refs, but in C#)
- skim A comprehensive overview of GPU accelerated databases[sharma2024comprehensive], an interesting area with sparse tensors as an in-memory database in mind
- skim Felix: Optimizing tensor programs with gradient descent[zhao2024felix] (uiuc-arc/felix), which uses egg

#compiler
- found Functoriality in finitary vacuum einstein gravity and free yang-mills theories from an abstract differential geometric perspective[raptis2024functoriality]
- found A tensor algebra compiler for sparse differentiation[shaikhha2024tensor] and Felix: Optimizing tensor programs with gradient descent[zhao2024felix]
- SDQLite Optimizing tensor programs on flexible storage[schleich2023optimizing] (based on SDQL) is an intermediate language that expresses sparse tensor workloads by separating the tensoropt computations from the storage formats
- reminds me of A multi-level superoptimizer for tensor programs[wu2024multi]

#gpu
- work on native-land about GPU computation, see relavant README updates.

#bevy #game #idea #rust
- watch Chris Biscardi - Bevy: A case study in ergonomic Rust
- have a better idea about the game about fly, evade, slingshot, and shoot around black holes, 4D implicit surfaces
- explore sketchfab, polyhaven, and openverse, and have a basic idea about how to use them in the early stage of the game
- learn about itch.io to surveying existing games, and a open revenue sharing platform to release games
- found Algebraic geometry: A problem solving approach[garrity2013algebraic]

#lean #os
- C++ Package Managers: The Ultimate Roundup, and start using xrepo for C/C++ package management, it also supports a wide range of package repositories, including Conan, Conda, Vcpkg, Homebrew, Apt, and Cargo. But not BinaryBuilder.jl ecosystem (see also this FAQ).
- clarify the license for GinacLean, laying the ground for potential future work around Cadabra 2, which is licensed under GPLv3
- learn about Kento Okura's forest and Glade and Nota

#formal #gpu #lean #llvm #os #vulkan #web #z3
- add more plans in formal-land
- recovered Research Codebase Manifesto from Lean-MLIR
- recovered quotes from CICM 2020 Slack chat
- make CubeCL example work
- add CI with WebGPU on Mac & Ubuntu thanks to `llvmpipe`, `lavapipe`, `Vulkan SDK`, `Mesa` setup by tracel-ai/github-actions/setup-linux@v1
- found Lorenz and modular flows: a visual introduction

#news #os #rust
- learned about lobste.rs, a computing-focused community centered around link aggregation and discussion, a bit like Hacker News but less noise maybe
- Rewriting Rust and Josh Triplett's comment
- A multi-level superoptimizer for tensor programs[wu2024multi] and learn about mirage
- port My math interests in 2024
- make the Railscasts theme for Zed

#apl #os #tla #z3
- found ipe that is used extensively in tungsteno (source)
- Why I use TLA+ and not(TLA+), learn about PlusCal, Quint and Apalache (TLA+ to Z3)
- trying to figure out if TLA+ can be run in browser via TeaVM or CheerpJ

#os #render #web
- A simple approach to differentiable rendering of SDFs[wang2024simple]
- Rose: Composable autodiff for the interactive web[estep2024rose], and learn about Getting to the point: Index sets and parallelism-preserving autodiff for pointful array programming[paszke2021getting] dex-lang
- they are read on mobile app Reflow which has good PDF reflow support for math formulas in Arxiv papers, but not so good for other math book PDFs

#category #game #idea
- learn about catcolab.org and double category
- learn about Curved Diffusion: A Generative Model With Optical Geometry Control from ECCV 2024
- Reusing Styles from Tailwind CSS, decide to use it for CSS refactor
- found vanjs, considering for using it for VDOM and SSR
- learn about the game sgued/slingshot (just like a recent idea about black hole puzzle game inspired by Star Trek: Discovery)

#os #render #rust #sci #shader
- Differentiable Programming
    - found Differentiable Programming for Image Processing and Deep Learning in Halide and gradient-halide autodiff for halide
    - Adelta: Automatic Differentiation for Discontinuous Programs for A𝛿: Autodiff for Discontinuous Programs – Applied to Shaders Aδ: Autodiff for discontinuous programs-applied to shaders[yang2022delta]
    - found Dr.Jit
    - found Stan Math Library
    - found Kokkos
    - should eval the Rust crates of Rose
- found mistral.rs for LLM inference, which uses a HF candle fork internally
- found Why is anything conscious?[bennett2024anything]

#render #rust #shader
- found A simple approach to differentiable rendering of SDFs[wang2024simple] and Interval shading: Using mesh shaders to generate shading intervals for volume rendering[tricard2024interval]
- work on Rust stuff, particularly read about dioxus

#lean
- skim rubik-lean4 and be reminded of On the nxnxn rubik’s cube[bonzio2018nxnxn] and Nxnxn rubik’s cubes and god’s number[salkinder2021nxnxn]
- skim read-lean