From bc0a71056c24b29c8289395ee01740bb2ef7ad8d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 18 Nov 2019 17:40:51 +0100 Subject: [test suite] infrastructure to test how some statements are printed --- .gitignore | 1 + .gitlab-ci.yml | 1 + mathcomp/Makefile.test-suite.coq.local | 22 +++++++++++++++ mathcomp/test_suite/output.v | 4 +++ mathcomp/test_suite/output.v.out | 48 +++++++++++++++++++++++++++++++++ mathcomp/test_suite/output.v.out.8.12 | 48 +++++++++++++++++++++++++++++++++ mathcomp/test_suite/output.v.out.8.13 | 49 ++++++++++++++++++++++++++++++++++ 7 files changed, 173 insertions(+) create mode 100644 mathcomp/Makefile.test-suite.coq.local create mode 100644 mathcomp/test_suite/output.v create mode 100644 mathcomp/test_suite/output.v.out create mode 100644 mathcomp/test_suite/output.v.out.8.12 create mode 100644 mathcomp/test_suite/output.v.out.8.13 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..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 -- cgit v1.2.3 From c0214cdb4a44261db539b48fb76dbdaded87312b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Sep 2020 15:22:29 +0200 Subject: default reference file for < 8.12 --- mathcomp/test_suite/output.v.out | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/mathcomp/test_suite/output.v.out b/mathcomp/test_suite/output.v.out index bc5d3c8..122ddf0 100644 --- a/mathcomp/test_suite/output.v.out +++ b/mathcomp/test_suite/output.v.out @@ -1,5 +1,5 @@ cyclic_pgroup_Aut_structure : -forall [gT : finGroupType] [p : nat] [G : {group gT}], +forall (gT : finGroupType) (p : nat) (G : {group gT}), p.-group G -> cyclic G -> G != 1 :> {set gT} -> @@ -42,7 +42,7 @@ exists m : {perm gT} -> 'Z_q, 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 +Arguments gT, p, G are implicit +Argument scopes are [_ nat_scope Group_scope _ _ _] cyclic_pgroup_Aut_structure is opaque Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure -- cgit v1.2.3 From 8bfcb13c1576a8d6e55dc7c732ec3bda5f5e4f7d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Sep 2020 15:05:49 +0200 Subject: Update mathcomp/Makefile.test-suite.coq.local Co-authored-by: Erik Martin-Dorel --- mathcomp/Makefile.test-suite.coq.local | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local index 5a1ec43..6f9454b 100644 --- a/mathcomp/Makefile.test-suite.coq.local +++ b/mathcomp/Makefile.test-suite.coq.local @@ -10,8 +10,7 @@ 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 ]; \ + if ! diff -q "$$REFERENCE" "$$f.out.new"; \ then echo "Output of file $$f differs!";\ diff -u $$REFERENCE $$f.out.new;\ exit 1;\ @@ -19,4 +18,4 @@ post-all:: $(OUTPUT_ARTIFACTS) done $(OUTPUT_ARTIFACTS): %.v.out.new: %.v all/all.vo - $(COQC) $(COQFLAGS) $(COQLIBS) $< > $<.out.new \ No newline at end of file + $(COQC) $(COQFLAGS) $(COQLIBS) $< > $<.out.new -- cgit v1.2.3 From 18edef73cdf0fb6671dbfb2e9d5829182a065919 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Sep 2020 15:06:07 +0200 Subject: Update mathcomp/Makefile.test-suite.coq.local Co-authored-by: Erik Martin-Dorel --- mathcomp/Makefile.test-suite.coq.local | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local index 6f9454b..119eff1 100644 --- a/mathcomp/Makefile.test-suite.coq.local +++ b/mathcomp/Makefile.test-suite.coq.local @@ -11,8 +11,7 @@ post-all:: $(OUTPUT_ARTIFACTS) if [ -e $$f.out.$(COQ_VERSION) ]; then REFERENCE=$$f.out.$(COQ_VERSION);\ else REFERENCE=$$f.out; fi;\ if ! diff -q "$$REFERENCE" "$$f.out.new"; \ - then echo "Output of file $$f differs!";\ - diff -u $$REFERENCE $$f.out.new;\ + then diff -u "$$REFERENCE" "$$f.out.new"; \ exit 1;\ fi;\ done -- cgit v1.2.3 From ff61778018f5eff362a50e48e5b3fd30dec962d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Sep 2020 15:06:33 +0200 Subject: Update mathcomp/Makefile.test-suite.coq.local Co-authored-by: Erik Martin-Dorel --- mathcomp/Makefile.test-suite.coq.local | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local index 119eff1..9db49c5 100644 --- a/mathcomp/Makefile.test-suite.coq.local +++ b/mathcomp/Makefile.test-suite.coq.local @@ -16,5 +16,5 @@ post-all:: $(OUTPUT_ARTIFACTS) fi;\ done -$(OUTPUT_ARTIFACTS): %.v.out.new: %.v all/all.vo +$(OUTPUT_ARTIFACTS): %.v.out.new: %.v $(COQC) $(COQFLAGS) $(COQLIBS) $< > $<.out.new -- cgit v1.2.3 From c7b1927d8072040d573757d543e2355e8280b9ee Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Sep 2020 15:22:50 +0200 Subject: new attempt --- .gitlab-ci.yml | 70 +++++++++++++++++++++++++++ mathcomp/test_suite/output.v | 2 +- mathcomp/test_suite/output.v.out | 91 +++++++++++++++++------------------ mathcomp/test_suite/output.v.out.8.12 | 48 ------------------ mathcomp/test_suite/output.v.out.8.13 | 49 ------------------- 5 files changed, 115 insertions(+), 145 deletions(-) delete mode 100644 mathcomp/test_suite/output.v.out.8.12 delete mode 100644 mathcomp/test_suite/output.v.out.8.13 diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a5fcc2c..173d42d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -113,6 +113,76 @@ 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 + - cd mathcomp + - make test-suite + 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/test_suite/output.v b/mathcomp/test_suite/output.v index 706f15d..7e9def3 100644 --- a/mathcomp/test_suite/output.v +++ b/mathcomp/test_suite/output.v @@ -1,4 +1,4 @@ From mathcomp Require Import all. Open Scope group_scope. -About cyclic_pgroup_Aut_structure. \ No newline at end of file +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 index 122ddf0..4db5888 100644 --- a/mathcomp/test_suite/output.v.out +++ b/mathcomp/test_suite/output.v.out @@ -1,48 +1,45 @@ -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]>]] +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 - 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]>]]]] - -Arguments gT, p, G are implicit -Argument scopes are [_ nat_scope Group_scope _ _ _] -cyclic_pgroup_Aut_structure is opaque -Expands to: Constant mathcomp.solvable.extremal.cyclic_pgroup_Aut_structure + 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.12 b/mathcomp/test_suite/output.v.out.8.12 deleted file mode 100644 index bc5d3c8..0000000 --- a/mathcomp/test_suite/output.v.out.8.12 +++ /dev/null @@ -1,48 +0,0 @@ -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 deleted file mode 100644 index 0546b70..0000000 --- a/mathcomp/test_suite/output.v.out.8.13 +++ /dev/null @@ -1,49 +0,0 @@ -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 -- cgit v1.2.3 From 39d3e313614d33b353978847f8d00d3fa2f2428f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Sep 2020 17:49:43 +0200 Subject: fix --- .gitlab-ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 173d42d..3f8309a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -128,6 +128,7 @@ coq-dev: - git rev-parse --verify HEAD - git describe --all --long --abbrev=40 --always --dirty - pwd + script: - cd mathcomp - make test-suite except: -- cgit v1.2.3 From 8d17e971db2d29fad93443e730ee378ec768ba68 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Sep 2020 09:49:04 +0200 Subject: rm docker run --- .gitlab-ci.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3f8309a..eb221d7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -70,7 +70,6 @@ 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 -- cgit v1.2.3 From f3ad9538962cd36d90ea3a6724125f448d7c0b10 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Sep 2020 09:52:42 +0200 Subject: fix 8.9, 8.8 and 8.7 --- mathcomp/test_suite/output.v.out.8.7 | 1 + mathcomp/test_suite/output.v.out.8.8 | 1 + mathcomp/test_suite/output.v.out.8.9 | 46 ++++++++++++++++++++++++++++++++++++ 3 files changed, 48 insertions(+) create mode 120000 mathcomp/test_suite/output.v.out.8.7 create mode 120000 mathcomp/test_suite/output.v.out.8.8 create mode 100644 mathcomp/test_suite/output.v.out.8.9 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]>]]]] -- cgit v1.2.3 From 4c35b309ece8c57088dffd7bea0ef7878f1d8d12 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Sep 2020 10:35:45 +0200 Subject: coq 8.13 does not exists yet --- .gitlab-ci.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index eb221d7..c39da82 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -147,11 +147,11 @@ test-coq-dev: 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.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 -- cgit v1.2.3 From bcbf0850d771c889431fb8d3c073c41059268c05 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Sep 2020 13:55:40 +0200 Subject: Update mathcomp/Makefile.test-suite.coq.local Co-authored-by: Erik Martin-Dorel --- mathcomp/Makefile.test-suite.coq.local | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local index 9db49c5..2de68fc 100644 --- a/mathcomp/Makefile.test-suite.coq.local +++ b/mathcomp/Makefile.test-suite.coq.local @@ -2,13 +2,13 @@ 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) +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 (or f.out if f.out.COQ_VERSION does not exist) +# 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) ]; then REFERENCE=$$f.out.$(COQ_VERSION);\ + 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"; \ -- cgit v1.2.3 From a28ed91e0d3b2d03940c9b930ac516f0769f7e17 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Sep 2020 16:35:14 +0200 Subject: avoid rebuild --- .gitlab-ci.yml | 2 +- mathcomp/Makefile.common | 8 +++++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c39da82..443c93a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -129,7 +129,7 @@ coq-dev: - pwd script: - cd mathcomp - - make test-suite + - make test-suite TEST_SKIP_BUILD=1 except: - tags - merge_requests diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index b6b71ea..9759158 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -56,7 +56,13 @@ Makefile.coq: pre-makefile $(COQPROJECT) Makefile # Test suite --------------------------------------------------------- -test_suite/test_hierarchy_all.v: build +ifneq "$(TEST_SKIP_BUILD)" "" +TEST_DEP := +else +TEST_DEP := build +endif + +test_suite/test_hierarchy_all.v: $(TEST_DEP) COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/test_hierarchy_all.v Makefile.test-suite.coq: test_suite/test_hierarchy_all.v -- cgit v1.2.3 From cfa21928a5148f826e19aa5a78b83b5ed4e165b9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 12 Sep 2020 13:24:47 +0200 Subject: avoid all.vo --- mathcomp/Makefile.common | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common index 9759158..df43b4f 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -63,7 +63,14 @@ TEST_DEP := build endif test_suite/test_hierarchy_all.v: $(TEST_DEP) - COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/test_hierarchy_all.v + COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp \ + -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 -- cgit v1.2.3 From 755068fd34f0fa1e918123c4859aef2e89bedfca Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Sep 2020 13:58:24 +0200 Subject: test-suite works both in local and system wide mode --- mathcomp/Make.test-suite | 1 - mathcomp/Makefile.common | 6 ++++-- 2 files changed, 4 insertions(+), 3 deletions(-) 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 df43b4f..b1603e6 100644 --- a/mathcomp/Makefile.common +++ b/mathcomp/Makefile.common @@ -58,12 +58,14 @@ Makefile.coq: pre-makefile $(COQPROJECT) Makefile 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 -R . mathcomp \ + COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify $(MATHCOMP_PATH) \ -lib all_ssreflect \ -lib all_algebra \ -lib all_field \ @@ -73,7 +75,7 @@ test_suite/test_hierarchy_all.v: $(TEST_DEP) > 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 -- cgit v1.2.3 From 38b28c7d9756da7d346a1866a4ce712b1c3472af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Sep 2020 15:11:14 +0200 Subject: don't use all.v in output.v --- mathcomp/test_suite/output.v | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/mathcomp/test_suite/output.v b/mathcomp/test_suite/output.v index 7e9def3..b0b0996 100644 --- a/mathcomp/test_suite/output.v +++ b/mathcomp/test_suite/output.v @@ -1,4 +1,10 @@ -From mathcomp Require Import all. +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 -- cgit v1.2.3