Canceling since a higher priority waiting request for 'CI @ Alizter:ps/branch/chore__move_tests_v_to_test__folder' exists

Canceling since a higher priority waiting request for 'CI @ Alizter:ps/branch/chore__move_tests_v_to_test__folder' exists

The operation was canceled.

Canceling since a higher priority waiting request for 'CI @ Alizter:ps/branch/chore__move_tests_v_to_test__folder' exists

The operation was canceled.

Canceling since a higher priority waiting request for 'CI @ Alizter:ps/branch/chore__move_tests_v_to_test__folder' exists

The operation was canceled.

Canceling since a higher priority waiting request for 'CI @ Alizter:ps/branch/chore__move_tests_v_to_test__folder' exists

The operation was canceled.

Canceling since a higher priority waiting request for 'CI @ Alizter:ps/branch/chore__move_tests_v_to_test__folder' exists

The operation was canceled.

Canceling since a higher priority waiting request for 'CI @ Alizter:ps/branch/chore__move_tests_v_to_test__folder' exists

The operation was canceled.

Canceling since a higher priority waiting request for 'CI @ Alizter:ps/branch/chore__move_tests_v_to_test__folder' exists

The operation was canceled.

Canceling since a higher priority waiting request for 'CI @ Alizter:ps/branch/chore__move_tests_v_to_test__folder' exists

The operation was canceled.

