diff options
Diffstat (limited to 'test-suite')
22 files changed, 59 insertions, 31 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index c2d6e540c6..b627f680b9 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -45,7 +45,7 @@ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) # read out an emacs config and look for coq-prog-args; if such exists, return it get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1) -get_coq_prog_args = $(strip $(filter-out "-emacs-U" "-emacs",$(shell $(call get_coq_prog_args_helper,$(1))))) +get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1)))) SINGLE_QUOTE=" #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter # wrap the arguments in parens, but only if they exist @@ -490,7 +490,7 @@ coq-makefile/%.log : coq-makefile/%/run.sh $(HIDE)(\ cd coq-makefile/$* && \ ./run.sh 2>&1; \ - if [ $$? = 0 ]; then \ + if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ else \ diff --git a/test-suite/coq-makefile/arg/run.sh b/test-suite/coq-makefile/arg/run.sh index 28b9bcb969..e98da17c78 100755 --- a/test-suite/coq-makefile/arg/run.sh +++ b/test-suite/coq-makefile/arg/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh index ccb348c6fa..28d9878f9b 100755 --- a/test-suite/coq-makefile/compat-subdirs/run.sh +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index e071f1db7a..d6bb52bb4a 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e @@ -11,10 +11,11 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . ./test +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index e071f1db7a..d6bb52bb4a 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e @@ -11,10 +11,11 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . ./test +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/extend-subdirs/run.sh b/test-suite/coq-makefile/extend-subdirs/run.sh index db11601132..ea5792a937 100755 --- a/test-suite/coq-makefile/extend-subdirs/run.sh +++ b/test-suite/coq-makefile/extend-subdirs/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/latex1/run.sh b/test-suite/coq-makefile/latex1/run.sh index 45f2269113..214a9d5b28 100755 --- a/test-suite/coq-makefile/latex1/run.sh +++ b/test-suite/coq-makefile/latex1/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh index 9b89e5b6e9..752c0c2cea 100755 --- a/test-suite/coq-makefile/merlin1/run.sh +++ b/test-suite/coq-makefile/merlin1/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 418a2fb775..f6fb3bcb42 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -10,11 +10,12 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test ./test/test.glob +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 418a2fb775..f6fb3bcb42 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -10,11 +10,12 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test ./test/test.glob +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index a24a8a3cf7..863c39f500 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e @@ -13,7 +13,7 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 097bd6398a..bc9f846dda 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -12,11 +12,12 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test ./test/test.glob +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx diff --git a/test-suite/coq-makefile/only/run.sh b/test-suite/coq-makefile/only/run.sh index 4b471bcb80..2ea3deffb7 100755 --- a/test-suite/coq-makefile/only/run.sh +++ b/test-suite/coq-makefile/only/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 684e0ece82..24ef8c891b 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -11,7 +11,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index 684e0ece82..24ef8c891b 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -11,7 +11,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index 684e0ece82..24ef8c891b 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e @@ -11,7 +11,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find) | sort > actual +(cd `find tmp -name user-contrib`; find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index bfd2c1b959..bfd2c1b959 100644..100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index d241762791..e525e12086 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e @@ -13,7 +13,7 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh index d241762791..e525e12086 100755 --- a/test-suite/coq-makefile/uninstall2/run.sh +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash #set -x set -e @@ -13,7 +13,7 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/validate1/run.sh b/test-suite/coq-makefile/validate1/run.sh index 61025021d0..aaa4194b38 100755 --- a/test-suite/coq-makefile/validate1/run.sh +++ b/test-suite/coq-makefile/validate1/run.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash #set -x set -e diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out new file mode 100644 index 0000000000..bf1bf2809d --- /dev/null +++ b/test-suite/output/Show.out @@ -0,0 +1,12 @@ +3 subgoals (ID 29) + + H : 0 = 0 + ============================ + 1 = 1 + +subgoal 2 (ID 33) is: + 1 = S (S m') +subgoal 3 (ID 20) is: + S (S n') = S m + +(dependent evars: (printing disabled) ) diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v new file mode 100644 index 0000000000..60faac8dd9 --- /dev/null +++ b/test-suite/output/Show.v @@ -0,0 +1,11 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *) + +(* tests of Show output with -emacs flag to coqtop; see bug 5535 *) + +Theorem nums : forall (n m : nat), n = m -> (S n) = (S m). +Proof. + intros. + induction n as [| n']. + induction m as [| m']. + Show. +Admitted. |