POET/.gitlab-ci.yml at main · PROSA-Project/POET · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
###################### Global Config ######################

workflow:
  rules:
    - if: '$CI_PIPELINE_SOURCE == "merge_request_event"'
    - if: "$CI_COMMIT_BRANCH && $CI_OPEN_MERGE_REQUESTS"
      when: never
    - if: "$CI_COMMIT_BRANCH"

stages:
  - test

.preferred-stable-version:
  image: bbbrandenburg/prosa:0.6-mathcomp-2.4.0-rocq-9.0.0

.preferred-dev-version:
  image: bbbrandenburg/mathcomp-for-prosa:2.5.0-rocq-prover-9.0.0-rocq-core-9.1.0

###################### Rules and Scripts ##################

.not_in_wip_branches:
  rules:
    - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")

.only_in_wip_branches:
  rules:
    - if: ($CI_COMMIT_BRANCH =~ /^wip-.*$/) && ($CI_PIPELINE_SOURCE != "merge_request_event")

########################## Setup ##########################

.install-Prosa-dev:
  script:
    - git clone --depth=1 https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git prosa
    - cd prosa
    - opam pin add -n -y -k path rocq-prosa .
    - opam install -y -v -j `getconf _NPROCESSORS_ONLN` rocq-prosa
    - opam pin add -n -y -k path rocq-prosa-refinements .
    - opam install -y -v -j `getconf _NPROCESSORS_ONLN` rocq-prosa-refinements
    - cd ..

########################## Tests  ##########################

.test-all-examples:
  script:
    - >-
      for WORKLOAD in examples/*.yaml;
      do
        CERT=certs/cert-for-`basename $WORKLOAD`;
        echo; echo; echo;
        echo "==================";
        echo "Testing $WORKLOAD:";
        mkdir -p $CERT;
        ./poet -v -o $CERT -j `getconf _NPROCESSORS_ONLN` -s $WORKLOAD 2>&1 | tee -a $CERT/output.txt;
      done;

test-examples-with-stable-Prosa:
  extends:
    - .not_in_wip_branches
    - .preferred-stable-version
  stage: test
  script:
    - !reference [.test-all-examples, script]
  artifacts:
    name: "POET-example-certificates"
    paths:
      - "certs/"
    exclude:
      - certs/**/*.aux
      - certs/**/*.vo
      - certs/**/*.glob
      - certs/**/*.vok
      - certs/**/*.vos
    expire_in: 1 week

test-examples-with-Prosa-dev:
  extends:
    - .only_in_wip_branches
    - .preferred-dev-version
  stage: test
  script:
    - !reference [.install-Prosa-dev, script]
    - !reference [.test-all-examples, script]

random-test-cases:
  extends:
    - .not_in_wip_branches
    - .preferred-stable-version
  stage: test
  script:
    - >-
      for WORKLOAD in `ls test-cases/*.yaml | sort -R | head -10`;
      do
        CERT=certs/cert-for-test-case-`basename $WORKLOAD`;
        echo; echo; echo;
        echo "==================";
        echo "Testing $WORKLOAD:";
        mkdir -p $CERT;
        ./poet -v -o $CERT -j `getconf _NPROCESSORS_ONLN` -b -s $WORKLOAD 2>&1 | tee -a $CERT/output.txt;
      done;