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.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"