Could not find a terminator for warning: File "./theories/Basics/Equivalences.v", line 104, characters 2-6: Warning: adj is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default] theories/Basics/Equivalences.vo (real: 0.37, user: 0.25, sys: 0.12, mem: 339940 ko) theories/Types/Unit.vo (real: 0.14, user: 0.06, sys: 0.05, mem: 113544 ko) theories/Basics/Trunc.vo (real: 0.21, user: 0.14, sys: 0.05, mem: 177056 ko) theories/Types/Empty.vo (real: 0.11, user: 0.05, sys: 0.04, mem: 96944 ko) theories/Types/Forall.vo (real: 0.29, user: 0.17, sys: 0.11, mem: 282464 ko) theories/Types/Paths.vo (real: 0.47, user: 0.29, sys: 0.14, mem: 344952 ko) theories/Categories/Category/Pi.vo (real: 0.11, user: 0.06, sys: 0.05, mem: 111536 ko) theories/HIT/Interval.vo (real: 0.10, user: 0.07, sys: 0.02, mem: 100612 ko) theories/PropResizing/PropResizing.vo (real: 0.10, user: 0.04, sys: 0.05, mem: 96788 ko) theories/WildCat/Equiv.vo (real: 0.50, user: 0.34, sys: 0.14, mem: 345504 ko) theories/Basics/Decidable.vo (real: 0.16, user: 0.09, sys: 0.05, mem: 142172 ko) theories/WildCat/Universe.vo (real: 0.18, user: 0.09, sys: 0.08, mem: 202988 ko) theories/WildCat/Induced.vo (real: 0.23, user: 0.12, sys: 0.11, mem: 266692 ko) theories/WildCat/Square.vo (real: 0.45, user: 0.32, sys: 0.11, mem: 338748 ko) theories/WildCat/PointedCat.vo (real: 0.26, user: 0.15, sys: 0.09, mem: 296388 ko) theories/Basics.vo (real: 0.11, user: 0.04, sys: 0.05, mem: 100256 ko) theories/Types/Arrow.vo (real: 0.17, user: 0.09, sys: 0.08, mem: 180424 ko) theories/Types/Prod.vo (real: 0.44, user: 0.31, sys: 0.11, mem: 344928 ko) test/bugs/github1358.vo (real: 0.10, user: 0.05, sys: 0.04, mem: 100708 ko) test/bugs/github973.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 100708 ko) theories/WildCat/NatTrans.vo (real: 0.50, user: 0.36, sys: 0.13, mem: 345576 ko) theories/WildCat/Prod.vo (real: 0.43, user: 0.33, sys: 0.08, mem: 345640 ko) theories/Types/Sigma.vo (real: 0.58, user: 0.47, sys: 0.09, mem: 348520 ko) theories/WildCat/EquivGpd.vo (real: 0.35, user: 0.24, sys: 0.11, mem: 343408 ko) theories/WildCat/FunctorCat.vo (real: 0.52, user: 0.40, sys: 0.11, mem: 344248 ko) theories/NullHomotopy.vo (real: 0.14, user: 0.08, sys: 0.05, mem: 129748 ko) theories/WildCat/TwoOneCat.vo (real: 0.26, user: 0.16, sys: 0.09, mem: 312904 ko) theories/Categories/Category/Prod.vo (real: 0.13, user: 0.07, sys: 0.05, mem: 137356 ko) theories/Tactics.vo (real: 0.21, user: 0.12, sys: 0.07, mem: 199620 ko) theories/Categories/Functor/Prod/Core.vo (real: 0.16, user: 0.09, sys: 0.06, mem: 164724 ko) theories/Categories/Category/Sigma/Core.vo (real: 0.20, user: 0.11, sys: 0.07, mem: 201752 ko) theories/Limits/Equalizer.vo (real: 0.12, user: 0.08, sys: 0.04, mem: 121360 ko) theories/Types/Equiv.vo (real: 0.27, user: 0.17, sys: 0.08, mem: 265184 ko) theories/Types/WType.vo (real: 0.17, user: 0.11, sys: 0.04, mem: 169468 ko) theories/HSet.vo (real: 0.20, user: 0.12, sys: 0.07, mem: 182680 ko) theories/WildCat/Opposite.vo (real: 0.39, user: 0.25, sys: 0.12, mem: 344620 ko) theories/Categories/Category/Morphisms.vo (real: 0.78, user: 0.61, sys: 0.15, mem: 353720 ko) theories/Categories/NaturalTransformation/Prod.vo (real: 0.15, user: 0.08, sys: 0.06, mem: 143560 ko) theories/EquivGroupoids.vo (real: 0.19, user: 0.13, sys: 0.06, mem: 186064 ko) theories/Types/Bool.vo (real: 0.17, user: 0.11, sys: 0.06, mem: 165588 ko) theories/Categories/Category/Paths.vo (real: 1.26, user: 1.12, sys: 0.11, mem: 356876 ko) theories/Types/IWType.vo (real: 0.56, user: 0.42, sys: 0.13, mem: 348708 ko) theories/WildCat/Yoneda.vo (real: 0.48, user: 0.35, sys: 0.12, mem: 347272 ko) theories/Categories/Category/Objects.vo (real: 0.13, user: 0.08, sys: 0.04, mem: 126688 ko) theories/WildCat/Bifunctor.vo (real: 0.26, user: 0.15, sys: 0.10, mem: 286292 ko) theories/Categories/Category/Univalent.vo (real:

adj is declared opaque (Qed) but this is not fully respected inside

Could not find a terminator for warning: File "./theories/Colimits/Pushout.v", line 281, characters 2-6: Warning: esp1_beta_pglue is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

esp1_beta_pglue is declared opaque (Qed) but this is not fully

Could not find a terminator for warning: File "./theories/Colimits/Pushout.v", line 300, characters 2-6: Warning: esp2_beta_pglue is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default] theories/Colimits/Pushout.vo (real: 0.92, user: 0.77, sys: 0.14, mem: 366956 ko) theories/Limits/Pullback.vo (real: 0.96, user: 0.83, sys: 0.13, mem: 360628 ko) theories/Pointed/pMap.vo (real: 0.50, user: 0.29, sys: 0.11, mem: 359692 ko) theories/Colimits/SpanPushout.vo (real: 0.18, user: 0.09, sys: 0.07, mem: 176164 ko) theories/HIT/Flattening.vo (real: 0.49, user: 0.38, sys: 0.11, mem: 354192 ko) theories/Categories/Category/Sigma/Univalent.vo (real: 2.43, user: 2.31, sys: 0.10, mem: 361376 ko) theories/Categories/Category/Subcategory/Full.vo (real: 0.10, user: 0.05, sys: 0.04, mem: 94904 ko) theories/Categories/Category/Subcategory/Wide.vo (real: 0.11, user: 0.07, sys: 0.02, mem: 94292 ko) theories/Categories/FunctorCategory/Core.vo (real: 0.12, user: 0.06, sys: 0.05, mem: 111892 ko) theories/Cubical/PathCube.vo (real: 4.19, user: 3.93, sys: 0.15, mem: 424488 ko) theories/Categories/HomFunctor.vo (real: 0.15, user: 0.08, sys: 0.06, mem: 145560 ko) theories/Categories/Functor/Pointwise/Core.vo (real: 0.16, user: 0.11, sys: 0.04, mem: 155424 ko) theories/Categories/FunctorCategory/Morphisms.vo (real: 0.19, user: 0.11, sys: 0.06, mem: 180464 ko) theories/Categories/FunctorCategory/Dual.vo (real: 0.15, user: 0.07, sys: 0.08, mem: 147744 ko) theories/Categories/CategoryOfGroupoids.vo (real: 0.12, user: 0.06, sys: 0.05, mem: 99752 ko) theories/Categories/SetCategory/Functors.vo (real: 0.10, user: 0.04, sys: 0.05, mem: 93844 ko) theories/Categories/Pseudofunctor/Core.vo (real: 0.18, user: 0.12, sys: 0.06, mem: 181492 ko) theories/Categories/Profunctor/Identity.vo (real: 0.12, user: 0.04, sys: 0.06, mem: 106172 ko) theories/Categories/Cat/Morphisms.vo (real: 0.13, user: 0.08, sys: 0.04, mem: 124484 ko) theories/Categories/ExponentialLaws/Law0.vo (real: 0.19, user: 0.11, sys: 0.07, mem: 195828 ko) theories/Categories/ExponentialLaws/Law1/Functors.vo (real: 0.19, user: 0.11, sys: 0.07, mem: 193212 ko) theories/Categories/ExponentialLaws/Law2/Functors.vo (real: 0.15, user: 0.07, sys: 0.07, mem: 140896 ko) theories/Categories/Comma/Notations.vo (real: 0.11, user: 0.06, sys: 0.04, mem: 98724 ko) theories/Categories/Comma/Projection.vo (real: 0.15, user: 0.09, sys: 0.05, mem: 131576 ko) theories/Categories/Comma/Dual.vo (real: 0.35, user: 0.20, sys: 0.12, mem: 347884 ko) theories/Categories/Comma/InducedFunctors.vo (real: 0.32, user: 0.19, sys: 0.12, mem: 326036 ko) theories/Categories/UniversalProperties.vo (real: 0.33, user: 0.19, sys: 0.13, mem: 343220 ko) theories/Categories/Adjoint/Dual.vo (real: 0.11, user: 0.05, sys: 0.06, mem: 101708 ko) theories/Categories/Adjoint/Hom.vo (real: 0.14, user: 0.07, sys: 0.06, mem: 125348 ko) theories/Categories/Comma/Functorial.vo (real: 0.90, user: 0.76, sys: 0.13, mem: 356364 ko) theories/Categories/Adjoint/Paths.vo (real: 0.29, user: 0.16, sys: 0.11, mem: 309476 ko) theories/Categories/Adjoint/Identity.vo (real: 0.11, user: 0.06, sys: 0.05, mem: 95300 ko) theories/Categories/Adjoint/Composition/Core.vo (real: 0.37, user: 0.25, sys: 0.11, mem: 352812 ko) theories/Categories/Adjoint/Functorial/Parts.vo (real: 0.17, user: 0.10, sys: 0.07, mem: 167740 ko) theories/Categories/PseudonaturalTransformation/Core.vo (real: 0.22, user: 0.14, sys: 0.07, mem: 206292 ko) theories/Categories/LaxComma/CoreParts.vo (real: 0.37, user: 0.28, sys: 0.08, mem: 352228 ko) test/Metatheory/UnivalenceImpliesFunext.vo (real: 0.11, user: 0.07, sys: 0.04, mem: 104536 ko) theories/Categories/Comma/Utf8.vo (real: 0.11, user: 0.06, sys: 0.04, mem: 100928 ko) theories/Categories/Grothendieck/ToSet/Morphisms.vo (real: 0.48, user: 0.36, sys: 0.10, mem: 354656 ko) theories/Limits/Limit.vo (real: 0.23, user:

esp2_beta_pglue is declared opaque (Qed) but this is not fully

Could not find a terminator for warning: File "./theories/Categories/LaxComma/Core.v", line 178, characters 4-82: Warning: This inductive will be minimized to Set even though Universe Minimization ToSet is unset. This will change in a future version. [bad-set-minimization,deprecated-since-8.18,deprecated,default]

This inductive will be minimized to Set even though Universe

Could not find a terminator for warning: File "./theories/Categories/LaxComma/Core.v", line 213, characters 4-84: Warning: This inductive will be minimized to Set even though Universe Minimization ToSet is unset. This will change in a future version. [bad-set-minimization,deprecated-since-8.18,deprecated,default] theories/Categories/LaxComma/Core.vo (real: 0.31, user: 0.20, sys: 0.10, mem: 319848 ko) theories/Categories/Grothendieck/ToSet.vo (real: 0.14, user: 0.05, sys: 0.04, mem: 96952 ko) theories/Categories/Grothendieck/ToCat.vo (real: 0.16, user: 0.08, sys: 0.05, mem: 128368 ko) theories/Spaces/Torus/Torus.vo (real: 0.19, user: 0.11, sys: 0.07, mem: 176640 ko) theories/Categories/Category/Utf8.vo (real: 0.12, user: 0.06, sys: 0.05, mem: 110816 ko) theories/Colimits/Colimit_Prod.vo (real: 0.15, user: 0.08, sys: 0.05, mem: 117632 ko) theories/Colimits/Colimit_Pushout_Flattening.vo (real: 0.98, user: 0.84, sys: 0.12, mem: 394704 ko) theories/Homotopy/Smash.vo (real: 0.53, user: 0.35, sys: 0.15, mem: 366080 ko) theories/Categories/Adjoint/Pointwise.vo (real: 3.44, user: 3.14, sys: 0.17, mem: 361800 ko) theories/Factorization.vo (real: 0.71, user: 0.56, sys: 0.12, mem: 368208 ko) theories/Categories/Category.vo (real: 0.17, user: 0.08, sys: 0.08, mem: 157480 ko) theories/Categories/ProductLaws.vo (real: 0.30, user: 0.16, sys: 0.13, mem: 341620 ko) theories/Categories/NaturalTransformation.vo (real: 0.11, user: 0.06, sys: 0.04, mem: 103652 ko) theories/Categories/FunctorCategory.vo (real: 0.12, user: 0.06, sys: 0.04, mem: 106520 ko) theories/Categories/InitialTerminalCategory.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 100308 ko) theories/Modalities/ReflectiveSubuniverse.vo (real: 2.46, user: 2.27, sys: 0.13, mem: 392156 ko) theories/Categories/ExponentialLaws/Law3/Law.vo (real: 1.85, user: 1.68, sys: 0.13, mem: 359452 ko) theories/Categories/Adjoint/UniversalMorphisms.vo (real: 0.11, user: 0.08, sys: 0.03, mem: 102036 ko) theories/Categories/Comma/ProjectionFunctors.vo (real: 0.78, user: 0.66, sys: 0.11, mem: 356992 ko) theories/Categories/Adjoint/Composition.vo (real: 0.12, user: 0.06, sys: 0.05, mem: 104488 ko) theories/Categories/Adjoint/Functorial.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 99700 ko) theories/Categories/LaxComma/Notations.vo (real: 0.13, user: 0.07, sys: 0.05, mem: 119864 ko) theories/Categories/Grothendieck.vo (real: 0.12, user: 0.04, sys: 0.06, mem: 104136 ko) theories/Categories/DependentProduct.vo (real: 0.13, user: 0.08, sys: 0.04, mem: 103816 ko) theories/Categories/LaxComma/Utf8.vo (real: 0.13, user: 0.06, sys: 0.06, mem: 123380 ko) theories/Pointed/pModality.vo (real: 0.18, user: 0.10, sys: 0.08, mem: 179040 ko) theories/Categories/Functor/Composition/Functorial/Core.vo (real: 0.16, user: 0.10, sys: 0.06, mem: 139352 ko) theories/Categories/ExponentialLaws/Law3.vo (real: 0.10, user: 0.06, sys: 0.04, mem: 96452 ko) theories/Categories/Comma.vo (real: 0.13, user: 0.08, sys: 0.05, mem: 116488 ko) theories/Modalities/Modality.vo (real: 0.74, user: 0.58, sys: 0.14, mem: 374376 ko) theories/Categories/KanExtensions/Core.vo (real: 0.13, user: 0.08, sys: 0.05, mem: 112516 ko) theories/Categories/Adjoint/Notations.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 100332 ko) theories/Categories/LaxComma.vo (real: 0.13, user: 0.08, sys: 0.04, mem: 126308 ko) theories/Modalities/Notnot.vo (real: 0.19, user: 0.12, sys: 0.05, mem: 182744 ko) theories/Categories/Adjoint/Utf8.vo (real: 0.11, user: 0.07, sys: 0.04, mem: 99720 ko) theories/Modalities/Accessible.vo (real: 0.25, user: 0.17, sys: 0.08, mem: 243384 ko) theories/Truncations/Core.vo (real: 0.39, user: 0.23, sys: 0.15, mem: 369472 ko) theories/Categories/ExponentialLaws.vo (real: 0.11, user: 0.05, sys: 0.06, mem: 103764 ko) theories/Categories/KanExtensions/Functors.vo (real: 0.14, user: 0.08, sys: 0.05, mem: 123432 ko) theories/Categories/Adjoint.vo (real: 0.13, user: 0.06, sys: 0.06, mem: 119840 ko) theories/Categories/Limits/Core.vo (real: 0.17, user: 0.10, sys: 0.07, mem: 154020 ko) theories/HIT/surjective_factor.vo (real: 0.19, user: 0.10, sys: 0.07,

This inductive will be minimized to Set even though Universe

adj is declared opaque (Qed) but this is not fully respected inside

esp1_beta_pglue is declared opaque (Qed) but this is not fully

esp2_beta_pglue is declared opaque (Qed) but this is not fully

This inductive will be minimized to Set even though Universe

This inductive will be minimized to Set even though Universe

Unexpected input(s) 'name', 'authToken', 'extraPullNames', valid inputs are ['extra_nix_config', 'github_access_token', 'install_url', 'install_options', 'nix_path']

The following actions uses node12 which is deprecated and will be forced to run on node16: geekyeggo/delete-artifact@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/

Unable to delete artifact "alectryon-html"; the artifact was not found.

Unable to delete artifact "workspace-8.17"; the artifact was not found.

Unable to delete artifact "file-dep-graphs"; the artifact was not found.

Unable to delete artifact "timing-html"; the artifact was not found.

Unable to delete artifact "workspace-dev"; the artifact was not found.

Unable to delete artifact "coqdoc-html"; the artifact was not found.