-
Notifications
You must be signed in to change notification settings - Fork 9
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
Add CircleCI template #28
Merged
Changes from 4 commits
Commits
Show all changes
5 commits
Select commit
Hold shift + click to select a range
b09ac39
Add CircleCI template
liyishuai 105fa3d
Apply suggestions from code review
liyishuai e5d66fd
circleci: use opam_name if defined
liyishuai f66162a
Apply suggestions from code review
liyishuai 6f78cd7
ci: disable --remote submodules; simplify PINS
liyishuai File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains 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
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,58 @@ | ||
version: 2.1 | ||
|
||
jobs: | ||
build: | ||
parameters: | ||
coq: | ||
type: string | ||
docker: | ||
- image: coqorg/coq:<<parameters.coq>> | ||
resource_class: medium | ||
environment: | ||
OPAMJOBS: 2 | ||
OPAMVERBOSE: 1 | ||
OPAMYES: true | ||
TERM: xterm | ||
steps: | ||
- checkout | ||
- run: | ||
name: Pull submodules | ||
command: git submodule update --init --remote | ||
- run: | ||
name: Configure environment | ||
command: echo . ~/.profile >> $BASH_ENV | ||
- run: | ||
name: Install dependencies | ||
command: | | ||
opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev | ||
opam update | ||
opam install --deps-only . | ||
- run: | ||
name: List installed packages | ||
command: opam list | ||
- run: | ||
name: Build, test, and install package | ||
command: opam install -t . | ||
{{# ci_test_dependants }} | ||
liyishuai marked this conversation as resolved.
Show resolved
Hide resolved
|
||
- run: | ||
name: Test dependants | ||
command: | | ||
PINS=($(opam list -s --pinned --columns=package)); PINS=$(IFS=, ; echo "${PINS[*]}") | ||
PACKAGES=`opam list -s --depends-on {{ opam_name }}{{^ opam_name }}coq-{{ shortname }}{{/ opam_name }} --coinstallable-with $PINS` | ||
if [ -n "$PACKAGES" ] | ||
then opam install -t $PACKAGES | ||
fi | ||
{{/ ci_test_dependants }} | ||
- run: | ||
name: Uninstall package | ||
command: opam uninstall . | ||
|
||
workflows: | ||
version: 2 | ||
test: | ||
jobs: | ||
{{# tested_coq_opam_versions }} | ||
- build: | ||
name: "Coq {{ version }}" | ||
coq: "{{ version }}" | ||
{{/ tested_coq_opam_versions }} |
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -22,6 +22,8 @@ jobs: | |
fail-fast: false | ||
steps: | ||
- uses: actions/checkout@v2 | ||
- name: Checkout submodules | ||
uses: textbook/[email protected] | ||
- uses: coq-community/docker-coq-action@v1 | ||
with: | ||
opam_file: '{{ opam_name }}{{^ opam_name }}coq-{{ shortname }}{{/ opam_name }}.opam' | ||
|
This file contains 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
This file contains 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
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.
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.
Is this yet another subtle difference between this template and the other CI templates?
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 so… Maybe adding this
git submodule
part is unneeded for the default coq-community templates? at least for the time being (IMHO the three CI templates should be as close as possible semantically one from the other, and later on other PRs could just as well add features that enhance them, in a row?)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.
Travis CI clones Git submodules by default. I've added submodule for GitHub Actions.
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.
OK! have you checked that this is exactly that command triggered by Travis for git submodule cloning?
(I'm not very submodule-savvy, but e.g. this blog https://mgalgs.github.io/2014/07/03/git-submodule-update-init-remote-recursive-considered-harmful.html mentions the following commands:
git submodule update --init --recursive; git submodule update --remote
)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.
Travis uses
git submodule update --init --recursive
. Should I just drop--remote
?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.
Maybe yes − this option is documented here:
https://git-scm.com/docs/git-submodule#Documentation/git-submodule.txt---remote ;
it appears to be related to remote-tracking branches (which would be a bit off-topic in the context of CI builds?)
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.
and this complies with the doc of GitLab CI as well:
https://docs.gitlab.com/ee/ci/git_submodules.html#using-git-submodules-in-your-ci-jobs
so
git submodule update --init --recursive
seems the way to goThere 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.
(actually the GItLab CI page I mentioned suggests two lines)