diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 1 | ||||
| -rw-r--r-- | mathcomp/Makefile.test-suite.coq.local | 22 | ||||
| -rw-r--r-- | mathcomp/test_suite/output.v | 4 | ||||
| -rw-r--r-- | mathcomp/test_suite/output.v.out | 48 | ||||
| -rw-r--r-- | mathcomp/test_suite/output.v.out.8.12 | 48 | ||||
| -rw-r--r-- | mathcomp/test_suite/output.v.out.8.13 | 49 |
7 files changed, 173 insertions, 0 deletions
@@ -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..a5fcc2c 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -70,6 +70,7 @@ make-coq-latest: script: - docker build --pull --build-arg=coq_image="coqorg/${CI_JOB_NAME//-/:}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" . - docker push "${IMAGE}" + - docker run --mount "type=bind,source=$(pwd),target=/home/coq/mathcomp" -w /home/coq/mathcomp -t "${IMAGE}" /bin/bash --login -c "set -x; cd mathcomp; make test-suite" - docker logout "${CI_REGISTRY}" except: - tags diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local new file mode 100644 index 0000000..5a1ec43 --- /dev/null +++ b/mathcomp/Makefile.test-suite.coq.local @@ -0,0 +1,22 @@ +OUTPUT_TESTS=test_suite/output.v + +OUTPUT_ARTIFACTS=$(OUTPUT_TESTS:%.v=%.v.out.new) + +COQ_VERSION=$(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 (or f.out if f.out.COQ_VERSION does not exist) +post-all:: $(OUTPUT_ARTIFACTS) + @for f in $(OUTPUT_TESTS); do\ + if [ -e $$f.out.$(COQ_VERSION) ]; then REFERENCE=$$f.out.$(COQ_VERSION);\ + else REFERENCE=$$f.out; fi;\ + diff -u $$REFERENCE $$f.out.new > /dev/null;\ + if [ $$? -ne 0 ]; \ + then echo "Output of file $$f differs!";\ + diff -u $$REFERENCE $$f.out.new;\ + exit 1;\ + fi;\ + done + +$(OUTPUT_ARTIFACTS): %.v.out.new: %.v all/all.vo + $(COQC) $(COQFLAGS) $(COQLIBS) $< > $<.out.new
\ No newline at end of file diff --git a/mathcomp/test_suite/output.v b/mathcomp/test_suite/output.v new file mode 100644 index 0000000..706f15d --- /dev/null +++ b/mathcomp/test_suite/output.v @@ -0,0 +1,4 @@ +From mathcomp Require Import all. + +Open Scope group_scope. +About 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..bc5d3c8 --- /dev/null +++ b/mathcomp/test_suite/output.v.out @@ -0,0 +1,48 @@ +cyclic_pgroup_Aut_structure : +forall [gT : finGroupType] [p : nat] [G : {group gT}], +p.-group G -> +cyclic G -> +G != 1 :> {set gT} -> +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]>]]]] + +cyclic_pgroup_Aut_structure is not universe polymorphic +Arguments cyclic_pgroup_Aut_structure [gT] [p]%nat_scope [G]%Group_scope +cyclic_pgroup_Aut_structure is opaque +Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure diff --git a/mathcomp/test_suite/output.v.out.8.12 b/mathcomp/test_suite/output.v.out.8.12 new file mode 100644 index 0000000..bc5d3c8 --- /dev/null +++ b/mathcomp/test_suite/output.v.out.8.12 @@ -0,0 +1,48 @@ +cyclic_pgroup_Aut_structure : +forall [gT : finGroupType] [p : nat] [G : {group gT}], +p.-group G -> +cyclic G -> +G != 1 :> {set gT} -> +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]>]]]] + +cyclic_pgroup_Aut_structure is not universe polymorphic +Arguments cyclic_pgroup_Aut_structure [gT] [p]%nat_scope [G]%Group_scope +cyclic_pgroup_Aut_structure is opaque +Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure diff --git a/mathcomp/test_suite/output.v.out.8.13 b/mathcomp/test_suite/output.v.out.8.13 new file mode 100644 index 0000000..0546b70 --- /dev/null +++ b/mathcomp/test_suite/output.v.out.8.13 @@ -0,0 +1,49 @@ +cyclic_pgroup_Aut_structure : +forall [gT : finGroupType] [p : nat] [G : {group gT}], +p.-group G -> +cyclic G -> +G != 1 :> {set gT} -> +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]>]]]] + +cyclic_pgroup_Aut_structure is not universe polymorphic +Arguments cyclic_pgroup_Aut_structure [gT] [p]%nat_scope [G]%Group_scope _ _ + _ +cyclic_pgroup_Aut_structure is opaque +Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure |