bat

Stream: general

[Julian Berman]

If anyone else likes/uses bat (https://github.com/sharkdp/bat/ -- a cat replacement), it was pretty easy to add Lean syntax support to it. The file is here: https://gist.github.com/Julian/062e5ae6a6a5edfea23f8c89a7ff5d41 which was just converted from the vscode-lean file. Stick it in $(bat --config-dir)/syntaxes, run bat cache --build and yeah should work then. Trying to see if a PR to bat would succeed but will see if it meets their inclusion criteria.

[Kevin Buzzard]

What does it _do_? A clueless mathematician.

[Julian Berman]

cat is a program whose function is essentially "print the contents of a file" (technically I'm lying, its real purpose is "conCATenate" a bunch of files together, but everyone uses it essentially for the former). bat is cat but with modernities like "highlight the file you outputted". Basically you use either one when you want to view stuff and aren't sitting inside an editor already (or when say, you are piping outputs from some commands to each other, which seems a bit less likely in this case).

[Julian Berman]

This got merged, yay: https://github.com/sharkdp/bat/pull/1446