diff options
| author | Pierre-Marie Pédrot | 2018-12-06 10:01:41 +0100 |
|---|---|---|
| committer | GitHub | 2018-12-06 10:01:41 +0100 |
| commit | f503e20667008eabb48aa1676ce56f4958c7087e (patch) | |
| tree | 94333b1e21124e4394dbd722276c37a62662f7a7 | |
| parent | 550472c67198353120cdc02b42683024b5b39765 (diff) | |
| parent | e2fe373a1947206746dd43afe6c9815c69453def (diff) | |
Merge pull request coq/ltac2#90 from ejgallego/tests
[build] Test tests in Travis, use coqc for tests.
| -rw-r--r-- | .travis.yml | 1 | ||||
| -rw-r--r-- | tests/Makefile | 4 | ||||
| -rw-r--r-- | 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. |