Commit 324e955c authored by Committed by Pierre Boutillier
Tooling, CI, Makefile: Dockerfiles and Make
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.
Showing with 158 additions and 93 deletions