• Daniel Grove's avatar
    Tooling, CI, Makefile: Dockerfiles and Make · 324e955c
    Daniel Grove authored
    The previous configuration of building with Docker used a lot of
    'magic' and required a fair bit of traversal between the shell scripts
    to understand what was happening and where. Most of it could be solved
    by using Docker Multi-staged Builds but to not constantly break the
    cache when just dealing with final artifacts I've split out the builder
    Dockerfile from the main Dockerfile. I've also broken out the commands
    run into individual make commands while trying to keep the original
    shell script API mostly intact.
    Running `./scripts/create_docker_image.sh` will work as it originally
    did just with the modifications necessary to align the script to also
    use the same underlying commands that are in make. I would have removed
    the script completely and adjusted the build pipelines, but the Makefile
    has an initial requirement of having `opam` installed which might not be
    the case for all users or the base build system.
    Othewise you can now just `make docker-image` but this will use the make
    bindings. It might be a good idea in the future to make your own Docker
    "building" image that can just use make within GitLabs CI system, but I
    think that was out of scope of this change.
Makefile 7.97 KB