Set up CI minimization resumption run for ci-oddorder

At coq/coq@1180a51 over coq/coq@f1de96d

.github/workflows/main.yml

@@ -20,7 +20,7 @@ jobs:
  - name: Run minimizer
  uses: coq-community/[email protected]
  with:
- #custom_image: 'registry.gitlab.com/coq/coq:CACHEKEY'
+ custom_image: 'registry.gitlab.inria.fr/coq/coq:edge_ubuntu-V2023-08-28-93124ee272'
  #coq_version: 'latest'
  #ocaml_version: 'default'
  custom_script: ./timeout-run.sh

bug.v

@@ -0,0 +1,249 @@
+
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-projection-no-head-constant" "-w" "-redundant-canonical-projection" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/oddorder/theories" "odd_order" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/HB" "HB" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/elpi" "elpi" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/mathcomp" "mathcomp" "-top" "odd_order.BGsection16") -*- *)
+(* File reduced by coq-bug-minimizer from original input, then from 1375 lines to 60 lines, then from 73 lines to 1675 lines, then from 1680 lines to 90 lines, then from 103 lines to 2712 lines, then from 2715 lines to 148 lines, then from 161 lines to 2932 lines, then from 2936 lines to 147 lines, then from 160 lines to 1746 lines, then from 1749 lines to 189 lines, then from 202 lines to 1254 lines, then from 1259 lines to 145 lines, then from 158 lines to 976 lines, then from 981 lines to 153 lines, then from 166 lines to 775 lines, then from 779 lines to 245 lines *)
+(* coqc version 8.19+alpha compiled with OCaml 4.14.1
+ coqtop version 728713d43dde:/builds/coq/coq/_build/default,(HEAD detached at 25e3b11) (25e3b11cee094cfce7e16d10e58d3b7b318ea70c)
+ Expected coqc runtime on this file: 2.237 sec *)
+Require mathcomp.solvable.pgroup.
+Require mathcomp.solvable.commutator.
+
+Module Export mathcomp_DOT_solvable_DOT_gseries_WRAPPED.
+Module Export gseries.
+Import mathcomp.ssreflect.ssrbool.
+Import mathcomp.ssreflect.fintype.
+Import mathcomp.ssreflect.finset.
+Import mathcomp.fingroup.fingroup.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Set Implicit Arguments.
+
+Import GroupScope.
+
+Section GroupDefs.
+
+Variable gT : finGroupType.
+Implicit Types A B U V : {set gT}.
+
+Definition maximal A B := [max A of G | G \proper B].
+
+Definition minnormal A B := [min A of G | G :!=: 1 & B \subset 'N(G)].
+
+Definition simple A := minnormal A A.
+End GroupDefs.
+
+Section Subnormal.
+
+End Subnormal.
+
+Section MorphSubNormal.
+
+End MorphSubNormal.
+
+Section MaxProps.
+
+End MaxProps.
+
+Section MinProps.
+
+End MinProps.
+
+Section MorphPreMax.
+
+End MorphPreMax.
+
+Section InjmMax.
+
+End InjmMax.
+
+Section QuoMax.
+
+End QuoMax.
+
+Section MaxNormalProps.
+
+End MaxNormalProps.
+
+Section Simple.
+
+End Simple.
+
+Section Chiefs.
+
+End Chiefs.
+
+Section Central.
+
+End Central.
+
+End gseries.
+Import mathcomp.ssreflect.ssrbool.
+Import mathcomp.ssreflect.ssrfun.
+Import mathcomp.ssreflect.fintype.
+Import mathcomp.ssreflect.finset.
+Import mathcomp.fingroup.fingroup.
+
+Set Implicit Arguments.
+
+Import GroupScope.
+
+Section PropertiesDefs.
+
+Variables (gT : finGroupType) (A : {set gT}).
+
+Definition solvable :=
+ [forall (G : {group gT} | G \subset A :&: [~: G, G]), G :==: 1].
+
+End PropertiesDefs.
+
+Import HB.structures.
+Import mathcomp.ssreflect.eqtype.
+Import mathcomp.ssreflect.ssrnat.
+Import mathcomp.ssreflect.choice.
+
+HB.mixin Record IsMinSimpleOddGroup gT of FinGroup gT := {
+ mFT_odd_full : odd #|[set: gT]|;
+ mFT_simple : simple [set: gT];
+ mFT_nonSolvable : ~~ solvable [set: gT];
+ mFT_min : forall M : {group gT}, M \proper [set: gT] -> solvable M
+}.
+
+#[short(type="minSimpleOddGroupType")]
+HB.structure
+Definition minSimpleOddGroup := { G of IsMinSimpleOddGroup G & FinGroup G }.
+
+Notation TheMinSimpleOddGroup gT :=
+ [set: BaseFinGroup.arg_sort gT]
+ (only parsing).
+
+Section MinSimpleOdd.
+
+Variable gT : minSimpleOddGroupType.
+Notation G := (TheMinSimpleOddGroup gT).
+
+Definition minSimple_max_groups := [set M : {group gT} | maximal M G].
+
+End MinSimpleOdd.
+
+Notation "''M'" := (minSimple_max_groups _) : group_scope.
+Import mathcomp.solvable.pgroup.
+Reserved Notation "M `_ \sigma" (at level 3, format "M `_ \sigma").
+
+Section Def.
+
+Variable gT : finGroupType.
+
+Variable M : {set gT}.
+
+Definition sigma :=
+ [pred p | [exists (P : {group gT} | p.-Sylow(M) P), 'N(P) \subset M]].
+Definition sigma_core := 'O_sigma(M).
+
+End Def.
+
+Notation "\sigma ( M )" := (sigma M) : group_scope.
+Notation "M `_ \sigma" := (sigma_core M) : group_scope.
+
+Import mathcomp.ssreflect.ssreflect.
+Import mathcomp.ssreflect.prime.
+
+Section Definitons.
+
+Variable gT : minSimpleOddGroupType.
+Implicit Type M X : {set gT}.
+
+Fact kappa_key : unit.
+Admitted.
+Definition kappa_def M : nat_pred.
+Admitted.
+Definition kappa := locked_with kappa_key kappa_def.
+
+Definition sigma_kappa M := [predU \sigma(M) & kappa M].
+
+Definition TypeF_maxgroups := [set M in 'M | (kappa M)^'.-group M].
+
+Definition TypeP_maxgroups := 'M :\: TypeF_maxgroups.
+
+Definition TypeP1_maxgroups :=
+ [set M in TypeP_maxgroups | (sigma_kappa M).-group M].
+
+End Definitons.
+
+Notation "\kappa ( M )" := (kappa M)
+ (at level 8, format "\kappa ( M )") : group_scope.
+
+Notation "''M_' ''P1'" := (TypeP1_maxgroups _)
+ (at level 2, format "''M_' ''P1'") : group_scope.
+
+Section Definitions.
+
+Variables (gT : finGroupType) (M : {set gT}).
+
+Definition Fitting_core :=
+ <<\bigcup_(P : {group gT} | Sylow M P && (P <| M)) P>>.
+
+End Definitions.
+
+Notation "M `_ \F" := (Fitting_core M)
+ (at level 3, format "M `_ \F") : group_scope.
+Import mathcomp.ssreflect.seq.
+Import mathcomp.fingroup.quotient.
+Import mathcomp.solvable.commutator.
+
+Section Definitions.
+
+Variable gT : minSimpleOddGroupType.
+
+Implicit Types M U V W X : {set gT}.
+
+Definition FTtype M :=
+ if \kappa(M)^'.-group M then 1%N else
+ if M`_\sigma != M^`(1) then 2 else
+ if M`_\F == M`_\sigma then 5 else
+ if abelian (M`_\sigma / M`_\F) then 3 else 4.
+
+Definition FTcore M := if 0 < FTtype M <= 2 then M`_\F else M^`(1).
+
+End Definitions.
+
+Notation "M `_ \s" := (FTcore M) (at level 3, format "M `_ \s") : group_scope.
+
+Variable gT : minSimpleOddGroupType.
+
+Variable M : {group gT}.
+
+Lemma FTtype_P1max : (M \in 'M_'P1) = (2 < FTtype M <= 5).
+Admitted.
+
+Lemma Msigma_eq_der1 : M \in 'M_'P1 -> M`_\sigma = M^`(1).
+Admitted.
+
+Lemma Fcore_eq_FTcore : reflect (M`_\F = M`_\s) (FTtype M \in pred3 1%N 2 5).
+Proof.
+rewrite /FTcore -mem_iota 3!inE orbA; case type12M: (_ || _); first by left.
+move: type12M FTtype_P1max; rewrite /FTtype; do 2![case: ifP => // _] => _.
+rewrite !(fun_if (leq^~ 5)) !(fun_if (leq 3)) !if_same /= => P1maxM.
+rewrite Msigma_eq_der1 // !(fun_if (eq_op^~ 5)) if_same.
+by rewrite [if _ then _ else _]andbT; apply: eqP.

coqbot-request-stamp

@@ -1 +1 @@
-DUMMY
+PR_kwDOABUDh85VFaaq <> coq-community/run-coq-bug-minimizer run-coq-bug-minimizer-124982383246 coq coq 17836

coqbot.ci-target

@@ -1 +1 @@
-TAKE FROM failing-log.log
+ci-oddorder

coqbot.compiler

@@ -1 +1 @@
-4.10.0
+4.14.1+flambda

coqbot.failing-artifact-urls

@@ -1 +1 @@
-
+https://gitlab.inria.fr/coq/coq/-/jobs/3443131/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3443171/artifacts/download

coqbot.failing-sha

@@ -1 +1 @@
-
+1180a512534f19bca0e1e8fffc96f553cd279bf5

coqbot.issue-number

@@ -0,0 +1 @@
+17836

coqbot.passing-artifact-urls

@@ -1 +1 @@
-
+https://gitlab.inria.fr/coq/coq/-/jobs/3442633/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3442673/artifacts/download

coqbot.passing-sha

@@ -1 +1 @@
-
+f1de96dc193b5889ba2ecbc9f276c3776e84248a

coqbot.resume-minimization-url

@@ -0,0 +1 @@
+https://coqbot.herokuapp.com/resume-ci-minimization

coqbot.resumption-args

@@ -0,0 +1,8 @@
+registry.gitlab.inria.fr/coq/coq:edge_ubuntu-V2023-08-28-93124ee272
+ci-oddorder
+4.14.1+flambda
+https://gitlab.inria.fr/coq/coq/-/jobs/3443131/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3443171/artifacts/download
+https://gitlab.inria.fr/coq/coq/-/jobs/3442633/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3442673/artifacts/download
+f1de96dc193b5889ba2ecbc9f276c3776e84248a
+1180a512534f19bca0e1e8fffc96f553cd279bf5
+

coqbot.url

@@ -0,0 +1 @@
+https://coqbot.herokuapp.com/ci-minimization