Statically separate the three kinds of δ-resolvers. - #22446
Merged
coqbot-app[bot] merged 4 commits intoSep 9, 2026
Merged
Conversation
ppedrot
added
kind: cleanup
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
The stdlib issue is a real problem not fixed by the pipeline of cleanups I have locally. I guess I have to try to fix this differently... |
Contributor
|
Do you have a minimized version? |
Member
Author
|
Does the minimizer work on the stdlib? @coqbot minimize |
Member
Author
|
@coqbot ci minimize |
Contributor
|
I have initiated minimization at commit a4bbe1e for the suggested targets ci-stdlib, ci-stdlib as requested. |
Contributor
|
Error: Could not minimize file in 5m 20s (from ci-stdlib) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 5.8MiB file on GitHub Actions Artifacts under
|
Contributor
|
Error: Could not minimize file in 9m 58s (from ci-stdlib) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 6.2MiB file on GitHub Actions Artifacts under
|
Member
Author
|
Let's retry: @coqbot ci minimize stdlib |
Contributor
|
I was unable to minimize any of the CI targets that you requested. |
Contributor
|
not sure what a retry can do but it's @coqbot ci minimize ci-stdlib |
Contributor
|
I am now running minimization at commit a4bbe1e on requested target ci-stdlib. I'll come back to you with the results once it's done. |
Contributor
|
Not sure if this is useful but here is one Gallina file that is accepted before and is now no longer accepted. There are a bunch of other bugs but apparently they are all related to the upper layers and if there are more changes pending there it might not make sense to dig into them. EDIT: The LLM sayskernel/mod_subst.ml:330-338, 629-636 | Equiv kequ -> Equiv (subst_kn_delta subst kequ)cannot preserve an InlineBody reached through the substitution. This violates the documented join law: |
Contributor
|
Error: Could not minimize file in 4m 32s (from ci-stdlib) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 5.8MiB file on GitHub Actions Artifacts under
|
Contributor
|
Error: Could not minimize file in 5m 7s (from ci-stdlib) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 5.8MiB file on GitHub Actions Artifacts under
|
Contributor
|
Error: Could not minimize file in 9m 0s (from ci-stdlib) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 6.2MiB file on GitHub Actions Artifacts under
|
Member
Author
|
Small repro but not self-contained: From Stdlib Require Import QArith_base.
From Stdlib Require Import Qminmax.
Goal (0 + 0 == 0)%Q.
Proof.
intros.
setoid_replace (0 + 0)%Q with 0%Q.
2: match goal with [ |- Q.OT.eq _ _ ] => idtac end.
Abort. |
Member
Author
|
Let's close for now, I'll first fix other issues before coming back to this one. |
Member
Author
|
Self-contained repro: |
ppedrot
added
the
request: full CI
coqbot-app
Bot
added
the
needs: rebase
ppedrot
force-pushed
the
module-static-delta-resolver-classification
branch
from
September 9, 2026 12:11
a4bbe1e to
dbe92ac
Compare
coqbot-app
Bot
removed
needs: rebase
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
module-static-delta-resolver-classification
branch
from
September 9, 2026 12:20
dbe92ac to
380ec17
Compare
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
I fixed the uncovered problem by handling substitution composition specifically, i.e. keeping the inlining payload in this case. The more I think about that the more I believe that the inlining payload shouldn't even be stored in the substitution resolver. |
…emods. Substituting the objects of a module defined by a functor application needs two things: the renaming that takes the names of the functor to the names of the new module, and the inlining that replaces the fields the parameter type declared inlinable by the body the argument gives them. The first one is the raison d'être of δ-resolvers, while the second one belongs to the substitution. Declaremods was getting both out of the resolver of the applied module, i.e. it relied on the inlined bodies having leaked from the functor application into a module body. This was breaking inlining invariants in the representation of δ-resolvers. We now recompute the inlining part separately and attach it where it should be after the fact. This should be semantics-preserving, as the inlining leak is still there.
Except for the broken upper layers, there were actually three distinct kinds of δ-resolvers. 1. Resolvers from module bodies without any inlining information, as it makes no sense there. 2. Resolvers from module types, which may carry inlining parameter information, i.e. an inlining level for some constants. 3. Resolvers from module substitutions, which may carry actual inlining payload as terms attached to some constant to replace them. The upper layers used to gladly break these invariants to carry both the aliasing and inlining information through the same channel, but this was fixed in the last commit. This commit annotates the type of δ-resolvers to statically separate the various kinds in the code. Fixes rocq-prover#22452: Anomaly with module-heavy file.
A δ-resolver records both the canonical name of constant, and, in a substitution, the inlining payload it should replace the constant with. It turns out that one cannot recover the canonical name transitively out of the payload, so there was cases where the name picked was not canonical. We fix this by keeping both datum in the δ-resolver. Fixes rocq-prover#22454: Anomaly with modules.
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
module-static-delta-resolver-classification
branch
from
September 9, 2026 15:04
380ec17 to
953c39d
Compare
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
CI failure spurious (@SkySkimmer replaced the overlay with another fix under the feet of the PR), this is ready to go. |
SkySkimmer
approved these changes
Sep 9, 2026
Contributor
|
@coqbot merge now |
Contributor
|
@SkySkimmer: Please take care of the following overlays:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Except for the broken upper layers, there were actually three distinct kinds of δ-resolvers.
The upper layers used to gladly break these invariants to carry both the aliasing and inlining information through the same channel, but this was fixed in the first commit.
The second commit annotates the type of δ-resolvers to statically separate the various kinds in the code.
The third commit fixes a surprising behaviour where both the aliasing and the inlining data matter for substitutions. (This indicates that the datastructure is not enforcing invariants statically enough in my opinion.)
Fixes #22452: Anomaly with module-heavy file.
Fixes #22454: Anomaly with modules.
Overlays: