aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorArthur Azevedo de Amorim2021-03-09 09:57:19 -0500
committerArthur Azevedo de Amorim2021-03-11 14:29:10 -0500
commitb1dec36c75d883f84babe534be3a47d44633f4f7 (patch)
tree9e3e386e890df596ddd79f55a16e84d74192fbef /dev/ci
parentb55216ab3509f48e45aac035f1b799529d068f51 (diff)
Add deriving lib to CI.
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh5
-rwxr-xr-xdev/ci/ci-deriving.sh10
2 files changed, 15 insertions, 0 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 8bcbd90f0b..4799755b15 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -308,3 +308,8 @@ project sf "https://github.com/DeepSpec/sf" "master"
# Coqtail
########################################################################
project coqtail "https://github.com/whonore/Coqtail" "master"
+
+########################################################################
+# Deriving
+########################################################################
+project deriving "https://github.com/arthuraa/deriving" "master"
diff --git a/dev/ci/ci-deriving.sh b/dev/ci/ci-deriving.sh
new file mode 100755
index 0000000000..ec3625c177
--- /dev/null
+++ b/dev/ci/ci-deriving.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+install_ssreflect
+
+git_download deriving
+
+( cd "${CI_BUILD_DIR}/deriving" && make && make tests && make install )