Interacting with the asciicasts
The asciicasts embedded in the Agda section of LACI were created using an open-source tool called asciinema.
You don’t need to install anything to watch the asciicasts, though I did have to install the software to make the recordings. The recordings themselves are just sequences of JSON objects containing timing information and strings. There is no audio or video, which makes them really small. The playback uses a related piece of software, asciinema-player, which is JavaScript code that runs a terminal emulator in the browser.
You can just click to start the recording and watch from start to finish. But there are some useful keyboard shortcuts for interaction that are easier than trying to click little icons.
The space bar will toggle between play and pause modes.
The f key will toggle fullscreen mode.
The forward and backward arrow keys will rewind or fast-forward five seconds, respectively.
The numbers 0, 1, ... 9 will jump to the 0%, 10%, ...90% point in the recording.
The < and > keys will decrease or increase playback speed, respectively.
Finally, it is possible to copy and paste from the asciicast window into another application. I don’t know how useful this will be, but you have the option.