Merge PR#456: Proposing improvement to the CI targets for local use

1 files changed, 15 insertions, 7 deletions

diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 91a33695b0..1ea56af29a 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -1,16 +1,24 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-# MetaCoq + UniCoq
+unicoq_CI_BRANCH=master
+unicoq_CI_GITURL=https://github.com/unicoq/unicoq.git
+unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
 
-git_checkout master https://github.com/unicoq/unicoq.git unicoq
+metacoq_CI_BRANCH=master
+metacoq_CI_GITURL=https://github.com/MetaCoq/MetaCoq.git
+metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
 
-( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+# Setup UniCoq
 
-git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq
+git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
 
-( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
+( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
 
+# Setup MetaCoq
+
+git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR}
+
+( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )