ci(scripts/detect_errors.py): enforce silent builds (#4025)
Refactor of #3989.
This changes the GitHub Actions workflow so that the main build step and the test step run `lean` with `--json`. The JSON output is piped to `detect_errors.py` which now exits at the end of the build if there is any output and also writes a file `src/.noisy_files` with the names of the noisy Lean files. This file is now included in the olean caches uploaded to Azure.
The "try to find olean cache" step now uses `src/.noisy_files` to delete all of the `.olean` files corresponding to the noisy Lean files, thus making the results of CI idempotent (hopefully).
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
