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

feat(Cache): Allow arguments of the form Mathlib.Data which correspond to a folder but not a file #21838

Open
wants to merge 72 commits into
base: master
Choose a base branch
from
Open

feat(Cache): Allow arguments of the form Mathlib.Data which correspond to a folder but not a file #21838

wants to merge 72 commits into from

Conversation

joneugster
Copy link
Collaborator

joneugster and others added 30 commits February 13, 2025 09:32
@joneugster
refactor getFileImports
1c27341
@joneugster
add filter to recover previous behaviour
c76a5d8
@joneugster
refactor getPackageDir
bcbc142
@joneugster
typos
e1ade0c
@joneugster
remove #check
6ed64fd
@joneugster
update docstring
6d0be59
@joneugster
Merge branch 'eugster/cache_FileImports' into eugster/cache_remove_ha…
74d0f2e 
…rdcoded_package_dirs
@joneugster
Merge branch 'eugster/cache_getPackageDir' into eugster/cache_remove_…
f91af0b 
…hardcoded_package_dirs
@joneugster
remove unused packageDirs
c38e3d7
@joneugster
fix docstring
df22a52
@joneugster
remove TODO
34922d0
@joneugster
remove more unused stuff
35a7294
@joneugster
support module names as arguments
a72f445
@joneugster
update docstring
28927c2
@joneugster
comment
c08b2fa
@joneugster
Merge branch 'master' into eugster/cache_getPackageDir
1edb8be
@joneugster
Merge remote-tracking branch 'origin/master' into eugster/cache_getPa…
4c054a6 
…ckageDir
@joneugster @eric-wieser
Update Cache/IO.lean
3a7e2d2 
Co-authored-by: Eric Wieser <[email protected]>
@joneugster
Merge remote-tracking branch 'origin/master' into eugster/cache_remov…
ffbb9b7 
…e_hardcoded_package_dirs
@joneugster
style
73383e0
@joneugster
improve error message
50f3d78
@joneugster
Merge branch 'eugster/cache_FileImports' into eugster/cache_remove_ha…
bde9913 
…rdcoded_package_dirs
@joneugster
Merge branch 'eugster/cache_getPackageDir' into eugster/cache_remove_…
697115b 
…hardcoded_package_dirs
@joneugster
Merge branch 'eugster/cache_remove_hardcoded_package_dirs' into eugst…
f765fad 
…er/cache_parse_args
@joneugster
use module name instead of FilePath
ec2da0a
@joneugster
style
639659e
@joneugster
better path reconstruction
eeca105
@joneugster
rename function
5ffc77a
@joneugster
variable name
85265fe
@joneugster
fix
969ba17
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 13, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 14, 2025
joneugster and others added 17 commits February 14, 2025 14:38
@joneugster
code review
0748957
@joneugster
Merge branch 'eugster/cache_FileImports' into eugster/cache_remove_ha…
1acf0ee 
…rdcoded_package_dirs
@joneugster
Merge branch 'eugster/cache_remove_hardcoded_package_dirs' into eugst…
21225a2 
…er/cache_parse_args
@joneugster
Merge branch 'eugster/cache_parse_args' into eugster/cache_use_mod_in…
453d136 
…stead_of_path
@joneugster
Merge branch 'eugster/cache_use_mod_instead_of_path' into eugster/cac…
5cea360 
…he_pseudo_module_args
@joneugster
update comment
55785d6
@eric-wieser
Update Hashing.lean
542beb8
@eric-wieser
Docstrings shouldn't be just a TODO
a59d21b
@joneugster @eric-wieser
Update Cache/Hashing.lean
3c3b196 
Co-authored-by: Eric Wieser <[email protected]>
@joneugster
Merge remote-tracking branch 'origin/master' into eugster/cache_FileI…
0a151c0 
…mports
@joneugster
Merge branch 'eugster/cache_remove_hardcoded_package_dirs' into eugst…
ee75e18 
…er/cache_FileImports
@joneugster
Merge branch 'eugster/cache_FileImports' into eugster/cache_parse_args
a7ef9b6
@joneugster
fix merge
d3dff36
@joneugster
Merge remote-tracking branch 'origin/master' into eugster/cache_use_m…
89b1519 
…od_instead_of_path
@joneugster
Merge branch 'eugster/cache_parse_args' into eugster/cache_use_mod_in…
3160a74 
…stead_of_path
@joneugster
Merge branch 'eugster/cache_use_mod_instead_of_path' into eugster/cac…
19d9def 
…he_pseudo_module_args
@joneugster
fix merge
b04d375
@joneugster joneugster changed the base branch from eugster/cache_use_mod_instead_of_path to master February 24, 2025 16:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) CI Modifies the continuous integration / deployment setup t-meta Tactics, attributes or user commands
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@joneugster @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant @eric-wieser