From e2fe373a1947206746dd43afe6c9815c69453def Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 28 Nov 2018 00:47:10 +0100
Subject: [build] Test tests in Travis, use coqc for tests.

`coqtop -batch` is an oxymoron, in prevision for upstream changes use
`coqc`.

We also call `make test` in Travis as to make CI more robust.
---
 .travis.yml      | 1 +
 tests/Makefile   | 4 ++--
 tests/example1.v | 1 +
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index d52b3ebd25..2628abde45 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -34,6 +34,7 @@ script:
     set -ex
     sudo chown -R coq:coq /home/coq/${CONTRIB_NAME}
     make
+    make tests
     "
 - docker stop COQ  # optional
 - echo -en 'travis_fold:end:script\\r'
diff --git a/tests/Makefile b/tests/Makefile
index 37915e0d6f..d85ae90dd6 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,11 +1,11 @@
 ifeq "$(COQBIN)" ""
-  COQBIN=$(dir $(shell which coqtop))/
+  COQBIN=$(dir $(shell which coqc))/
 endif
 
 all: $(patsubst %.v,%.v.log,$(wildcard *.v))
 
 %.v.log: %.v
-	$(COQBIN)/coqtop -batch -I ../src -Q ../theories Ltac2 -lv $< > $@
+	$(COQBIN)/coqc -I ../src -Q ../theories Ltac2 $< > $@
 	if [ $$? = 0 ]; then \
 		echo "    $<... OK"; \
 	else \
diff --git a/tests/example1.v b/tests/example1.v
index 1b26aad824..023791050f 100644
--- a/tests/example1.v
+++ b/tests/example1.v
@@ -24,3 +24,4 @@ Goal forall n m, n + m = 0 -> n = 0.
 Proof.
 refine (fun () => '(fun n m H => _)).
 let t := get_hyp_by_name @H in Message.print (Message.of_constr t).
+Abort.
-- 
cgit v1.2.3