Continuous docker #4884
Closed
Continuous docker #4884
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
nmanthey
commented
Jul 8, 2019
nmanthey
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md. (added none)
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/ (only change to tooling)
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message). (no tests included)
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
This script allows to run commands inside a Docker container easily. The current directory, as well as the home directory are mounted inside the container, and the user id of the calling user is used, or, in case sudo is specified, the root user will be chosen. This way, file write operations inside the container can be visible to the outside, which allows to debug more easily, e.g. build failures.
The existing solution to build Xen did not allow to easily retrieve the build artifacts after the build, not files that allow to work on bug fixes in the tool chain. The new approach builds Xen inside the CBMC tree, so that all files are available afterwards. Note, CBMC is also build within the container, so that the relevant tools can be used inside the container as well.
We are interested in being able to compile the Linux kernel with goto-gcc. To not be required to have all tools available on a local machine, this change provides a docker setup that allows to build the Linux kernel natively, as well as with goto-gcc via the wrapper one-line-scan. Similarly to the Xen tooling, the build files, as well as logs and files for debugging are accessible after the run is complete.
nmanthey
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton,
tautschnig and
thk123
as code owners
|
The presented commits allow to compile Xen and the Linux kernel with goto-gcc, which, once fixed, could be useful to make sure changes to goto-gcc to not break these builds. Given these commits, adding more projects should be straight-forward. |
allredj
reviewed
Jul 8, 2019
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: a15047b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/118337550
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
Codecov Report
@@ Coverage Diff @@
## develop #4884 +/- ##
===========================================
- Coverage 69.09% 69.09% -0.01%
===========================================
Files 1298 1298
Lines 106944 106947 +3
===========================================
+ Hits 73895 73896 +1
- Misses 33049 33051 +2
Continue to review full report at Codecov.
|
peterschrammel
approved these changes
Nov 1, 2019
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.