begin a test suite

Makefile.coq.local

+# run tests with main build
+real-all: test
+
+# the test suite
+TESTFILES=$(wildcard tests/*.v)
+
+test: $(TESTFILES:.v=.vo)
+.PHONY: test
+
+COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
+
+# Can't use pipes because that discards error codes and dash provides no way to control that.
+# Also egrep errors if it doesn't match anything, we have to ignore that.
+# Oh Unix...
+REF_FILTER=egrep -v '(^Welcome to Coq|^Skipping rcfile loading.$$)'
+
+tests/.coqdeps.d: $(TESTFILES)
+	$(SHOW)'COQDEP TESTFILES'
+	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
+-include tests/.coqdeps.d
+
+$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
+	$(SHOW)$(if $(MAKE_REF),COQTEST [ref],COQTEST) $<
+	$(HIDE)TEST="$$(basename -s .v $<)" && \
+	  TMPFILE="$$(mktemp)" && \
+	  $(TIMER) $(COQ_TEST) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< $(TIMING_EXTRA) > "$$TMPFILE" && \
+	  ($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
+	  $(if $(MAKE_REF), \
+	    mv "$$TMPFILE.filtered" "tests/$$TEST.ref", \
+	    diff -u "tests/$$TEST.ref" "$$TMPFILE.filtered") && \
+	  rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
+	  touch $@

tests/solve_proper.v

+From stdpp Require Import prelude.
+
+(** Some tests for solve_proper. *)
+Section tests.
+  Context {A B : Type} `{!Equiv A, !Equiv B}.
+  Context (foo : A → A) (bar : A → B) (baz : B → A → A).
+  Context `{!Proper ((≡) ==> (≡)) foo,
+            !Proper ((≡) ==> (≡)) bar,
+            !Proper ((≡) ==> (≡) ==> (≡)) baz}.
+
+  Definition test1 (x : A) := baz (bar (foo x)) x.
+  Global Instance : Proper ((≡) ==> (≡)) test1.
+  Proof. solve_proper. Qed.
+
+  Definition test2 (b : bool) (x : A) :=
+    if b then bar (foo x) else bar x.
+  Global Instance : ∀ b, Proper ((≡) ==> (≡)) (test2 b).
+  Proof. solve_proper. Qed.
+
+  Definition test3 (f : nat → A) :=
+    baz (bar (f 0)) (f 2).
+  Global Instance : Proper (pointwise_relation nat (≡) ==> (≡)) test3.
+  Proof. solve_proper. Qed.
+End tests.

tests/typeclasses.v

+From stdpp Require Import prelude.
+
+(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
+    Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
+    we cannot [1].  So at least we try to make sure the first solution found
+    is the right one, to not pay performance in the success case [2].
+
+    [1] https://github.com/coq/coq/issues/7916
+    [2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
+*)
+Lemma test_setoid_rewrite :
+  exists R, @Reflexive Prop R /\ R = iff.
+Proof.
+  eexists. split.
+  - apply _.
+  - reflexivity.
+Qed.