Stop treating user-global directory as writeable; cache build artifacts

[joshlf]

• [anneal] Use Lean artifact cache; use local-filesystem git dep #3304
  • NOTE: This deletes the setup_repair test in preparation for future changes, leaving setup's repair logic untested
  • Update setup to initialize git repo in Aeneas Lean library
  • Update setup to lake build with LAKE_CACHE_DIR and LAKE_ARTIFACT_CACHE=1
  • Update generate/verify to generate a local-filesystem git dep on the Aeneas Lean library
  • Update generate/verify to set LAKE_CACHE_DIR when running lake build
• Investigate whether the prior work allows us to remove the worker pool/cache pool infra from integration tests
  • [anneal] Cleanup test infrastructure and implement atomic setup #3305
• Update setup to clone Mathlib into the toolchain directory and rewrite Aeneas's dep to be a local-filesystem git dep. Do this recursively for Mathlib's deps
  • [anneal] In setup, recursively cache Lean sources #3306
• Do as much of this as possible while building the .zst artifact
• Add extensive comments to explain all design decisions; refactor code so relevant tricky bits of logic all live together if necessary