aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Yishuai Li <yishuai@cis.upenn.edu>2018-04-13 20:09:00 -0400
committerGravatar Yishuai Li <yishuai@cis.upenn.edu>2018-04-15 02:58:06 -0400
commit01aa4fb84a32d0a94f88c5ec785030264452ae91 (patch)
tree3146e666de421ddc4f0edd50b81858069e3cb133
parentc291a8829556dc2a61fcacc08b34e1d68d66b89e (diff)
Simplify CircleCI script
-rw-r--r--.circleci/config.yml10
-rw-r--r--CREDITS2
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
diff --git a/CREDITS b/CREDITS
index 7d9dfb492..f59bfca86 100644
--- a/CREDITS
+++ b/CREDITS
@@ -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,