Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v (from ci-hott) (full log on GitHub Actions)
We are collecting data on the user experience of the Coq Bug Minimizer.
If you haven't already filled the survey for this PR, please fill out our short survey!
Minimized Coq File (consider adding this file to the test-suite)
```coq
(** * Coproduct of natural transformations *)
Require Coq.Init.Ltac.
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Require Import HoTT.Categories.Category.Sum HoTT.Categories.Functor.Sum HoTT.Categories.NaturalTransformation.Core.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Section sum.
Definition sum
C C' D F G F' G'
(T : @NaturalTransformation C D F G)
(T' : @NaturalTransformation C' D F' G')
: NaturalTransformation (F + F') (G + G').
Proof.
refine (Build_NaturalTransformation
(F + F') (G + G')
(fun x => match x with
| Datatypes.inl c => T c
| Datatypes.inr c' => T' c'
end)
_).
abstract (
repeat (intros [] || intro); simpl;
auto with natural_transformation
).
Defined.
End sum.
Module Export NaturalTransformationSumNotations.
Notation "T + U" := (sum T U) : natural_transformation_scope.
End NaturalTransformationSumNotations.
```
Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)
```coq
```
Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 2.9MiB file on GitHub Actions Artifacts under build.log)
```
0m00.71s | 367072 ko | Algebra/Groups/GroupCoeq.vo
0m00.71s | 346456 ko | Modalities/Descent.vo
0m00.70s | 351340 ko | Homotopy/Suspension.vo
0m00.61s | 395152 ko | Homotopy/WhiteheadsPrinciple.vo
0m00.57s | 343872 ko | Truncations/Connectedness.vo
0m00.55s | 328068 ko | Cubical/DPathCube.vo
0m00.55s | 361536 ko | ObjectClassifier.vo
0m00.54s | 348028 ko | Spaces/Finite/Fin.vo
0m00.52s | 344664 ko | Modalities/Localization.vo
0m00.51s | 373120 ko | Algebra/Groups/Presentation.vo
0m00.51s | 354828 ko | Homotopy/Join.vo
0m00.49s | 368648 ko | Algebra/AbGroups/AbelianGroup.vo
0m00.47s | 322332 ko | HIT/Flattening.vo
0m00.47s | 349668 ko | Projective.vo
0m00.46s | 342284 ko | HIT/epi.vo
0m00.45s | 346784 ko | Spaces/Nat/Arithmetic.vo
0m00.42s | 320264 ko | Cubical/PathSquare.vo
0m00.42s | 349772 ko | Modalities/Separated.vo
0m00.41s | 377128 ko | Algebra/Groups/ShortExactSequence.vo
0m00.39s | 347804 ko | Classes/theory/groups.vo
0m00.39s | 343896 ko | Constant.vo
0m00.39s | 347108 ko | Pointed/pTrunc.vo
0m00.36s | 351376 ko | Algebra/Groups/Image.vo
0m00.36s | 318392 ko | Categories/ExponentialLaws/Law4/Functors.vo
0m00.36s | 223692 ko | Spaces/Finite/FinInduction.vo
0m00.35s | 370624 ko | Algebra/Groups/Lagrange.vo
0m00.35s | 345236 ko | Spaces/Int/Spec.vo
0m00.35s | 344268 ko | Spaces/Nat/Core.vo
0m00.34s | 341948 ko | DProp.vo
0m00.32s | 368904 ko | Algebra/AbGroups/AbHom.vo
0m00.32s | 353256 ko | Truncations/SeparatedTrunc.vo
0m00.31s | 320576 ko | Categories/Functor/Pointwise/Properties.vo
0m00.31s | 330160 ko | Pointed/pMap.vo
0m00.31s | 342144 ko | Truncations/Core.vo
0m00.30s | 353180 ko | Homotopy/Freudenthal.vo
0m00.30s | 320124 ko | Spaces/Circle.vo
0m00.29s | 366956 ko | Algebra/AbGroups/Centralizer.vo
0m00.29s | 332120 ko | Colimits/MappingCylinder.vo
0m00.28s | 351124 ko | Algebra/Groups/Kernel.vo
0m00.27s | 299068 ko | Spaces/Int/LoopExp.vo
0m00.26s | 301936 ko | Algebra/AbGroups/Cyclic.vo
0m00.26s | 324124 ko | Categories/ProductLaws.vo
0m00.26s | 319920 ko | Spaces/Finite/FinNat.vo
0m00.24s | 287168 ko | Categories/Functor/Attributes.vo
0m00.23s | 262924 ko | Classes/interfaces/canonical_names.vo
0m00.23s | 271072 ko | Spaces/Pos/Spec.vo
0m00.22s | 317528 ko | Pointed/pHomotopy.vo
0m00.21s | 271056 ko | Algebra/AbGroups/AbProjective.vo
0m00.21s | 334992 ko | Categories/Functor/Composition/Functorial/Attributes.vo
0m00.21s | 276672 ko | Pointed/pSect.vo
0m00.20s | 254200 ko | Algebra/AbGroups/AbPullback.vo
0m00.20s | 211176 ko | Categories/NaturalTransformation/Isomorphisms.vo
0m00.20s | 221352 ko | Modalities/Accessible.vo
0m00.18s | 184024 ko | Pointed/pEquiv.vo
0m00.17s | 204528 ko | Algebra/AbGroups/Z.vo
0m00.16s | 289568 ko | Cubical/DPathSquare.vo
0m00.16s | 194812 ko | Spaces/No/Negation.vo
0m00.14s | 228068 ko | Algebra/AbGroups.vo
0m00.14s | 140164 ko | Modalities/Identity.vo
0m00.14s | 171760 ko | Pointed/pModality.vo
0m00.14s | 155392 ko | Spaces/Int/Core.vo
0m00.14s | 184836 ko | Spaces/Pos/Core.vo
0m00.13s | 148908 ko | Algebra/Congruence.vo
0m00.13s | 128172 ko | Categories/Functor/Notations.vo
0m00.13s | 167520 ko | Colimits/SpanPushout.vo
0m00.13s | 143216 ko | Spaces/Finite.vo
0m00.13s | 162300 ko | Spaces/Int/Equiv.vo
0m00.12s | 204824 ko | Algebra/Groups.vo
0m00.12s | 146836 ko | Categories/Category.vo
0m00.12s | 159984 ko | Homotopy/SuccessorStructure.vo
0m00.11s | 144020 ko | Categories/Functor.vo
0m00.11s | 126472 ko | Categories/Functor/Composition.vo
0m00.11s | 135104 ko | HIT/unique_choice.vo
0m00.11s | 134544 ko | Pointed.vo
0m00.11s | 115496 ko | Truncations.vo
0m00.10s | 92340 ko | Categories/Category/Sigma.vo
0m00.10s | 133404 ko | Categories/Functor/Composition/Functorial.vo
0m00.10s | 121280 ko | Categories/Functor/Composition/Functorial/Core.vo
0m00.10s | 124892 ko | Categories/Functor/Prod/Functorial.vo
0m00.10s | 83288 ko | Cubical.vo
0m00.10s | 106444 ko | HIT/SetCone.vo
0m00.10s | 124372 ko | Spaces/Nat.vo
0m00.10s | 144588 ko | Spaces/No.vo
0m00.09s | 141024 ko | Categories/Functor/Pointwise/Core.vo
0m00.09s | 113992 ko | HIT/iso.vo
0m00.08s | 70636 ko | Categories/Functor/Prod.vo
0m00.08s | 132620 ko | Categories/HomFunctor.vo
0m00.08s | 117980 ko | Spaces/Pos.vo
0m00.07s | 79892 ko | Categories/Category/Notations.vo
0m00.07s | 88536 ko | Categories/FunctorCategory/Core.vo
0m00.07s | 85740 ko | Categories/NaturalTransformation/Composition/Functorial.vo
0m00.07s | 81096 ko | Categories/NaturalTransformation/Sum.vo
0m00.07s | 122936 ko | Spaces/Int.vo
0m00.06s | 71620 ko | Categories/Functor/Pointwise.vo
0m00.06s | 65180 ko | Categories/NaturalTransformation/Composition.vo
0m00.06s | 132588 ko | Spaces/Finite/Tactics.vo
0m00.05s | 70900 ko | Categories/Category/Subcategory/Full.vo
0m00.04s | 69704 ko | Categories/Category/Subcategory.vo
Makefile.ci:155: recipe for target 'ci-hott' failed
make: *** [ci-hott] Error 2
/github/workspace/builds/coq /github/workspace
::endgroup::
```
Minimization Log
```
Coq version: 8.19+alpha compiled with OCaml 4.09.0
First, I will attempt to absolutize relevant [Require]s in /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v, and store the result in /github/workspace/cwd/bug_01.v...
getting /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v
getting /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.glob
Now, I will attempt to coq the file, and find the error...
Coqing the file (/github/workspace/cwd/bug_01.v)...
Running command: "/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig" "-time-file" "theories/Categories/NaturalTransformation/Sum.v.timing" "-q" "-noinit" "-indices-matter" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/theories" "HoTT" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/contrib" "HoTT.Contrib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "HoTT.Categories.NaturalTransformation.Sum" "-R" "/tmp/tmpkuugzbjr" "" "/tmp/tmpkuugzbjr/HoTT/Categories/NaturalTransformation/Sum.v" "-q"
The timeout for /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig has been set to: 3
This file produces the following output when Coq'ed:
Error:
System error: "theories/Categories/NaturalTransformation/Sum.v.timing: No such file or directory"
The current state of the file does not have a recognizable error.
Traceback (most recent call last):
File "/github/workspace/coq-tools/find-bug.py", line 1470, in
env['error_reg_string'] = get_error_reg_string(output_file_name, **env)
File "/github/workspace/coq-tools/find-bug.py", line 284, in get_error_reg_string
error_reg_string = get_error_reg_string_of_output(output, **kwargs)
File "/github/workspace/coq-tools/find-bug.py", line 246, in get_error_reg_string_of_output
error_reg_string = rawMinimized File /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v (from ci-hott) (full log [on GitHub Actions](https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/5680722946))
We are collecting data on the user experience of the Coq Bug Minimizer.
If you haven't already filled the survey *for this PR*, please fill out [our short survey](https://docs.google.com/forms/d/e/1FAIpQLSeWNKcF_XM0PPkydbvx4gaiKJFUG5xpMyewYK1dbtjAQt7FnQ/viewform?entry.155981120=17888)!
Minimized Coq File (consider adding this file to the test-suite)
```coq
(** * Coproduct of natural transformations *)
Require Coq.Init.Ltac.
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Require Import HoTT.Categories.Category.Sum HoTT.Categories.Functor.Sum HoTT.Categories.NaturalTransformation.Core.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Section sum.
Definition sum
C C' D F G F' G'
(T : @NaturalTransformation C D F G)
(T' : @NaturalTransformation C' D F' G')
: NaturalTransformation (F + F') (G + G').
Proof.
refine (Build_NaturalTransformation
(F + F') (G + G')
(fun x => match x with
| Datatypes.inl c => T c
| Datatypes.inr c' => T' c'
end)
_).
abstract (
repeat (intros [] || intro); simpl;
auto with natural_transformation
).
Defined.
End sum.
Module Export NaturalTransformationSumNotations.
Notation "T + U" := (sum T U) : natural_transformation_scope.
End NaturalTransformationSumNotations.
```
Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)
```coq
```
Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 2.9MiB file on GitHub Actions Artifacts under build.log)
```
0m00.71s | 367072 ko | Algebra/Groups/GroupCoeq.vo
0m00.71s | 346456 ko | Modalities/Descent.vo
0m00.70s | 351340 ko | Homotopy/Suspension.vo
0m00.61s | 395152 ko | Homotopy/WhiteheadsPrinciple.vo
0m00.57s | 343872 ko | Truncations/Connectedness.vo
0m00.55s | 328068 ko | Cubical/DPathCube.vo
0m00.55s | 361536 ko | ObjectClassifier.vo
0m00.54s | 348028 ko | Spaces/Finite/Fin.vo
0m00.52s | 344664 ko | Modalities/Localization.vo
0m00.51s | 373120 ko | Algebra/Groups/Presentation.vo
0m00.51s | 354828 ko | Homotopy/Join.vo
0m00.49s | 368648 ko | Algebra/AbGroups/AbelianGroup.vo
0m00.47s | 322332 ko | HIT/Flattening.vo
0m00.47s | 349668 ko | Projective.vo
0m00.46s | 342284 ko | HIT/epi.vo
0m00.45s | 346784 ko | Spaces/Nat/Arithmetic.vo
0m00.42s | 320264 ko | Cubical/PathSquare.vo
0m00.42s | 349772 ko | Modalities/Separated.vo
0m00.41s | 377128 ko | Algebra/Groups/ShortExactSequence.vo
0m00.39s | 347804 ko | Classes/theory/groups.vo
0m00.39s | 343896 ko | Constant.vo
0m00.39s | 347108 ko | Pointed/pTrunc.vo
0m00.36s | 351376 ko | Algebra/Groups/Image.vo
0m00.36s | 318392 ko | Categories/ExponentialLaws/Law4/Functors.vo
0m00.36s | 223692 ko | Spaces/Finite/FinInduction.vo
0m00.35s | 370624 ko | Algebra/Groups/Lagrange.vo
0m00.35s | 345236 ko | Spaces/Int/Spec.vo
0m00.35s | 344268 ko | Spaces/Nat/Core.vo
0m00.34s | 341948 ko | DProp.vo
0m00.32s | 368904 ko | Algebra/AbGroups/AbHom.vo
0m00.32s | 353256 ko | Truncations/SeparatedTrunc.vo
0m00.31s | 320576 ko | Categories/Functor/Pointwise/Properties.vo
0m00.31s | 330160 ko | Pointed/pMap.vo
0m00.31s | 342144 ko | Truncations/Core.vo
0m00.30s | 353180 ko | Homotopy/Freudenthal.vo
0m00.30s | 320124 ko | Spaces/Circle.vo
0m00.29s | 366956 ko | Algebra/AbGroups/Centralizer.vo
0m00.29s | 332120 ko | Colimits/MappingCylinder.vo
0m00.28s | 351124 ko | Algebra/Groups/Kernel.vo
0m00.27s | 299068 ko | Spaces/Int/LoopExp.vo
0m00.26s | 301936 ko | Algebra/AbGroups/Cyclic.vo
0m00.26s | 324124 ko | Categories/ProductLaws.vo
0m00.26s | 319920 ko | Spaces/Finite/FinNat.vo
0m00.24s | 287168 ko | Categories/Functor/Attributes.vo
0m00.23s | 262924 ko | Classes/interfaces/canonical_names.vo
0m00.23s | 271072 ko | Spaces/Pos/Spec.vo
0m00.22s | 317528 ko | Pointed/pHomotopy.vo
0m00.21s | 271056 ko | Algebra/AbGroups/AbProjective.vo
0m00.21s | 334992 ko | Categories/Functor/Composition/Functorial/Attributes.vo
0m00.21s | 276672 ko | Pointed/pSect.vo
0m00.20s | 254200 ko | Algebra/AbGroups/AbPullback.vo
0m00.20s | 211176 ko | Categories/NaturalTransformation/Isomorphisms.vo
0m00.20s | 221352 ko | Modalities/Accessible.vo
0m00.18s | 184024 ko | Pointed/pEquiv.vo
0m00.17s | 204528 ko | Algebra/AbGroups/Z.vo
0m00.16s | 289568 ko | Cubical/DPathSquare.vo
0m00.16s | 194812 ko | Spaces/No/Negation.vo
0m00.14s | 228068 ko | Algebra/AbGroups.vo
0m00.14s | 140164 ko | Modalities/Identity.vo
0m00.14s | 171760 ko | Pointed/pModality.vo
0m00.14s | 155392 ko | Spaces/Int/Core.vo
0m00.14s | 184836 ko | Spaces/Pos/Core.vo
0m00.13s | 148908 ko | Algebra/Congruence.vo
0m00.13s | 128172 ko | Categories/Functor/Notations.vo
0m00.13s | 167520 ko | Colimits/SpanPushout.vo
0m00.13s | 143216 ko | Spaces/Finite.vo
0m00.13s | 162300 ko | Spaces/Int/Equiv.vo
0m00.12s | 204824 ko | Algebra/Groups.vo
0m00.12s | 146836 ko | Categories/Category.vo
0m00.12s | 159984 ko | Homotopy/SuccessorStructure.vo
0m00.11s | 144020 ko | Categories/Functor.vo
0m00.11s | 126472 ko | Categories/Functor/Composition.vo
0m00.11s | 135104 ko | HIT/unique_choice.vo
0m00.11s | 134544 ko | Pointed.vo
0m00.11s | 115496 ko | Truncations.vo
0m00.10s | 92340 ko | Categories/Category/Sigma.vo
0m00.10s | 133404 ko | Categories/Functor/Composition/Functorial.vo
0m00.10s | 121280 ko | Categories/Functor/Composition/Functorial/Core.vo
0m00.10s | 124892 ko | Categories/Functor/Prod/Functorial.vo
0m00.10s | 83288 ko | Cubical.vo
0m00.10s | 106444 ko | HIT/SetCone.vo
0m00.10s | 124372 ko | Spaces/Nat.vo
0m00.10s | 144588 ko | Spaces/No.vo
0m00.09s | 141024 ko | Categories/Functor/Pointwise/Core.vo
0m00.09s | 113992 ko | HIT/iso.vo
0m00.08s | 70636 ko | Categories/Functor/Prod.vo
0m00.08s | 132620 ko | Categories/HomFunctor.vo
0m00.08s | 117980 ko | Spaces/Pos.vo
0m00.07s | 79892 ko | Categories/Category/Notations.vo
0m00.07s | 88536 ko | Categories/FunctorCategory/Core.vo
0m00.07s | 85740 ko | Categories/NaturalTransformation/Composition/Functorial.vo
0m00.07s | 81096 ko | Categories/NaturalTransformation/Sum.vo
0m00.07s | 122936 ko | Spaces/Int.vo
0m00.06s | 71620 ko | Categories/Functor/Pointwise.vo
0m00.06s | 65180 ko | Categories/NaturalTransformation/Composition.vo
0m00.06s | 132588 ko | Spaces/Finite/Tactics.vo
0m00.05s | 70900 ko | Categories/Category/Subcategory/Full.vo
0m00.04s | 69704 ko | Categories/Category/Subcategory.vo
Makefile.ci:155: recipe for target 'ci-hott' failed
make: *** [ci-hott] Error 2
/github/workspace/builds/coq /github/workspace
::endgroup::
```
Minimization Log
```
Coq version: 8.19+alpha compiled with OCaml 4.09.0
First, I will attempt to absolutize relevant [Require]s in /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v, and store the result in /github/workspace/cwd/bug_01.v...
getting /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v
getting /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.glob
Now, I will attempt to coq the file, and find the error...
Coqing the file (/github/workspace/cwd/bug_01.v)...
Running command: "/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig" "-time-file" "theories/Categories/NaturalTransformation/Sum.v.timing" "-q" "-noinit" "-indices-matter" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/theories" "HoTT" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/contrib" "HoTT.Contrib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "HoTT.Categories.NaturalTransformation.Sum" "-R" "/tmp/tmpkuugzbjr" "" "/tmp/tmpkuugzbjr/HoTT/Categories/NaturalTransformation/Sum.v" "-q"
The timeout for /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig has been set to: 3
This file produces the following output when Coq'ed:
Error:
System error: "theories/Categories/NaturalTransformation/Sum.v.timing: No such file or directory"
The current state of the file does not have a recognizable error.
Traceback (most recent call last):
File "/github/workspace/coq-tools/find-bug.py", line 1470, in
env['error_reg_string'] = get_error_reg_string(output_file_name, **env)
File "/github/workspace/coq-tools/find-bug.py", line 284, in get_error_reg_string
error_reg_string = get_error_reg_string_of_output(output, **kwargs)
File "/github/workspace/coq-tools/find-bug.py", line 246, in get_error_reg_string_of_output
error_reg_string = raw_input('\nPlease enter a regular expression which matches on the output. Leave blank to re-coq the file.\n')
EOFError: EOF when reading a line
```
If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging `@JasonGross`).
If you believe there's a bug in the bug minimizer, please report it on [the bug minimizer issue tracker](https://github.com/JasonGross/coq-tools/issues).
_input('\nPlease enter a regular expression which matches on the output. Leave blank to re-coq the file.\n')
EOFError: EOF when reading a line
```
If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.
https://github.com/coq/coq/pull/17888#issuecomment-1653571095
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v (from ci-hott) (full log on GitHub Actions)
We are collecting data on the user experience of the Coq Bug Minimizer. If you haven't already filled the survey for this PR, please fill out our short survey!
Minimized Coq File (consider adding this file to the test-suite)
```coq (** * Coproduct of natural transformations *) Require Coq.Init.Ltac. Module Export AdmitTactic. Module Import LocalFalse. Inductive False : Prop := . End LocalFalse. Axiom proof_admitted : False. Import Coq.Init.Ltac. Tactic Notation "admit" := abstract case proof_admitted. End AdmitTactic. Require Import HoTT.Categories.Category.Sum HoTT.Categories.Functor.Sum HoTT.Categories.NaturalTransformation.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. Section sum. Definition sum C C' D F G F' G' (T : @NaturalTransformation C D F G) (T' : @NaturalTransformation C' D F' G') : NaturalTransformation (F + F') (G + G'). Proof. refine (Build_NaturalTransformation (F + F') (G + G') (fun x => match x with | Datatypes.inl c => T c | Datatypes.inr c' => T' c' end) _). abstract ( repeat (intros [] || intro); simpl; auto with natural_transformation ). Defined. End sum. Module Export NaturalTransformationSumNotations. Notation "T + U" := (sum T U) : natural_transformation_scope. End NaturalTransformationSumNotations. ```Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)
```coq ```Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 2.9MiB file on GitHub Actions Artifacts under
``` 0m00.71s | 367072 ko | Algebra/Groups/GroupCoeq.vo 0m00.71s | 346456 ko | Modalities/Descent.vo 0m00.70s | 351340 ko | Homotopy/Suspension.vo 0m00.61s | 395152 ko | Homotopy/WhiteheadsPrinciple.vo 0m00.57s | 343872 ko | Truncations/Connectedness.vo 0m00.55s | 328068 ko | Cubical/DPathCube.vo 0m00.55s | 361536 ko | ObjectClassifier.vo 0m00.54s | 348028 ko | Spaces/Finite/Fin.vo 0m00.52s | 344664 ko | Modalities/Localization.vo 0m00.51s | 373120 ko | Algebra/Groups/Presentation.vo 0m00.51s | 354828 ko | Homotopy/Join.vo 0m00.49s | 368648 ko | Algebra/AbGroups/AbelianGroup.vo 0m00.47s | 322332 ko | HIT/Flattening.vo 0m00.47s | 349668 ko | Projective.vo 0m00.46s | 342284 ko | HIT/epi.vo 0m00.45s | 346784 ko | Spaces/Nat/Arithmetic.vo 0m00.42s | 320264 ko | Cubical/PathSquare.vo 0m00.42s | 349772 ko | Modalities/Separated.vo 0m00.41s | 377128 ko | Algebra/Groups/ShortExactSequence.vo 0m00.39s | 347804 ko | Classes/theory/groups.vo 0m00.39s | 343896 ko | Constant.vo 0m00.39s | 347108 ko | Pointed/pTrunc.vo 0m00.36s | 351376 ko | Algebra/Groups/Image.vo 0m00.36s | 318392 ko | Categories/ExponentialLaws/Law4/Functors.vo 0m00.36s | 223692 ko | Spaces/Finite/FinInduction.vo 0m00.35s | 370624 ko | Algebra/Groups/Lagrange.vo 0m00.35s | 345236 ko | Spaces/Int/Spec.vo 0m00.35s | 344268 ko | Spaces/Nat/Core.vo 0m00.34s | 341948 ko | DProp.vo 0m00.32s | 368904 ko | Algebra/AbGroups/AbHom.vo 0m00.32s | 353256 ko | Truncations/SeparatedTrunc.vo 0m00.31s | 320576 ko | Categories/Functor/Pointwise/Properties.vo 0m00.31s | 330160 ko | Pointed/pMap.vo 0m00.31s | 342144 ko | Truncations/Core.vo 0m00.30s | 353180 ko | Homotopy/Freudenthal.vo 0m00.30s | 320124 ko | Spaces/Circle.vo 0m00.29s | 366956 ko | Algebra/AbGroups/Centralizer.vo 0m00.29s | 332120 ko | Colimits/MappingCylinder.vo 0m00.28s | 351124 ko | Algebra/Groups/Kernel.vo 0m00.27s | 299068 ko | Spaces/Int/LoopExp.vo 0m00.26s | 301936 ko | Algebra/AbGroups/Cyclic.vo 0m00.26s | 324124 ko | Categories/ProductLaws.vo 0m00.26s | 319920 ko | Spaces/Finite/FinNat.vo 0m00.24s | 287168 ko | Categories/Functor/Attributes.vo 0m00.23s | 262924 ko | Classes/interfaces/canonical_names.vo 0m00.23s | 271072 ko | Spaces/Pos/Spec.vo 0m00.22s | 317528 ko | Pointed/pHomotopy.vo 0m00.21s | 271056 ko | Algebra/AbGroups/AbProjective.vo 0m00.21s | 334992 ko | Categories/Functor/Composition/Functorial/Attributes.vo 0m00.21s | 276672 ko | Pointed/pSect.vo 0m00.20s | 254200 ko | Algebra/AbGroups/AbPullback.vo 0m00.20s | 211176 ko | Categories/NaturalTransformation/Isomorphisms.vo 0m00.20s | 221352 ko | Modalities/Accessible.vo 0m00.18s | 184024 ko | Pointed/pEquiv.vo 0m00.17s | 204528 ko | Algebra/AbGroups/Z.vo 0m00.16s | 289568 ko | Cubical/DPathSquare.vo 0m00.16s | 194812 ko | Spaces/No/Negation.vo 0m00.14s | 228068 ko | Algebra/AbGroups.vo 0m00.14s | 140164 ko | Modalities/Identity.vo 0m00.14s | 171760 ko | Pointed/pModality.vo 0m00.14s | 155392 ko | Spaces/Int/Core.vo 0m00.14s | 184836 ko | Spaces/Pos/Core.vo 0m00.13s | 148908 ko | Algebra/Congruence.vo 0m00.13s | 128172 ko | Categories/Functor/Notations.vo 0m00.13s | 167520 ko | Colimits/SpanPushout.vo 0m00.13s | 143216 ko | Spaces/Finite.vo 0m00.13s | 162300 ko | Spaces/Int/Equiv.vo 0m00.12s | 204824 ko | Algebra/Groups.vo 0m00.12s | 146836 ko | Categories/Category.vo 0m00.12s | 159984 ko | Homotopy/SuccessorStructure.vo 0m00.11s | 144020 ko | Categories/Functor.vo 0m00.11s | 126472 ko | Categories/Functor/Composition.vo 0m00.11s | 135104 ko | HIT/unique_choice.vo 0m00.11s | 134544 ko | Pointed.vo 0m00.11s | 115496 ko | Truncations.vo 0m00.10s | 92340 ko | Categories/Category/Sigma.vo 0m00.10s | 133404 ko | Categories/Functor/Composition/Functorial.vo 0m00.10s | 121280 ko | Categories/Functor/Composition/Functorial/Core.vo 0m00.10s | 124892 ko | Categories/Functor/Prod/Functorial.vo 0m00.10s | 83288 ko | Cubical.vo 0m00.10s | 106444 ko | HIT/SetCone.vo 0m00.10s | 124372 ko | Spaces/Nat.vo 0m00.10s | 144588 ko | Spaces/No.vo 0m00.09s | 141024 ko | Categories/Functor/Pointwise/Core.vo 0m00.09s | 113992 ko | HIT/iso.vo 0m00.08s | 70636 ko | Categories/Functor/Prod.vo 0m00.08s | 132620 ko | Categories/HomFunctor.vo 0m00.08s | 117980 ko | Spaces/Pos.vo 0m00.07s | 79892 ko | Categories/Category/Notations.vo 0m00.07s | 88536 ko | Categories/FunctorCategory/Core.vo 0m00.07s | 85740 ko | Categories/NaturalTransformation/Composition/Functorial.vo 0m00.07s | 81096 ko | Categories/NaturalTransformation/Sum.vo 0m00.07s | 122936 ko | Spaces/Int.vo 0m00.06s | 71620 ko | Categories/Functor/Pointwise.vo 0m00.06s | 65180 ko | Categories/NaturalTransformation/Composition.vo 0m00.06s | 132588 ko | Spaces/Finite/Tactics.vo 0m00.05s | 70900 ko | Categories/Category/Subcategory/Full.vo 0m00.04s | 69704 ko | Categories/Category/Subcategory.vo Makefile.ci:155: recipe for target 'ci-hott' failed make: *** [ci-hott] Error 2 /github/workspace/builds/coq /github/workspace ::endgroup:: ```build.log)Minimization Log
``` Coq version: 8.19+alpha compiled with OCaml 4.09.0 First, I will attempt to absolutize relevant [Require]s in /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v, and store the result in /github/workspace/cwd/bug_01.v... getting /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v getting /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.glob Now, I will attempt to coq the file, and find the error... Coqing the file (/github/workspace/cwd/bug_01.v)... Running command: "/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig" "-time-file" "theories/Categories/NaturalTransformation/Sum.v.timing" "-q" "-noinit" "-indices-matter" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/theories" "HoTT" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/contrib" "HoTT.Contrib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "HoTT.Categories.NaturalTransformation.Sum" "-R" "/tmp/tmpkuugzbjr" "" "/tmp/tmpkuugzbjr/HoTT/Categories/NaturalTransformation/Sum.v" "-q" The timeout for /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig has been set to: 3 This file produces the following output when Coq'ed: Error: System error: "theories/Categories/NaturalTransformation/Sum.v.timing: No such file or directory" The current state of the file does not have a recognizable error. Traceback (most recent call last): File "/github/workspace/coq-tools/find-bug.py", line 1470, inMinimized Coq File (consider adding this file to the test-suite)
```coq (** * Coproduct of natural transformations *) Require Coq.Init.Ltac. Module Export AdmitTactic. Module Import LocalFalse. Inductive False : Prop := . End LocalFalse. Axiom proof_admitted : False. Import Coq.Init.Ltac. Tactic Notation "admit" := abstract case proof_admitted. End AdmitTactic. Require Import HoTT.Categories.Category.Sum HoTT.Categories.Functor.Sum HoTT.Categories.NaturalTransformation.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. Section sum. Definition sum C C' D F G F' G' (T : @NaturalTransformation C D F G) (T' : @NaturalTransformation C' D F' G') : NaturalTransformation (F + F') (G + G'). Proof. refine (Build_NaturalTransformation (F + F') (G + G') (fun x => match x with | Datatypes.inl c => T c | Datatypes.inr c' => T' c' end) _). abstract ( repeat (intros [] || intro); simpl; auto with natural_transformation ). Defined. End sum. Module Export NaturalTransformationSumNotations. Notation "T + U" := (sum T U) : natural_transformation_scope. End NaturalTransformationSumNotations. ```Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)
```coq ```Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 2.9MiB file on GitHub Actions Artifacts under
``` 0m00.71s | 367072 ko | Algebra/Groups/GroupCoeq.vo 0m00.71s | 346456 ko | Modalities/Descent.vo 0m00.70s | 351340 ko | Homotopy/Suspension.vo 0m00.61s | 395152 ko | Homotopy/WhiteheadsPrinciple.vo 0m00.57s | 343872 ko | Truncations/Connectedness.vo 0m00.55s | 328068 ko | Cubical/DPathCube.vo 0m00.55s | 361536 ko | ObjectClassifier.vo 0m00.54s | 348028 ko | Spaces/Finite/Fin.vo 0m00.52s | 344664 ko | Modalities/Localization.vo 0m00.51s | 373120 ko | Algebra/Groups/Presentation.vo 0m00.51s | 354828 ko | Homotopy/Join.vo 0m00.49s | 368648 ko | Algebra/AbGroups/AbelianGroup.vo 0m00.47s | 322332 ko | HIT/Flattening.vo 0m00.47s | 349668 ko | Projective.vo 0m00.46s | 342284 ko | HIT/epi.vo 0m00.45s | 346784 ko | Spaces/Nat/Arithmetic.vo 0m00.42s | 320264 ko | Cubical/PathSquare.vo 0m00.42s | 349772 ko | Modalities/Separated.vo 0m00.41s | 377128 ko | Algebra/Groups/ShortExactSequence.vo 0m00.39s | 347804 ko | Classes/theory/groups.vo 0m00.39s | 343896 ko | Constant.vo 0m00.39s | 347108 ko | Pointed/pTrunc.vo 0m00.36s | 351376 ko | Algebra/Groups/Image.vo 0m00.36s | 318392 ko | Categories/ExponentialLaws/Law4/Functors.vo 0m00.36s | 223692 ko | Spaces/Finite/FinInduction.vo 0m00.35s | 370624 ko | Algebra/Groups/Lagrange.vo 0m00.35s | 345236 ko | Spaces/Int/Spec.vo 0m00.35s | 344268 ko | Spaces/Nat/Core.vo 0m00.34s | 341948 ko | DProp.vo 0m00.32s | 368904 ko | Algebra/AbGroups/AbHom.vo 0m00.32s | 353256 ko | Truncations/SeparatedTrunc.vo 0m00.31s | 320576 ko | Categories/Functor/Pointwise/Properties.vo 0m00.31s | 330160 ko | Pointed/pMap.vo 0m00.31s | 342144 ko | Truncations/Core.vo 0m00.30s | 353180 ko | Homotopy/Freudenthal.vo 0m00.30s | 320124 ko | Spaces/Circle.vo 0m00.29s | 366956 ko | Algebra/AbGroups/Centralizer.vo 0m00.29s | 332120 ko | Colimits/MappingCylinder.vo 0m00.28s | 351124 ko | Algebra/Groups/Kernel.vo 0m00.27s | 299068 ko | Spaces/Int/LoopExp.vo 0m00.26s | 301936 ko | Algebra/AbGroups/Cyclic.vo 0m00.26s | 324124 ko | Categories/ProductLaws.vo 0m00.26s | 319920 ko | Spaces/Finite/FinNat.vo 0m00.24s | 287168 ko | Categories/Functor/Attributes.vo 0m00.23s | 262924 ko | Classes/interfaces/canonical_names.vo 0m00.23s | 271072 ko | Spaces/Pos/Spec.vo 0m00.22s | 317528 ko | Pointed/pHomotopy.vo 0m00.21s | 271056 ko | Algebra/AbGroups/AbProjective.vo 0m00.21s | 334992 ko | Categories/Functor/Composition/Functorial/Attributes.vo 0m00.21s | 276672 ko | Pointed/pSect.vo 0m00.20s | 254200 ko | Algebra/AbGroups/AbPullback.vo 0m00.20s | 211176 ko | Categories/NaturalTransformation/Isomorphisms.vo 0m00.20s | 221352 ko | Modalities/Accessible.vo 0m00.18s | 184024 ko | Pointed/pEquiv.vo 0m00.17s | 204528 ko | Algebra/AbGroups/Z.vo 0m00.16s | 289568 ko | Cubical/DPathSquare.vo 0m00.16s | 194812 ko | Spaces/No/Negation.vo 0m00.14s | 228068 ko | Algebra/AbGroups.vo 0m00.14s | 140164 ko | Modalities/Identity.vo 0m00.14s | 171760 ko | Pointed/pModality.vo 0m00.14s | 155392 ko | Spaces/Int/Core.vo 0m00.14s | 184836 ko | Spaces/Pos/Core.vo 0m00.13s | 148908 ko | Algebra/Congruence.vo 0m00.13s | 128172 ko | Categories/Functor/Notations.vo 0m00.13s | 167520 ko | Colimits/SpanPushout.vo 0m00.13s | 143216 ko | Spaces/Finite.vo 0m00.13s | 162300 ko | Spaces/Int/Equiv.vo 0m00.12s | 204824 ko | Algebra/Groups.vo 0m00.12s | 146836 ko | Categories/Category.vo 0m00.12s | 159984 ko | Homotopy/SuccessorStructure.vo 0m00.11s | 144020 ko | Categories/Functor.vo 0m00.11s | 126472 ko | Categories/Functor/Composition.vo 0m00.11s | 135104 ko | HIT/unique_choice.vo 0m00.11s | 134544 ko | Pointed.vo 0m00.11s | 115496 ko | Truncations.vo 0m00.10s | 92340 ko | Categories/Category/Sigma.vo 0m00.10s | 133404 ko | Categories/Functor/Composition/Functorial.vo 0m00.10s | 121280 ko | Categories/Functor/Composition/Functorial/Core.vo 0m00.10s | 124892 ko | Categories/Functor/Prod/Functorial.vo 0m00.10s | 83288 ko | Cubical.vo 0m00.10s | 106444 ko | HIT/SetCone.vo 0m00.10s | 124372 ko | Spaces/Nat.vo 0m00.10s | 144588 ko | Spaces/No.vo 0m00.09s | 141024 ko | Categories/Functor/Pointwise/Core.vo 0m00.09s | 113992 ko | HIT/iso.vo 0m00.08s | 70636 ko | Categories/Functor/Prod.vo 0m00.08s | 132620 ko | Categories/HomFunctor.vo 0m00.08s | 117980 ko | Spaces/Pos.vo 0m00.07s | 79892 ko | Categories/Category/Notations.vo 0m00.07s | 88536 ko | Categories/FunctorCategory/Core.vo 0m00.07s | 85740 ko | Categories/NaturalTransformation/Composition/Functorial.vo 0m00.07s | 81096 ko | Categories/NaturalTransformation/Sum.vo 0m00.07s | 122936 ko | Spaces/Int.vo 0m00.06s | 71620 ko | Categories/Functor/Pointwise.vo 0m00.06s | 65180 ko | Categories/NaturalTransformation/Composition.vo 0m00.06s | 132588 ko | Spaces/Finite/Tactics.vo 0m00.05s | 70900 ko | Categories/Category/Subcategory/Full.vo 0m00.04s | 69704 ko | Categories/Category/Subcategory.vo Makefile.ci:155: recipe for target 'ci-hott' failed make: *** [ci-hott] Error 2 /github/workspace/builds/coq /github/workspace ::endgroup:: ```build.log)Minimization Log
``` Coq version: 8.19+alpha compiled with OCaml 4.09.0 First, I will attempt to absolutize relevant [Require]s in /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v, and store the result in /github/workspace/cwd/bug_01.v... getting /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.v getting /github/workspace/builds/coq/coq-failing/_build_ci/hott/theories/Categories/NaturalTransformation/Sum.glob Now, I will attempt to coq the file, and find the error... Coqing the file (/github/workspace/cwd/bug_01.v)... Running command: "/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig" "-time-file" "theories/Categories/NaturalTransformation/Sum.v.timing" "-q" "-noinit" "-indices-matter" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/theories" "HoTT" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/contrib" "HoTT.Contrib" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "HoTT.Categories.NaturalTransformation.Sum" "-R" "/tmp/tmpkuugzbjr" "" "/tmp/tmpkuugzbjr/HoTT/Categories/NaturalTransformation/Sum.v" "-q" The timeout for /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig has been set to: 3 This file produces the following output when Coq'ed: Error: System error: "theories/Categories/NaturalTransformation/Sum.v.timing: No such file or directory" The current state of the file does not have a recognizable error. Traceback (most recent call last): File "/github/workspace/coq-tools/find-bug.py", line 1470, inIf you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging
@JasonGross). If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.