stages:
- lint
# the build stage runs out-of-order w.r.t the lint stage as their is
# no dependence. the separation is purely conceptual
- build
# the contracts stage depends only on michocoq:8.11 in the build
# stage
- contracts
lint:
stage: lint
image: alpine
before_script:
- apk --no-cache add emacs-nox
- export scversion="latest"
- wget -qO- "https://github.com/koalaman/shellcheck/releases/download/latest/shellcheck-"${scversion}".linux.x86_64.tar.xz" | tar -xJv
script:
- shellcheck-"${scversion}"/shellcheck `find -name 'configure'`
- emacs --batch -l scripts/org-lint-README.el --kill
.build:
stage: build
# do not wait for lint
needs: []
before_script:
- echo -e "section_start:`date +%s`:setup_switch\r\e[0K setup opam switch"
- opam switch $COMPILER_EDGE; eval $(opam env)
- echo -e "section_end:`date +%s`:setup_switch\r\e[0K"
- echo -e "section_start:`date +%s`:setup_deps\r\e[0K setup the package dependencies"
- opam update -y
- sudo apt-get update -y -q
- sudo chown -R coq:coq "$CI_PROJECT_DIR"
- opam pin add -k git -y --no-action coq-mi-cho-coq .
- opam depext -y coq-mi-cho-coq
- echo -e "section_end:`date +%s`:setup_deps\r\e[0K"
script:
- echo -e "section_start:`date +%s`:project_build\r\e[0K build the project"
# Use inplace build to get reusable build results
- opam install -y --inplace-build -j ${NJOBS} --with-test coq-mi-cho-coq
- echo -e "section_end:`date +%s`:project_build\r\e[0K"
- which michocoq
michocoq:8.8:
image: coqorg/coq:8.8
extends: .build
michocoq:8.9:
image: coqorg/coq:8.9
extends: .build
michocoq:8.10:
image: coqorg/coq:8.10
extends: .build
michocoq:8.11:
image: coqorg/coq:8.11
extends: .build
# pass built michocoq framework to contracts:8.11 job as artifacts
# to speed up its build.
artifacts:
paths:
- src/michocoq/*.vo
- src/michocoq/micheline_parser.v
- src/michocoq/extraction/_build
contracts:8.11:
image: coqorg/coq:8.11
extends: .build
stage: contracts
# only wait for michocoq:8.11
needs:
- michocoq:8.11
script:
- echo -e "section_start:`date +%s`:project_build\r\e[0K build the project"
- opam install -y -j ${NJOBS} --deps-only coq-mi-cho-coq
- echo -e "section_end:`date +%s`:project_build\r\e[0K"
- echo -e "section_start:`date +%s`:check_contracts_coq\r\e[0K check contracts_coq"
- ./configure contracts_coq
- make
- echo -e "section_end:`date +%s`:check_contracts_coq\r\e[0K"