Rocq N'Roll
summary
Rocq N’Roll parses Rocq proof tactics into MIDI in real time, using the VS Code LSP (proofView JSON RPC) to extract proof states and uses VSCode LSP proofView to expand automated steps; MIDI generation is implemented in Rust rather than OCaml and outputs a single MIDI channel with manual ADSR to any synth (OP‑1 or GarageBand). Automated tactics like auto can emit sequences or chords — auto can output 1–20 notes — semicolon produces simultaneous chords, and the system runs live, with an autoplay mode and modular code for extension.
AI-written summary · about
chapters (13)
- 0:00Welcome to Rocq N'Roll
- 0:44Motivation for proof music
- 1:48Proof sounds and dissonance
- 3:13Tactics into musical notes
- 4:58Rock tactics to MIDI sounds
- 6:46Music theory and auto tactic sounds
- 8:10Architecture and language server
- 11:21Language server trade-offs
- 12:02MIDI generation and synth
- 13:03Design space and GUI
- 14:09Open questions and future
- 14:49Closing and performance
- 15:13Q&A
related talks
41mIt's More Fun to Compute
37mRhythm 'n Rust: Building a Synthesizer from A to Z in Rust
43mProgramming Music with Overtone
49mArchaeopteryx: A Ruby MIDI Generator
13mMaking music with Ruby and Sonic Pi
55mCollaborative Live Coding With Glicol Music Programming Language
33mSounds, Synths, and Sonic Pi! Oh My!
25mDemo: Composable Compositions in Tonart