.gitlab-ci.yml

image: giomasce/testenv

variables:
  GIT_STRATEGY: fetch
  GIT_SUBMODULE_STRATEGY: recursive
  GIT_DEPTH: "3"

before_script:
  - cat /proc/cpuinfo
  - cat /proc/meminfo
  - apt-get update
  - apt-get install -y --no-upgrade eatmydata

stages:
  - build
  - test

build:
  stage: build
  script:
    - eatmydata apt-get install -y --no-upgrade build-essential libz3-dev libmicrohttpd-dev qt5-default libboost-all-dev binutils-dev pkg-config wget git
    - sed -i -e 's|^USE_QT = .*$|USE_QT = true|' mmpp.pro
    - sed -i -e 's|^USE_MICROHTTPD = .*$|USE_MICROHTTPD = true|' mmpp.pro
    - sed -i -e 's|^USE_BEAST = .*$|USE_BEAST = true|' mmpp.pro
    - sed -i -e 's|^USE_Z3 = .*$|USE_Z3 = true|' mmpp.pro
    - mkdir build
    - cd build
    - qmake ..
    - make -j $(nproc)
    - cd ..
    - mkdir artifacts
    - cp build/mmpp artifacts
    - strip artifacts/mmpp
  artifacts:
    paths:
      - artifacts

tsc:
  stage: build
  script:
    - eatmydata apt-get install -y --no-upgrade node-typescript
    - tsc -p resources/static/ts

scala:
  stage: build
  script:
    - eatmydata apt-get install -y --no-upgrade scala
    - cd gapt
    - ./download_gapt.sh
    - ./compile.sh
  artifacts:
    paths:
      - gapt/gapt-2.14.jar
      - gapt/*.class

test:
  stage: test
  script:
    - eatmydata apt-get install -y --no-upgrade build-essential libz3-dev libmicrohttpd-dev qt5-default libboost-all-dev binutils-dev wget
    - wget -q -O resources/set.mm https://github.com/giomasce/set.mm/raw/develop/set.mm
    - time ./artifacts/mmpp test

verify_all:
  stage: test
  script:
    - eatmydata apt-get install -y --no-upgrade build-essential libz3-dev libmicrohttpd-dev qt5-default libboost-all-dev binutils-dev git
    - git clone https://github.com/giomasce/metamath-test.git resources/metamath-test
    - time ./artifacts/mmpp verify_all

gapt:
  stage: test
  script:
    - eatmydata apt-get install -y --no-upgrade build-essential libz3-dev libmicrohttpd-dev qt5-default libboost-all-dev binutils-dev wget git scala prover9
    - wget -q -O resources/set.mm https://github.com/giomasce/set.mm/raw/develop/set.mm
    - cd gapt
    - "time ./run.sh ':- f | -f' > gapt1"
    - "time ./run.sh ':- ?x (f(x) -> !y f(y))' > gapt2"
    - "time ./run.sh '!x f(x) -> g :- ?x (f(x) -> g)' > gapt3"
    - "time ./run.sh '(f -> g) | (f -> h) :- f -> (g | h)' > gapt4"
    - "time ./run.sh '!x !y ((f(x)=f(y))->(x=y)) :- !x !y ((f(f(x))=f(f(y)))->x=y)' > gapt5"
    - "time ./run.sh '!X !Y !Z (mult(X, mult(Y, Z))=mult(mult(X, Y), Z)), !X (mult(X, e)=X) :- (!X (mult(X, X)=e))->(!X !Y (mult(X, Y)=mult(Y, X)))' > gapt6"
    - "time ./run.sh ':- ((?x !y (f(x) <-> f(y))) <-> ((?x (g(x)) <-> (!y g(y))))) <-> ((?x !y (g(x) <-> g(y))) <-> ((?x (f(x)) <-> (!y f(y)))))' > gapt7"
    - cd ..
    - "time ./artifacts/mmpp read_gapt < gapt/gapt1"
    - "time ./artifacts/mmpp read_gapt < gapt/gapt2"
    - "time ./artifacts/mmpp read_gapt < gapt/gapt3"
    - "time ./artifacts/mmpp read_gapt < gapt/gapt4"
    - "time ./artifacts/mmpp read_gapt < gapt/gapt5"
    - "time ./artifacts/mmpp read_gapt < gapt/gapt6"
    - "time ./artifacts/mmpp read_gapt < gapt/gapt7"