#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]