Commit 2023-07-12 04:07 806f7f97

View on Github →

chore: revert move utilities into Util directory (#5787) (#5825) This reverts commit 4dd7b55f0a06bd862d0c42066d159914327abf2f. Per zulip discussion.

Estimated changes

Modified .github/workflows/bors.yml

Modified .github/workflows/build.yml

Modified .github/workflows/build.yml.in

Modified .github/workflows/build_fork.yml

Renamed Util/Cache/Hashing.lean to Cache/Hashing.lean

modified def Cache.Hashing.roots

Renamed Util/Cache/IO.lean to Cache/IO.lean

Renamed Util/Cache/Main.lean to Cache/Main.lean

Renamed Util/Cache/Requests.lean to Cache/Requests.lean

Modified Mathlib/Tactic/LibrarySearch.lean

Modified Mathlib/Tactic/Rewrites.lean

Created MathlibExtras.lean

Renamed Util/TacticCaches/LibrarySearch.lean to MathlibExtras/LibrarySearch.lean

Renamed Util/TacticCaches/Rewrites.lean to MathlibExtras/Rewrites.lean

Deleted Util/ImportGraph/Main.lean

deleted def asDotGraph

deleted def graph

deleted def importGraphCLI

deleted def main

Deleted Util/TacticCaches.lean

Modified lakefile.lean

Modified test/LibrarySearch/basic.lean

Modified test/rewrites.lean