diff options
| author |  Yishuai Li <yishuai@cis.upenn.edu> | 2018-04-13 20:09:00 -0400 |
|---|---|---|
| committer | Yishuai Li <yishuai@cis.upenn.edu> | 2018-04-15 02:58:06 -0400 |
| commit | 01aa4fb84a32d0a94f88c5ec785030264452ae91 (patch) | |
| tree | 3146e666de421ddc4f0edd50b81858069e3cb133 | |
| parent | c291a8829556dc2a61fcacc08b34e1d68d66b89e (diff) | |
Simplify CircleCI script
| -rw-r--r-- | .circleci/config.yml | 10 | ||||
| -rw-r--r-- | CREDITS | 2 |
2 files changed, 3 insertions, 9 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 352ec5a51..00db64f26 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -31,11 +31,11 @@ before_script: &before_script source ~/.profile printenv if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -yq && sudo apt-get install -yq --no-install-recommends ${EXTRA_PACKAGES}; fi + echo . ~/.profile >> $BASH_ENV opam-switch: &opam-switch name: Select opam switch command: | - source ~/.profile opam switch ${COMPILER} opam config list opam list @@ -48,7 +48,6 @@ opam-switch: &opam-switch - run: name: Cache selection command: | - source ~/.profile # We can't use environment variables in cache names # So put it in a file and use the checksum echo "$COMPILER" > COMPILER @@ -59,19 +58,16 @@ opam-switch: &opam-switch - run: name: Update opam lists command: | - source ~/.profile opam repository set-url default https://opam.ocaml.org opam update - run: name: Install opam packages command: | - source ~/.profile opam switch -j ${NJOBS} ${COMPILER} opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} - run: name: Clean cache command: | - source ~/.profile rm -rf ~/.opam/log/ - save_cache: key: coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}- @@ -93,13 +89,10 @@ opam-switch: &opam-switch - run: &build-configure name: Configure command: | - source ~/.profile - ./configure -local -native-compiler ${NATIVE_COMP} -coqide no - run: &build-build name: Build command: | - source ~/.profile make -j ${NJOBS} byte make -j ${NJOBS} make test-suite/misc/universes/all_stdlib.v @@ -118,7 +111,6 @@ opam-switch: &opam-switch - run: name: Test command: | - source ~/.profile dev/ci/ci-wrapper.sh ${CIRCLE_JOB} - persist_to_workspace: root: *workspace @@ -128,6 +128,8 @@ of the Coq Proof assistant during the indicated time: Matej Košík (INRIA, 2015-2017) Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS then IRIF, 2009-now) + Yishuai Li (ORCID: https://orcid.org/0000-0002-5728-5903 + U. Penn, 2018) Patrick Loiseleur (Paris Sud, 1997-1999) Evgeny Makarov (INRIA, 2007) Gregory Malecha (Harvard University 2013-2015, |