feat: live links for uses of example directive

[jcreedcmu]

Add some important pieces of the implementation of links to http://live.lean-lang.org/ without actually enabling it yet. This PR should be a no-op on the main content of the reference manual, although it has the side effect of producing an additional directory extracted-examples/ inside the output directory during HTML rendering of the reference manual.

This includes:

• Helper functions to traverse verso content finding code blocks that are not -keep or +error, suitably concatenating their contents and cleaning up whitespace.
• Filtering out :::examples that have no such blocks to display.
• LZ compression compatible with http://live.lean-lang.org/#codez= urls
• Extracting all examples to files in _out during document rendering so that we can run CI on them
• CSS for displaying the link when we want to.
• One incidental fix of a scope bug in documentation in Monads.lean

Progress towards leanprover/verso#569 .

[jcreedcmu]

A quick check of how many failing/succeeding examples there are right now shows 270 pass and 36 failing, via

find extracted-examples -name '*lean' | while read -r file; do
    output=$(lean "$file" 2>&1)
    status=$?
    if [ $status -ne 0 ]; then
        echo "Failed: $file (exit status: $status)"
    else
        echo "Succeeded: $file (exit status: $status)"
    fi
done

Hand inspection of the failures reveals that it's mostly about needing suitable imports (e.g. Lean or Std) and occasionally examples referring non-hermetically to previously-defined constants (for example, @robsimmons, your last #guard_msgs example in the Axioms section unfortunately does this) and occasionally #check_msgs, which is a reference-manual specific definition, is sometimes used inside :::example environments. I think maybe these last group can be dealt with simply by annotating them -keep?

[github-actions]

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 1a62df9.