Revision 324e955cc8091466f16bd6d7b7897a49872cca79 authored by Danny Grove on 08 January 2020, 12:16:21 UTC, committed by Pierre Boutillier on 13 January 2020, 18:12:54 UTC
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.
1 parent 318c9f2
File | Mode | Size |
---|---|---|
.github | ||
.gitlab | ||
docs | ||
emacs | ||
scripts | ||
src | ||
tests_python | ||
vendors | ||
.dockerignore | -rw-r--r-- | 634 bytes |
.gitattributes | -rw-r--r-- | 132 bytes |
.gitignore | -rw-r--r-- | 837 bytes |
.gitlab-ci.yml | -rw-r--r-- | 29.4 KB |
.ocp-indent | -rw-r--r-- | 17 bytes |
Dockerfile | -rw-r--r-- | 2.1 KB |
LICENSE | -rw-r--r-- | 1.1 KB |
Makefile | -rw-r--r-- | 8.0 KB |
README.md | -rw-r--r-- | 1.8 KB |
active_protocol_versions | -rw-r--r-- | 32 bytes |
build.Dockerfile | -rw-r--r-- | 477 bytes |
contributing.md | -rw-r--r-- | 2.3 KB |
dune | -rw-r--r-- | 191 bytes |
dune-workspace | -rw-r--r-- | 16 bytes |
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...