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

Could not find a terminator for warning: File "./theories/WildCat/Equiv.v", line 501, characters 0-35: Warning: The default value for Typeclasses Opaque and Typeclasses Transparent locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding typeclass transparency hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Typeclasses Transparent foo.". This is supported since Coq 8.15. [deprecated-typeclasses-transparency-without-locality,deprecated-since-8.15,deprecated,default] theories/WildCat/Equiv.vo (real: 0.57, user: 0.49, sys: 0.07, mem: 359576 ko) theories/Classes/implementations/family_prod.vo (real: 0.11, user: 0.05, sys: 0.06, mem: 122880 ko) test/Tactics/transport_paths.vo (real: 0.18, user: 0.11, sys: 0.07, mem: 237916 ko) theories/Types/Empty.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 112848 ko) theories/Basics/Decidable.vo (real: 0.15, user: 0.08, sys: 0.06, mem: 171028 ko) theories/Types/Forall.vo (real: 0.22, user: 0.15, sys: 0.07, mem: 294240 ko) theories/WildCat/Square.vo (real: 0.27, user: 0.19, sys: 0.07, mem: 347240 ko) theories/WildCat/Induced.vo (real: 0.13, user: 0.07, sys: 0.05, mem: 182528 ko) theories/Basics.vo (real: 0.08, user: 0.02, sys: 0.05, mem: 103500 ko) theories/WildCat/PointedCat.vo (real: 0.18, user: 0.11, sys: 0.07, mem: 288960 ko) theories/Types/Arrow.vo (real: 0.15, user: 0.09, sys: 0.06, mem: 218392 ko) theories/Types/Prod.vo (real: 0.32, user: 0.24, sys: 0.07, mem: 353732 ko) test/bugs/github1358.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 111244 ko) test/bugs/github973.vo (real: 0.10, user: 0.04, sys: 0.06, mem: 110840 ko) theories/WildCat/NatTrans.vo (real: 0.38, user: 0.30, sys: 0.08, mem: 355248 ko) theories/Tactics.vo (real: 0.15, user: 0.08, sys: 0.07, mem: 214324 ko) theories/Types/Sigma.vo (real: 0.45, user: 0.37, sys: 0.07, mem: 358960 ko) theories/WildCat/Prod.vo (real: 0.39, user: 0.32, sys: 0.07, mem: 355484 ko) theories/WildCat/FunctorCat.vo (real: 0.35, user: 0.24, sys: 0.11, mem: 352360 ko) theories/WildCat/EquivGpd.vo (real: 0.23, user: 0.15, sys: 0.08, mem: 342780 ko) theories/WildCat/Category.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 118784 ko) theories/Categories/Category/Morphisms.vo (real: 0.53, user: 0.45, sys: 0.07, mem: 358876 ko) theories/WildCat/Displayed.vo (real: 0.69, user: 0.61, sys: 0.08, mem: 366880 ko) theories/Categories/Category/Prod.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 147040 ko) theories/Categories/Category/Sigma/Core.vo (real: 0.15, user: 0.10, sys: 0.05, mem: 188724 ko) theories/Categories/Category/Univalent.vo (real: 0.12, user: 0.06, sys: 0.06, mem: 135664 ko) theories/Categories/GroupoidCategory/Core.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 138356 ko) theories/Categories/IndiscreteCategory.vo (real: 0.11, user: 0.06, sys: 0.04, mem: 160880 ko) theories/Categories/Functor/Prod/Core.vo (real: 0.12, user: 0.06, sys: 0.06, mem: 173792 ko) theories/Categories/Category/Paths.vo (real: 0.91, user: 0.83, sys: 0.07, mem: 364660 ko) theories/Categories/GroupoidCategory/Morphisms.vo (real: 0.60, user: 0.52, sys: 0.07, mem: 355340 ko) theories/Limits/Equalizer.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 134412 ko)

Could not find a terminator for warning: File "./theories/WildCat/Core.v", line 246, characters 0-29: Warning: The default value for Typeclasses Opaque and Typeclasses Transparent locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding typeclass transparency hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Typeclasses Transparent foo.". This is supported since Coq 8.15. [deprecated-typeclasses-transparency-without-locality,deprecated-since-8.15,deprecated,default] theories/WildCat/Core.vo (real: 0.37, user: 0.29, sys: 0.07, mem: 348568 ko) theories/Categories/Functor/Core.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 101952 ko) theories/Categories/Category/Strict.vo (real: 0.08, user: 0.03, sys: 0.05, mem: 95180 ko) theories/Categories/Functor/Composition/Core.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 107752 ko) theories/Categories/Category/Sum.vo (real: 0.17, user: 0.10, sys: 0.07, mem: 245796 ko) theories/Categories/Functor/Identity.vo (real: 0.07, user: 0.02, sys: 0.05, mem: 95588 ko) theories/Categories/NaturalTransformation/Core.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 140832 ko) theories/Utf8Minimal.vo (real: 0.08, user: 0.03, sys: 0.05, mem: 95996 ko) theories/Universes/UniverseLevel.vo (real: 0.11, user: 0.05, sys: 0.06, mem: 166208 ko) theories/Basics/Contractible.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 132012 ko) theories/Basics/Numeral.vo (real: 0.07, user: 0.03, sys: 0.04, mem: 97684 ko) theories/WildCat/Opposite.vo (real: 0.14, user: 0.08, sys: 0.06, mem: 202916 ko) theories/Tactics/EvalIn.vo (real: 0.10, user: 0.04, sys: 0.06, mem: 107188 ko) theories/Diagrams/CommutativeSquares.vo (real: 0.21, user: 0.14, sys: 0.06, mem: 299748 ko) theories/WildCat/Sigma.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 121192 ko) theories/WildCat/Forall.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 147824 ko) theories/WildCat/UnitCat.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 106680 ko) theories/WildCat/EmptyCat.vo (real: 0.09, user: 0.04, sys: 0.04, mem: 113080 ko) theories/Spaces/TwoSphere.vo (real: 0.31, user: 0.25, sys: 0.06, mem: 355076 ko) theories/WildCat/Sum.vo (real: 0.36, user: 0.28, sys: 0.07, mem: 349164 ko) theories/Categories/NaturalTransformation/Composition/Core.vo (real: 0.11, user: 0.06, sys: 0.05, mem: 165952 ko) theories/Categories/NaturalTransformation/Identity.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 120816 ko) theories/Basics/Nat.vo (real: 0.09, user: 0.04, sys: 0.04, mem: 112332 ko) theories/Tactics/BinderApply.vo (real: 0.09, user: 0.04, sys: 0.04, mem: 118044 ko) theories/Basics/Equivalences.vo (real: 0.27, user: 0.19, sys: 0.08, mem: 346472 ko) theories/Tactics/RewriteModuloAssociativity.vo (real: 0.14, user: 0.08, sys: 0.06, mem: 224260 ko) theories/Types/Unit.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 121364 ko) theories/Basics/Trunc.vo (real: 0.17, user: 0.11, sys: 0.05, mem: 208160 ko) theories/Types/Paths.vo (real: 0.36, user: 0.28, sys: 0.07, mem: 353088 ko) theories/Categories/Category/Pi.vo (real: 0.09, user: 0.04, sys: 0.04, mem: 121740 ko) theories/HIT/Interval.vo (real: 0.08, user: 0.03, sys: 0.05, mem: 113480 ko)

Could not enable unknown warning deprecated-tactic-notation-since-2025-03-11

