Merge pull request #433 from math-comp/output-test

[test suite] infrastructure to test how some statements are printed

10 files changed, 213 insertions, 4 deletions

diff --git a/.gitignore b/.gitignore
index 9c96cbf..b67b048 100644
--- a/.gitignore
+++ b/.gitignore
@@ -25,6 +25,7 @@ mathcomp/ssrmatching.v
 mathcomp/ssreflect_plugin.mllib
 mathcomp/ssreflect_plugin.mlpack
 mathcomp/test_suite/hierarchy_test.v
+mathcomp/test_suite/*.v.out.new
 mathcomp-*.tar.gz
 *#
 htmldoc/mathcomp.*html
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6e96a28..443c93a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -112,6 +112,77 @@ coq-dev:
 ##### test stage
 ################
 
+# run "make test-suite" (required variable: COQ_VERSION)
+.test:
+  stage: test
+  image: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}_coq-${COQ_VERSION}"
+  before_script:
+    - cat /proc/{cpu,mem}info || true
+    # don't printenv to avoid cluttering the log
+    - opam config list
+    - opam repo list
+    - opam list
+    - coqc --version
+    - echo "${COQ_VERSION}"
+    - git rev-parse --verify HEAD
+    - git describe --all --long --abbrev=40 --always --dirty
+    - pwd
+  script:
+    - cd mathcomp
+    - make test-suite TEST_SKIP_BUILD=1
+  except:
+    - tags
+    - merge_requests
+
+# run "make test-suite" only for push pipelines (not for scheduled pipelines)
+.test-once:
+  extends: .test
+  except:
+    - tags
+    - merge_requests
+    - schedules
+
+test-coq-dev:
+  extends: .test
+  variables:
+    COQ_VERSION: "dev"
+
+# test-coq-8.13:
+#   # to be replaced with .test-once (to disable this nightly build) when 8.13.0 is released
+#   extends: .test
+#   variables:
+#     COQ_VERSION: "8.13"
+
+test-coq-8.12:
+  extends: .test-once
+  variables:
+    COQ_VERSION: "8.12"
+
+test-coq-8.11:
+  extends: .test-once
+  variables:
+    COQ_VERSION: "8.11"
+
+test-coq-8.10:
+  extends: .test-once
+  variables:
+    COQ_VERSION: "8.10"
+
+test-coq-8.9:
+  extends: .test-once
+  variables:
+    COQ_VERSION: "8.9"
+
+test-coq-8.8:
+  extends: .test-once
+  variables:
+    COQ_VERSION: "8.8"
+
+test-coq-8.7:
+  extends: .test-once
+  variables:
+    COQ_VERSION: "8.7"
+
 # set CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using
 .ci:
   stage: test
diff --git a/mathcomp/Make.test-suite b/mathcomp/Make.test-suite
index 0b51909..f34958d 100644
--- a/mathcomp/Make.test-suite
+++ b/mathcomp/Make.test-suite
@@ -3,7 +3,6 @@ test_suite/test_ssrAC.v
 test_suite/test_guard.v
 
 -I .
--R . mathcomp
 
 -arg -w -arg -notation-overridden
 -arg -w -arg -ambiguous-paths
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
index b6b71ea..b1603e6 100644
--- a/mathcomp/Makefile.common
+++ b/mathcomp/Makefile.common
@@ -56,11 +56,26 @@ Makefile.coq: pre-makefile $(COQPROJECT) Makefile
 
 # Test suite ---------------------------------------------------------
 
-test_suite/test_hierarchy_all.v: build
-	COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/test_hierarchy_all.v
+ifneq "$(TEST_SKIP_BUILD)" ""
+TEST_DEP :=
+MATHCOMP_PATH := -R test_suite mathcomp.test_suite
+else
+TEST_DEP := build
+MATHCOMP_PATH := -R . mathcomp
+endif
+
+test_suite/test_hierarchy_all.v: $(TEST_DEP)
+	COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify $(MATHCOMP_PATH) \
+		-lib all_ssreflect \
+		-lib all_algebra \
+		-lib all_field \
+		-lib all_character \
+		-lib all_fingroup \
+		-lib all_solvable \
+		> test_suite/test_hierarchy_all.v
 
 Makefile.test-suite.coq: test_suite/test_hierarchy_all.v
-	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f Make.test-suite -o Makefile.test-suite.coq
+	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f Make.test-suite $(MATHCOMP_PATH) -o Makefile.test-suite.coq
 
 # Global config, build, clean and distclean --------------------------
 config: sub-config this-config
diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local
new file mode 100644
index 0000000..2de68fc
--- /dev/null
+++ b/mathcomp/Makefile.test-suite.coq.local
@@ -0,0 +1,20 @@
+OUTPUT_TESTS=test_suite/output.v
+
+OUTPUT_ARTIFACTS=$(OUTPUT_TESTS:%.v=%.v.out.new)
+
+COQ_VERSION_MINOR=$(shell $(COQC) -print-version | cut -d ' ' -f 1 | cut -d '.' -f 1-2)
+
+# Given a file f we compare its compilation output f.out.new with
+# f.out.COQ_VERSION_MINOR (or f.out if f.out.COQ_VERSION_MINOR does not exist)
+post-all:: $(OUTPUT_ARTIFACTS)
+	@for f in $(OUTPUT_TESTS); do\
+	  if [ -e "$$f.out.$(COQ_VERSION_MINOR)" ]; then REFERENCE="$$f.out.$(COQ_VERSION_MINOR)";\
+	  else REFERENCE=$$f.out; fi;\
+	  if ! diff -q "$$REFERENCE" "$$f.out.new"; \
+	    then diff -u "$$REFERENCE" "$$f.out.new"; \
+		exit 1;\
+	  fi;\
+	done
+
+$(OUTPUT_ARTIFACTS): %.v.out.new: %.v
+	$(COQC) $(COQFLAGS) $(COQLIBS) $< > $<.out.new
diff --git a/mathcomp/test_suite/output.v b/mathcomp/test_suite/output.v
new file mode 100644
index 0000000..b0b0996
--- /dev/null
+++ b/mathcomp/test_suite/output.v
@@ -0,0 +1,10 @@
+From mathcomp Require Import
+  all_ssreflect
+  all_algebra
+  all_field
+  all_character
+  all_fingroup
+  all_solvable.
+
+Open Scope group_scope.
+Check @cyclic_pgroup_Aut_structure.
\ No newline at end of file
diff --git a/mathcomp/test_suite/output.v.out b/mathcomp/test_suite/output.v.out
new file mode 100644
index 0000000..4db5888
--- /dev/null
+++ b/mathcomp/test_suite/output.v.out
@@ -0,0 +1,45 @@
+cyclic_pgroup_Aut_structure
+     : forall (gT : finGroupType) (p : nat) (G : {group gT}),
+       p.-group G ->
+       cyclic G ->
+       G != 1 ->
+       let q := #|G| in
+       let n := (logn p q).-1 in
+       let A := Aut G in
+       let P := 'O_p(A) in
+       let F := 'O_p^'(A) in
+       exists m : {perm gT} -> 'Z_q,
+         [/\ [/\ {in A & G, forall (a : {perm gT}) (x : gT), x ^+ m a = a x},
+                 m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}},
+                 {in A &, injective m} /\ [seq m x | x in A] =i GRing.unit,
+                 forall k : nat,
+                 {in A, {morph m : a / a ^+ k >-> (a ^+ k)%R}}
+               & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
+             [/\ abelian A, cyclic F, #|F| = p.-1
+               & [faithful F, on 'Ohm_1(G) | [Aut G]]]
+           & if n == 0
+             then A = F
+             else
+              exists t : perm_for_finType gT,
+                [/\ t \in A, #[t] = 2, m t = (-1)%R
+                  & if odd p
+                    then
+                     [/\ cyclic A /\ cyclic P,
+                         exists s : perm_for_finType gT,
+                           [/\ s \in A, #[s] = (p ^ n)%N, m s = (p.+1%:R)%R
+                             & P = <[s]>]
+                       & exists s0 : perm_for_finType gT,
+                           [/\ s0 \in A, #[s0] = p, m s0 = ((p ^ n).+1%:R)%R
+                             & 'Ohm_1(P) = <[s0]>]]
+                    else
+                     if n == 1
+                     then A = <[t]>
+                     else
+                      exists s : perm_for_finType gT,
+                        [/\ s \in A, #[s] = (2 ^ n.-1)%N, 
+                           m s = (5%:R)%R, <[s]> \x <[t]> = A
+                          & exists s0 : perm_for_finType gT,
+                              [/\ s0 \in A, #[s0] = 2,
+                                  m s0 = ((2 ^ n).+1%:R)%R,
+                                  m (s0 * t) = ((2 ^ n).-1%:R)%R
+                                & 'Ohm_1(<[s]>) = <[s0]>]]]]
diff --git a/mathcomp/test_suite/output.v.out.8.7 b/mathcomp/test_suite/output.v.out.8.7
new file mode 120000
index 0000000..896b7ac
--- /dev/null
+++ b/mathcomp/test_suite/output.v.out.8.7
@@ -0,0 +1 @@
+output.v.out.8.9
\ No newline at end of file
diff --git a/mathcomp/test_suite/output.v.out.8.8 b/mathcomp/test_suite/output.v.out.8.8
new file mode 120000
index 0000000..896b7ac
--- /dev/null
+++ b/mathcomp/test_suite/output.v.out.8.8
@@ -0,0 +1 @@
+output.v.out.8.9
\ No newline at end of file
diff --git a/mathcomp/test_suite/output.v.out.8.9 b/mathcomp/test_suite/output.v.out.8.9
new file mode 100644
index 0000000..25583d5
--- /dev/null
+++ b/mathcomp/test_suite/output.v.out.8.9
@@ -0,0 +1,46 @@
+cyclic_pgroup_Aut_structure
+     : forall (gT : finGroupType) (p : nat) (G : {group gT}),
+       p.-group G ->
+       cyclic G ->
+       G != 1 ->
+       let q := #|G| in
+       let n := (logn p q).-1 in
+       let A := Aut G in
+       let P := 'O_p(A) in
+       let F := 'O_p^'(A) in
+       exists m : {perm gT} -> 'Z_q,
+         [/\ [/\ {in A & G, forall (a : {perm gT}) (x : gT), x ^+ m a = a x},
+                 m 1 = 1%R /\ {in A &, {morph m : a b / a * b >-> (a * b)%R}},
+                 {in A &, injective m} /\ [seq m x | x in A] =i GRing.unit,
+                 forall k : nat,
+                 {in A, {morph m : a / a ^+ k >-> 
+                 (a ^+ k)%R}}
+               & {in A, {morph m : a / a^-1 >-> (a^-1)%R}}],
+             [/\ abelian A, cyclic F, #|F| = p.-1
+               & [faithful F, on 'Ohm_1(G) | [Aut G]]]
+           & if n == 0
+             then A = F
+             else
+              exists t : perm_for_finType gT,
+                [/\ t \in A, #[t] = 2, m t = (-1)%R
+                  & if odd p
+                    then
+                     [/\ cyclic A /\ cyclic P,
+                         exists s : perm_for_finType gT,
+                           [/\ s \in A, #[s] = (p ^ n)%N, m s = (p.+1%:R)%R
+                             & P = <[s]>]
+                       & exists s0 : perm_for_finType gT,
+                           [/\ s0 \in A, #[s0] = p, m s0 = ((p ^ n).+1%:R)%R
+                             & 'Ohm_1(P) = <[s0]>]]
+                    else
+                     if n == 1
+                     then A = <[t]>
+                     else
+                      exists s : perm_for_finType gT,
+                        [/\ s \in A, #[s] = (2 ^ n.-1)%N, 
+                           m s = (5%:R)%R, <[s]> \x <[t]> = A
+                          & exists s0 : perm_for_finType gT,
+                              [/\ s0 \in A, #[s0] = 2,
+                                  m s0 = ((2 ^ n).+1%:R)%R,
+                                  m (s0 * t) = ((2 ^ n).-1%:R)%R
+                                & 'Ohm_1(<[s]>) = <[s0]>]]]]