Commit 2023-07-11 10:52 4dd7b55f

View on Github →

chore: move utilities into Util directory (#5787) As discussed during review of #5513, and on zulip

depends on: #5513

Estimated changes

Modified .github/workflows/bors.yml

Modified .github/workflows/build.yml

Modified .github/workflows/build.yml.in

Modified .github/workflows/build_fork.yml

Modified Mathlib/Tactic/LibrarySearch.lean

Modified Mathlib/Tactic/Rewrites.lean

Deleted MathlibExtras.lean

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

modified def Cache.Hashing.roots

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

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

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

Created Util/ImportGraph/Main.lean

added def asDotGraph

added def graph

added def importGraphCLI

added def main

Created Util/TacticCaches.lean

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

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

Modified lakefile.lean

Modified test/LibrarySearch/basic.lean

Modified test/rewrites.lean