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.

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

Allow loading of extraperfect files from all root dirs #5938

Conversation

lgoettgens
Copy link
Contributor

The former code for loading perf27.grp and perf33.grp tried to load them using READ_GAP_ROOT which only checks the root directories in SyGapRootPaths aka the root paths that are known at GAP's startup e.g. via the -l flag.
However, this won't check any root directories that were added later using ExtendRootDirectories.

This PR changes this to check all root directories in GAPInfo.RootPaths. The motivation for this is in OSCAR, where we want the julia lazy artifact handler to do the downloading of these files on first access, but due to how julia loads OSCAR and GAP.jl, this seems to be only possible using ExtendRootDirectories. (x-ref oscar-system/Oscar.jl#4592)

cc @fingolfin @ThomasBreuer

@fingolfin fingolfin added kind: enhancement Label for issues suggesting enhancements; and for pull requests implementing enhancements topic: library backport-to-4.14 labels Feb 21, 2025
@fingolfin
Copy link
Member

@ThomasBreuer any objections to merging this?

@ThomasBreuer
Copy link
Contributor

I think that this proposal is fine for the moment.

As soon as READ_GAP_ROOT, ReadGapRoot, ReadLib, ReadGrp have access to the full list of root directories, we could change the code again, in order to call ReadGrp in both places in question.

@ThomasBreuer ThomasBreuer merged commit 078f6c9 into gap-system:master Feb 23, 2025
33 checks passed
@fingolfin
Copy link
Member

Indeed, but that work will only be in GAP 4.15, while this patch can be backported for 4.14.1 :-)

@lgoettgens lgoettgens deleted the lg/extraperfect-ExtendRootDirectories branch February 24, 2025 10:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
backport-to-4.14 kind: enhancement Label for issues suggesting enhancements; and for pull requests implementing enhancements topic: library
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants