Node.js 20 actions are deprecated. The following actions are running on Node.js 20 and may not work as expected: actions/checkout@v4, actions/upload-artifact@v4. Actions will be forced to run with Node.js 24 by default starting June 16th, 2026. Node.js 20 will be removed from the runner on September 16th, 2026. Please check if updated versions of these actions are available that support Node.js 24. To opt into Node.js 24 now, set the FORCE_JAVASCRIPT_ACTIONS_TO_NODE24=true environment variable on the runner or in your workflow file. Once Node.js 24 becomes the default, you can temporarily opt out by setting ACTIONS_ALLOW_USE_UNSECURE_NODE_VERSION=true. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/

Could not find a terminator for warning: File "./theories/Basics/PathGroupoids.v", line 502, characters 9-36: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default]

Could not find a terminator for warning: File "./theories/Basics/PathGroupoids.v", line 483, characters 15-24: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default]

Could not find a terminator for warning: File "./theories/Basics/PathGroupoids.v", line 467, characters 15-31: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default]

Could not find a terminator for warning: File "./theories/Basics/PathGroupoids.v", line 77, characters 14-19: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default]

Could not find a terminator for warning: File "./theories/Categories/Functor/Core.v", line 65, characters 0-45: Warning: Implicitly declaring Rewrite hint databases is deprecated. Please explicitly create "functor" [implicit-create-rewrite-hint-db,deprecated-since-9.2,deprecated,default] theories/Categories/Functor/Core.vo (real: 0.08, user: 0.04, sys: 0.04, mem: 99836 ko) theories/Categories/Category/Strict.vo (real: 0.09, user: 0.04, sys: 0.04, mem: 89948 ko)

Could not find a terminator for warning: File "./theories/Categories/Category/Core.v", line 116, characters 0-63: Warning: Implicitly declaring Rewrite hint databases is deprecated. Please explicitly create "morphism" [implicit-create-rewrite-hint-db,deprecated-since-9.2,deprecated,default] theories/Categories/Category/Core.vo (real: 0.11, user: 0.06, sys: 0.04, mem: 132144 ko) theories/Spaces/List/Core.vo (real: 0.11, user: 0.06, sys: 0.04, mem: 109528 ko) theories/Types/Option.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 88936 ko) test/bugs/github1794.vo (real: 0.09, user: 0.04, sys: 0.05, mem: 86544 ko) theories/Diagrams/Graph.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 87236 ko) theories/Tactics/Nameless.vo (real: 0.08, user: 0.03, sys: 0.05, mem: 89692 ko) theories/Axioms/Funext.vo (real: 0.08, user: 0.03, sys: 0.05, mem: 86348 ko) theories/Axioms/PropResizing.vo (real: 0.08, user: 0.03, sys: 0.04, mem: 86220 ko) theories/Basics/Classes.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 125104 ko) theories/Basics/Iff.vo (real: 0.09, user: 0.03, sys: 0.05, mem: 103292 ko) theories/Basics/Numerals/Hexadecimal.vo (real: 0.10, user: 0.05, sys: 0.04, mem: 121488 ko) theories/Basics/Predicate.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 133988 ko)

Could not find a terminator for warning: File "./theories/Categories/Category/Core.v", line 114, characters 0-63: Warning: Implicitly declaring Rewrite hint databases is deprecated. Please explicitly create "category" [implicit-create-rewrite-hint-db,deprecated-since-9.2,deprecated,default]

Could not find a terminator for warning: File "./theories/Basics/Overture.v", line 405, characters 7-20: Warning: Autogenerated "rew_r" scheme for paths. Use "Scheme Rewriting for paths" to explicitly generate it. This will become an error in the future. [missing-scheme,deprecated-since-9.2,deprecated,default] theories/Basics/Overture.vo (real: 0.17, user: 0.11, sys: 0.05, mem: 196656 ko) theories/Basics/Numerals/Decimal.vo (real: 0.12, user: 0.06, sys: 0.06, mem: 113096 ko) theories/Basics/Tactics.vo (real: 0.18, user: 0.12, sys: 0.06, mem: 189280 ko)

Could not find a terminator for warning: File "./theories/Basics/Overture.v", line 402, characters 7-20: Warning: Autogenerated "rew" scheme for paths. Use "Scheme Rewriting for paths" to explicitly generate it. This will become an error in the future. [missing-scheme,deprecated-since-9.2,deprecated,default]