Skip to content
This repository has been archived by the owner on Aug 29, 2023. It is now read-only.

fix: various improvements to get-cache #113

Merged

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Aug 22, 2021

Apologies for the size of this PR; my impression was that the semantics of some of the commands were mixed up, and it was easier to change them all at once

Before this PR

  • leanproject mk-cache --force on a dirty tree:

    • Creates a cache entry for HEAD that represents the dirty state of the working tree (which is not HEAD!)
  • leanproject get-cache

    • on Mathlib:
      • Does a full history search
      • Unpacks the full archive over the working tree. If this archive comes from azure, it contains only oleans; if it comes from mk-cache it contains all the lean source files too.
    • on another project:
      • Uses only an exact match
      • Always overwrites local lean files, meaning that get-cache --rev old_revision acts much like git checkout old_revision -- .
  • leanproject get-mathlib-cache

    • on mathlib:
      • Behaved identically to leanproject get-cache
    • on another project:
      • Does a full history search
      • Checks out lean files by running git reset on mathlib

After this PR

  • leanproject mk-cache --force on a dirty tree:

    • is not supported. --force is now only for overwriting the cache if it exists
  • leanproject get-cache on any project:

    • Does a full history search
    • Unpacks only olean files
    • No longer supports --force. It only made sense in the presence of the destructive behavior regarding .lean files, which is no longer present.
  • leanproject get-mathlib-cache

    • No longer supports --rev
    • on mathlib:
      • Behaved identically to leanproject get-cache, spits out a warning telling the user to use get-cache directly.
    • on another project:
      • Does a full history search
      • Checks out mathlib lean files by running git reset on mathlib, then applying lean files from the tarball.

This replaces #96

@eric-wieser eric-wieser changed the title Use the new cache-searching logic in non-mathlib project too fix: various improvements to get-cache Aug 22, 2021
@eric-wieser eric-wieser removed the WIP label Aug 22, 2021
CHANGELOG.md Outdated Show resolved Hide resolved
CHANGELOG.md Outdated Show resolved Hide resolved
CHANGELOG.md Outdated Show resolved Hide resolved
@eric-wieser eric-wieser merged commit 93e6ae8 into leanprover-community:master Sep 17, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants