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

WIP Use bash script to build docker images #5

Open
wants to merge 22 commits into
base: main
Choose a base branch
from

Conversation

wucas
Copy link

@wucas wucas commented Mar 31, 2022

I've read the discussion around PR #3 and tried to incorporate all suggestions to come as close as possible to @fingolfin vision as described in Issue #1.

The prepare_gap.sh script does the downloading/cloning, compiling and downloading and compiling of the packages. It has three options -v, -t and -d. The first is to specify a version of GAP, the second to decide whether to download only required packages (argument: minimal) or all packages (argument: full) and the last is to choose whether to build GAP in debug mode or not (argument: 0 or 1).

The Dockerfile defines several build targets. base is the newest ubuntu with only packages installed that are necessary to download and compile GAP. all-deps then adds packages required to build all packages.
Then there are targets of the form "gap-{minimal,full}(-debug)" that then use the script prepare_gap.sh to build GAP accordingly. Note that we could also use another build argument to decide whether to build a debug version or not. But we cannot easily use a build argument to decide between minimal and full as these are based on different images (namely base or all-deps) and Dockerfiles are just not flexible enough to do that (afaik).

This PR does not implement correct github actions yet. And there's the question on how to name the various docker images in a consistent way. The dockerfile and script mainly work on my local machine atm some things likely have to be changed to make it work with ghcr.io.

Before I continue with this I'd love to hear feedback and suggestions!

@wucas wucas mentioned this pull request Mar 31, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant