.gitlab-ci.yml

stages:
- prepare
- prove
- build
- test
- deploy

image: nixos/nix:2.3.12

variables:
  NIX_PATH: nixpkgs=channel:nixpkgs-unstable

  EXTRA_SUBSTITUTERS: https://jasmin.cachix.org
  EXTRA_PUBLIC_KEYS: jasmin.cachix.org-1:aA5r1ovq4HYKUa+8QHVvIP7K6Fi9L75b0SaN/sooWSY=
  NIXOS_PUBLIC_KEY: cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
  NIXPKGS_ALLOW_UNFREE: 1

  VERSION: development version at commit $CI_COMMIT_SHA on branch $CI_COMMIT_REF_NAME

.common:
  before_script:
  - nix-shell -p nix-info --run 'nix-info -m'
  - >-
    nix-shell
    --extra-substituters "$EXTRA_SUBSTITUTERS"
    --trusted-public-keys "$NIXOS_PUBLIC_KEY $EXTRA_PUBLIC_KEYS"
    --arg inCI true
    $EXTRA_NIX_ARGUMENTS
    --run 'echo done'
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'sed -i -e "s|@VERSION@|$VERSION|" compiler/src/glob_options.ml'

cache dependencies:
  stage: prepare
  extends: .common
  variables:
    EXTRA_NIX_ARGUMENTS: --arg coqDeps true --arg ocamlDeps true --arg testDeps true --arg ecDeps true --arg opamDeps true
  environment: cachix
  only:
    variables:
    - $CACHIX_SIGNING_KEY
  script:
  - >-
    nix-shell -p cachix --run
    'nix-store --query --references $(nix-instantiate --arg inCI true $EXTRA_NIX_ARGUMENTS default.nix)
    | xargs nix-store --realise
    | xargs nix-store --query --requisites
    | cachix push jasmin'

coq:
  stage: prove
  variables:
    EXTRA_NIX_ARGUMENTS: --arg coqDeps true
  extends: .common
  script:
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C proofs'
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C compiler CIL'
  artifacts:
    paths:
    - compiler/CIL/

ocaml:
  stage: build
  variables:
    EXTRA_NIX_ARGUMENTS: --arg ocamlDeps true
  extends: .common
  needs:
  - coq
  dependencies:
  - coq
  script:
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C compiler'
  artifacts:
    paths:
    - compiler/_build/
    - compiler/jasminc.native

eclib:
  stage: prove
  variables:
    EXTRA_NIX_ARGUMENTS: --arg ecDeps true
  extends: .common
  script:
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt why3config -why3 eclib/why3.conf'
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt     config -why3 eclib/why3.conf'
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make ECARGS="-why3 why3.conf" -C eclib'

opam:
  stage: prove
  variables:
    OPAMROOTISOK: 'true'
    OPAMROOT: mapo
    PREFIX: jasmin-$CI_COMMIT_REF_NAME-$CI_COMMIT_SHORT_SHA
    EXTRA_NIX_ARGUMENTS: --arg opamDeps true
  extends: .common
  cache:
    key:
      files:
        - scripts/nixpkgs.nix
      prefix: opam
    paths:
      - $OPAMROOT
  script:
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'scripts/opam-setup.sh ALL'
  - >-
    nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run
    'eval $(opam env) &&
     make -j$NIX_BUILD_CORES &&
     make install'
  artifacts:
    paths:
    - $PREFIX

opam-compiler:
  stage: build
  variables:
    OPAMROOTISOK: 'true'
    OPAMROOT: mapo
    EXTRA_NIX_ARGUMENTS: --arg opamDeps true
  extends: .common
  needs:
  - coq
  dependencies:
  - coq
  cache:
    key:
      files:
        - scripts/nixpkgs.nix
      prefix: opam
    paths:
      - $OPAMROOT
  script:
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'scripts/opam-setup.sh'
  - >-
    nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run
    'eval $(opam env) &&
     make -C compiler -j$NIX_BUILD_CORES &&
     (cd compiler && mkdir -p bin && cp _build/entry/jasminc.native bin/jasminc)'
  artifacts:
    paths:
    - compiler/bin/jasminc

tarball:
  stage: build
  variables:
    EXTRA_NIX_ARGUMENTS: --arg testDeps true
    TARBALL: jasmin-compiler-$CI_COMMIT_SHORT_SHA
  extends: .common
  needs:
  - coq
  dependencies:
  - coq
  script:
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler dist DISTDIR=$TARBALL'
  artifacts:
    paths:
    - compiler/$TARBALL.tgz

build-from-tarball:
  stage: test
  variables:
    TARBALL: jasmin-compiler-$CI_COMMIT_SHORT_SHA
  needs:
  - tarball
  dependencies:
  - tarball
  script:
  - tar xvf compiler/$TARBALL.tgz
  - nix build -o out -f $TARBALL
  - ./out/bin/jasminc -version

check:
  stage: test
  variables:
    EXTRA_NIX_ARGUMENTS: --arg testDeps true
  extends: .common
  needs:
  - coq
  - ocaml
  dependencies:
  - coq
  - ocaml
  script:
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './compiler/jasminc.native -version'
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C compiler check-ci'

libjade-compile-to-asm:
  stage: test
  variables:
    EXTRA_NIX_ARGUMENTS: --arg testDeps true
  extends: .common
  needs:
  - coq
  - ocaml
  dependencies:
  - coq
  - ocaml
  script:
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './scripts/test-libjade.sh src'
  artifacts:
    paths:
    - results/

libjade-extract-to-ec:
  stage: test
  variables:
    EXTRA_NIX_ARGUMENTS: --arg testDeps true --arg ecDeps true
    WHY3_CONF: $CI_PROJECT_DIR/why3.conf
    ECARGS: -why3 $WHY3_CONF -I Jasmin:$CI_PROJECT_DIR/eclib
    ECJOBS: '$(NIX_BUILD_CORES)'
  extends: .common
  needs:
  - coq
  - ocaml
  dependencies:
  - coq
  - ocaml
  script:
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt why3config -why3 $WHY3_CONF'
  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './scripts/test-libjade.sh proof'
  artifacts:
    paths:
    - results/

push-compiler-code:
  stage: deploy
  environment: deployment
  only:
    variables:
    - $DEPLOY_KEY
  variables:
    GIT_STRATEGY: none
    TARBALL: jasmin-compiler-$CI_COMMIT_SHORT_SHA
  needs:
  - tarball
  dependencies:
  - tarball
  before_script:
  - nix-env -iA nixpkgs.git
  - nix-env -iA nixpkgs.openssh
  - eval $(ssh-agent -s)
  - mkdir -p ~/.ssh
  - chmod 700 ~/.ssh
  - ssh-keyscan gitlab.com >> ~/.ssh/known_hosts
  - git config --global user.name "Jasmin Contributors"
  - git config --global user.email "nobody@noreply.example.com"
  script:
  - echo "$DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null
  - git clone git@gitlab.com:jasmin-lang/jasmin-compiler.git _deploy
  - cd _deploy
  - git checkout $CI_COMMIT_REF_NAME || git checkout --orphan $CI_COMMIT_REF_NAME
  - rm -rf compiler
  - tar xzvf ../compiler/$TARBALL.tgz
  - mv $TARBALL/ compiler
  - git add compiler
  - git commit -m "Jasmin compiler on branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA"  || true
  - git push --set-upstream origin $CI_COMMIT_REF_NAME