Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: specific file names for cache get and cache get! #1430

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat: specific file names for cache get and cache get! #1430

wants to merge 12 commits into from

Conversation

arthurpaulino
Copy link
Collaborator

@arthurpaulino arthurpaulino commented Jan 8, 2023 •
edited

This PR allows arguments for cache get and cache get! as explained in the help menu:

'get' and 'get!' can process list of paths, allowing the user to be more
specific about what should be downloaded. For example, with automatic glob
expansion in shell, one can call:

$ lake exe cache get Mathlib/Algebra/Field/* Mathlib/Data/*

Which will download the cache for:
* Everything that starts with 'Mathlib/Algebra/Field/'
* Everything that starts with 'Mathlib/Data/'
* Everything that's needed for the above

@arthurpaulino arthurpaulino added the awaiting-review The author would like community review of the PR label Jan 8, 2023
YaelDillies
YaelDillies reviewed Jan 8, 2023
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you very much! This is a dream come true.

Cache/Main.lean Outdated Show resolved Hide resolved
eric-wieser
eric-wieser reviewed Jan 9, 2023
View reviewed changes
Cache/Main.lean Outdated Show resolved Hide resolved
eric-wieser
eric-wieser reviewed Jan 9, 2023
View reviewed changes
Cache/Main.lean Outdated Show resolved Hide resolved
eric-wieser
eric-wieser reviewed Jan 9, 2023
View reviewed changes
Cache/Hashing.lean Outdated Show resolved Hide resolved
gebner
gebner reviewed Jan 9, 2023
View reviewed changes
Cache/Hashing.lean Outdated Show resolved Hide resolved
eric-wieser
eric-wieser reviewed Jan 9, 2023
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What happens if I:

  • Request a file that doesn't exist locally
  • Request a file that has no available cache

Do I get any warning or error message?

@arthurpaulino
Copy link
Collaborator Author

arthurpaulino commented Jan 9, 2023 •
edited

No warning, but a warning could be added to the first case.

eric-wieser
eric-wieser reviewed Jan 10, 2023
View reviewed changes
Cache/Hashing.lean Outdated Show resolved Hide resolved
eric-wieser
eric-wieser reviewed Jan 10, 2023
View reviewed changes
Cache/Hashing.lean Outdated Show resolved Hide resolved
eric-wieser
eric-wieser reviewed Jan 10, 2023
View reviewed changes
Cache/Hashing.lean Outdated Show resolved Hide resolved
@eric-wieser
Copy link
Member

Probably the word "patterns" should be removed from the PR title and description too.

@arthurpaulino arthurpaulino changed the title feat: patterns for cache get and cache get! feat: specific file names for cache get and cache get! Jan 10, 2023
@gebner
Copy link
Member

gebner commented Jan 10, 2023

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jan 10, 2023
bors bot pushed a commit that referenced this pull request Jan 10, 2023
@arthurpaulino
feat: specific file names for cache get and cache get! (#1430)
1d47ea1 
This PR allows arguments for `cache get` and `cache get!` as explained in the help menu:

```text
'get' and 'get!' can process list of paths, allowing the user to be more
specific about what should be downloaded. For example, with automatic glob
expansion in shell, one can call:

$ lake exe cache get Mathlib/Algebra/Field/* Mathlib/Data/*

Which will download the cache for:
* Everything that starts with 'Mathlib/Algebra/Field/'
* Everything that starts with 'Mathlib/Data/'
* Everything that's needed for the above
```
@bors
Copy link

bors bot commented Jan 10, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: specific file names for cache get and cache get! [Merged by Bors] - feat: specific file names for cache get and cache get! Jan 10, 2023
@bors bors bot closed this Jan 10, 2023
@bors bors bot deleted the ap/cache-get-patterns branch January 10, 2023 18:56
@YaelDillies
Copy link
Collaborator

The description looks wrong. lake exe cache get Mathlib/Data/Set/* returns uncaught exception: No match for Mathlib/Data/Set/Accumulate.lean

@gebner gebner mentioned this pull request Jan 12, 2023
Closed
bors bot pushed a commit that referenced this pull request Jan 12, 2023
@gebner
fix: unpack all files in lake cache get (#1510)
84db453 
Redo of #1342.  This regression was introduced in #1430.
jcommelin pushed a commit that referenced this pull request Jan 23, 2023
@arthurpaulino @jcommelin
feat: specific file names for cache get and cache get! (#1430)
716eb4c 
This PR allows arguments for `cache get` and `cache get!` as explained in the help menu:

```text
'get' and 'get!' can process list of paths, allowing the user to be more
specific about what should be downloaded. For example, with automatic glob
expansion in shell, one can call:

$ lake exe cache get Mathlib/Algebra/Field/* Mathlib/Data/*

Which will download the cache for:
* Everything that starts with 'Mathlib/Algebra/Field/'
* Everything that starts with 'Mathlib/Data/'
* Everything that's needed for the above
```
jcommelin pushed a commit that referenced this pull request Jan 23, 2023
@gebner @jcommelin
fix: unpack all files in lake cache get (#1510)
9fb4df8 
Redo of #1342.  This regression was introduced in #1430.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@gebner gebner gebner left review comments

@digama0 digama0 digama0 left review comments

@YaelDillies YaelDillies YaelDillies left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@arthurpaulino @eric-wieser @gebner @YaelDillies @digama0