"coq-core" has been renamed to "rocq-runtime".

Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 12, characters 0-90: Warning: "coq-core" has been renamed to "rocq-runtime". [coq-core-plugin,deprecated-since-9.0,deprecated,default] theories/Basics/Settings.vo (real: 0.10, user: 0.06, sys: 0.03, mem: 96660 ko) theories/Basics/Utf8.vo (real: 0.06, user: 0.02, sys: 0.03, mem: 66608 ko) theories/Basics/Overture.vo (real: 0.16, user: 0.10, sys: 0.06, mem: 185816 ko) theories/Basics/Numerals/Decimal.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 116388 ko) theories/Basics/Tactics.vo (real: 0.14, user: 0.09, sys: 0.04, mem: 190888 ko) theories/Categories/Category/Core.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 123160 ko) theories/Spaces/List/Core.vo (real: 0.09, user: 0.05, sys: 0.04, mem: 116528 ko) theories/Types/Option.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 100336 ko) test/bugs/github1794.vo (real: 0.07, user: 0.03, sys: 0.04, mem: 95816 ko) theories/Axioms/Funext.vo (real: 0.07, user: 0.03, sys: 0.04, mem: 95660 ko) theories/Axioms/PropResizing.vo (real: 0.08, user: 0.04, sys: 0.04, mem: 95688 ko) theories/Diagrams/Graph.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 97888 ko) theories/Tactics/Nameless.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 100080 ko) theories/Basics/Classes.vo (real: 0.08, user: 0.04, sys: 0.03, mem: 108436 ko) theories/Basics/Iff.vo (real: 0.08, user: 0.04, sys: 0.04, mem: 112652 ko) theories/Basics/Numerals/Hexadecimal.vo (real: 0.09, user: 0.04, sys: 0.04, mem: 122888 ko) theories/Categories/Functor/Core.vo (real: 0.08, user: 0.03, sys: 0.05, mem: 107852 ko) theories/Categories/Category/Strict.vo (real: 0.07, user: 0.03, sys: 0.03, mem: 99364 ko) theories/Categories/Category/Sum.vo (real: 0.16, user: 0.09, sys: 0.06, mem: 269984 ko) theories/Basics/PathGroupoids.vo (real: 0.65, user: 0.57, sys: 0.07, mem: 362964 ko) theories/Utf8Minimal.vo (real: 0.07, user: 0.04, sys: 0.03, mem: 99832 ko) theories/Universes/UniverseLevel.vo (real: 0.11, user: 0.06, sys: 0.05, mem: 166644 ko) theories/Basics/Contractible.vo (real: 0.10, user: 0.06, sys: 0.04, mem: 136396 ko) theories/WildCat/Core.vo (real: 0.41, user: 0.35, sys: 0.06, mem: 354508 ko) theories/Basics/Numeral.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 101476 ko) theories/Tactics/EvalIn.vo (real: 0.08, user: 0.04, sys: 0.04, mem: 109592 ko) theories/Categories/Functor/Composition/Core.vo (real: 0.08, user: 0.04, sys: 0.04, mem: 111656 ko) theories/Categories/Functor/Identity.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 99596 ko) theories/Categories/NaturalTransformation/Core.vo (real: 0.10, user: 0.05, sys: 0.04, mem: 146744 ko) theories/Diagrams/CommutativeSquares.vo (real: 0.19, user: 0.13, sys: 0.06, mem: 290164 ko) theories/WildCat/Opposite.vo (real: 0.14, user: 0.09, sys: 0.05, mem: 205252 ko) theories/WildCat/Sigma.vo (real: 0.09, user: 0.04, sys: 0.04, mem: 127464 ko) theories/WildCat/Forall.vo (real: 0.10, user: 0.06, sys: 0.04, mem: 149588 ko) theories/WildCat/EmptyCat.vo (real: 0.09, user: 0.05, sys: 0.03, mem: 116924 ko) theories/WildCat/UnitCat.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 110408 ko) theories/WildCat/Sum.vo (real: 0.31, user: 0.24, sys: 0.07, mem: 349440 ko) theories/Spaces/TwoSphere.vo (real: 0.25, user: 0.18, sys: 0.07, mem: 355264 ko) theories/Basics/Nat.vo (real: 0.10, user: 0.05, sys: 0.04, mem: 116320 ko) theories/Tactics/BinderApply.vo (real: 0.09, user: 0.04, sys: 0.04, mem: 120328 ko) theories/Basics/Equivalences.vo (real: 0.30, user: 0.23, sys: 0.06, mem: 352280 ko) theories/Categories/NaturalTransformation/Composition/Core.vo (real: 0.11, user: 0.06, sys: 0.05, mem: 171644 ko) theories/Categories/NaturalTransformation/Identity.vo (real: 0.10, user: 0.05, sys: 0.04, mem: 126836 ko) theories/Types/Unit.vo (real: 0.10, user: 0.05, sys: 0.04, mem: 121976 ko) theories/Tactics/RewriteModuloAssociativity.vo (real: 0.14, user: 0.09, sys: 0.05, mem: 228696 ko) theories/Basics/Trunc.vo (real: 0.17, user: 0.11, sys: 0.05, mem: 217112 ko) theories/WildCat/Equiv.vo (real: 0.60, user: 0.53, sys: 0.07, mem: 365536 ko) theories/Categories/Cate

Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 12, characters 0-90: Warning: Legacy loading plugin method has been removed from Rocq, and the `:` syntax is deprecated, and its first argument ignored; please remove "number_string_notation_plugin:" from your Declare ML [legacy-loading-removed,deprecated-since-9.0,deprecated,default]

"coq-core" has been renamed to "rocq-runtime".

Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 10, characters 0-54: Warning: "coq-core" has been renamed to "rocq-runtime". [coq-core-plugin,deprecated-since-9.0,deprecated,default]

Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 10, characters 0-54: Warning: Legacy loading plugin method has been removed from Rocq, and the `:` syntax is deprecated, and its first argument ignored; please remove "ltac_plugin:" from your Declare ML [legacy-loading-removed,deprecated-since-9.0,deprecated,default]

Could not enable unknown warning

"coq-core" has been renamed to "rocq-runtime".

"coq-core" has been renamed to "rocq-runtime".

Could not enable unknown warning

Could not enable unknown warning

The default value for Typeclasses Opaque and Typeclasses Transparent