-
Notifications
You must be signed in to change notification settings - Fork 56
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
Use private submodules before CI run #711
Conversation
041d24e
to
c965652
Compare
The CBMC CI will now replace some of the submodules in this repository with 'private' versions if the CI run was triggered by the private version of this repository.
c965652
to
1684a40
Compare
cbmc-ci/ci-config.yaml
Outdated
# If this is the private version of the repository, we need to pull in | ||
# the private versions of the submodules. | ||
- "echo Originating GitHub repository: ${GITHUB_REPOSITORY}" | ||
- cbmc-ci/switch-private-submodules --verbose env |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it's totally reasonable to move switch-private-submodule
to the root of the repo, since it's not CBMC-specific. We already have reformat.sh
there as well.
cbmc-ci/switch-private-submodules
Outdated
logging.info("Switching to %s version of the submodules", version) | ||
for module in MODULES: | ||
cmd = [ | ||
"git", "config", "--file=.gitmodules", |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So I see that this modifies the .gitmodule
file itself locally. That's not ideal if we're asking developers to run this themselves locally, since then they have a spurious edit they have to ignore.
How about this instead, since it only modifies .git/config
?
git config url."<private url>".insteadOf <public url>
https://git-scm.com/docs/git-config#Documentation/git-config.txt-urlltbasegtinsteadOf
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM.
#731) * Add CBMC CI configuration (#709) This commit adds a configuration file for the "CBMC Proofs" CI check. This is in preparation for adding some custom check-out steps later. * Use private submodules before CI run (#711) * chore: Use continuous-integration environment for private submodule access (#714) Co-authored-by: Robin Salkeld <salkeldr@amazon.com> * chore: Add support policy (#720) * Upgrade CBMC proof tools: starter kit and Litani 1.10.0 (#722) * Upgrade proof tool submodules This commit advances Litani to release 1.10.0, and the starter kit to the tip-of-tree. This brings the following improvements: - Profiling - Litani measures the memory usage of the CBMC safety checking and coverage checking jobs - The dashboard includes box-and-whisker diagrams for memory use per proof - The dashboard includes a graph of how many parallel jobs are running over the whole run, making it easy to choose a CI machine with enough parallelism - It is now possible to designate particular proofs as "EXPENSIVE"; Litani runs expensive proofs serially, ensuring that they do not over-consume resources like RAM. - UI improvements - Each pipeline page includes a table of contents - Each pipeline page includes a dependency graph of the pipeline - Each job on the pipeline page has a hyperlink to that job - The terminal output is now less noisy * Change cbmc-batch.yaml to cbmc-proof.txt This makes the proof layout consistent with the starter kit, which will allow us to use a generic run script in a future commit. Putting this in commit by itself because the diff is huge and not worth reading (just moving some files and changing two lines in the runscript). * Symlink run-cbmc-proofs.py to starter kit The run script is now a symbolic link into the starter kit submodule, meaning that it will be updated whenever the starter kit is. This is done iso that E-SDK doesn't carry custom modifications to the run script unless necessary; previous commits have made the E-SDK proofs consistent with the generic starter kit conventions. * fix: Simplify / update build instructions. (#713) Co-authored-by: June Blender <juneb@users.noreply.github.com> Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com> * fix(proof_timeout): mark high-memory proofs expensive (#710) * Removed OOM test, as OOM is no longer possible from aws allocators (#728) * chore: pin newer aws-sdk-cpp in macOS CI builds (#729) * chore: update version number and changelog for v1.9.1 * chore: update CBMC CI submodules Co-authored-by: Kareem Khazem <karkhaz@amazon.com> Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Ben Farley <47006790+farleyb-amazon@users.noreply.github.com> Co-authored-by: lizroth <30636882+lizroth@users.noreply.github.com> Co-authored-by: June Blender <juneb@users.noreply.github.com> Co-authored-by: Justin Boswell <boswej@amazon.com>
The CBMC CI will now replace some of the submodules in this repository
with 'private' versions if the CI run was triggered by the private
version of this repository.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.