Skip to content

GenConstr can intern directly to constr - #22106

Merged
coqbot-app[bot] merged 2 commits into
rocq-prover:masterfrom
SkySkimmer:intern-gen
Aug 26, 2026
Merged

GenConstr can intern directly to constr#22106
coqbot-app[bot] merged 2 commits into
rocq-prover:masterfrom
SkySkimmer:intern-gen

Conversation

@SkySkimmer

@SkySkimmer SkySkimmer commented Jun 8, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 8, 2026
@SkySkimmer SkySkimmer mentioned this pull request Jun 8, 2026
Merged
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 8, 2026
@coqbot-app coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Jun 8, 2026
@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Jun 9, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 19, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 19, 2026
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Aug 19, 2026
@SkySkimmer
Fix phase separation for lib:qid syntax
85e0a39 
Using rocq-prover/rocq#22106

Implicit argument handling is not ideal and only works for maximal
implicits. To fix that I think we would need to parse applied `lib:qid args`
instead of parsing just the `lib:qid`, or change the upstream Rocq
code somehow.

TODO optcomp
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Aug 19, 2026
@SkySkimmer
Fix phase separation for lib:qid syntax
fcbea6f 
Using rocq-prover/rocq#22106

Implicit argument handling may be bugged

TODO optcomp
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Aug 19, 2026
@SkySkimmer
Fix phase separation for lib:qid syntax
d0a37df 
Using rocq-prover/rocq#22106

Implicit argument handling may be bugged

TODO optcomp
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Aug 20, 2026
@SkySkimmer
Fix phase separation for lib:qid syntax
299b278 
Using rocq-prover/rocq#22106

TODO optcomp
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 20, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 20, 2026
@SkySkimmer SkySkimmer removed the needs: overlay This is breaking external developments we track in CI. label Aug 20, 2026
SkySkimmer
SkySkimmer commented Aug 20, 2026
View reviewed changes
Comment thread interp/genintern.mli

type ('raw, 'glb) constr_intern_fun = ?loc:Loc.t -> glob_sign -> 'raw -> 'glb

type constr_intern_info = { passthrough_impls : bool }

@SkySkimmer SkySkimmer Aug 20, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

instead of telling the interner to look at the produced term we could return the data produced by find appl_head_data (as used in

rocq/interp/constrintern.ml

Line 2317 in 9fa45ea

let head, impls, subscopes = find_appl_head_data genv env lvar c in
) directly
That would allow genargs to have implicits even when interning to GGenarg
not sure if worth doing

@SkySkimmer
SkySkimmer marked this pull request as ready for review August 20, 2026 14:27
@SkySkimmer
SkySkimmer requested a review from a team as a code owner August 20, 2026 14:27
@SkySkimmer

SkySkimmer commented Aug 20, 2026

Copy link
Copy Markdown
Contributor Author

This version seems to work. We need the ability to control whether implicits of the produced term are used to support both lib:id (uses implicits) and lib:@id (does not use implicits).

@ppedrot ppedrot self-assigned this Aug 24, 2026
@ppedrot ppedrot added the kind: internal API, ML documentation... label Aug 24, 2026
@ppedrot ppedrot added this to the 9.4+rc1 milestone Aug 24, 2026
@ppedrot

ppedrot commented Aug 24, 2026

Copy link
Copy Markdown
Member

@SkySkimmer please ping me when you have time to write the optcomp layer for elpi.

@SkySkimmer

SkySkimmer commented Aug 24, 2026

Copy link
Copy Markdown
Contributor Author

In principle this PR can be merged before the elpi side is ready (it modifies the generic_intern APIs but elpi doesn't use those, the elpi side just uses the new APIs). The elpi side is done as a overlay for testing that the new API is sufficient.

@ppedrot
Remove the overlay.
9623c35 
It is not needed and was just there to prototype the API.
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 26, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 26, 2026
@ppedrot

ppedrot commented Aug 26, 2026

Copy link
Copy Markdown
Member

I pushed a tiny commit that removed the elpi overlay to double-check everything is fine. If the CI goes through I'll merge right after.

@ppedrot

ppedrot commented Aug 26, 2026

Copy link
Copy Markdown
Member

@coqbot merge now

@coqbot-app
coqbot-app Bot merged commit 58232a9 into rocq-prover:master Aug 26, 2026
9 checks passed
@SkySkimmer
SkySkimmer deleted the intern-gen branch September 7, 2026 11:32
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Sep 7, 2026
@SkySkimmer
Fix phase separation for lib:qid syntax
53f8bb3 
Using rocq-prover/rocq#22106
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Sep 7, 2026
@SkySkimmer
Fix phase separation for lib:qid syntax
290b6eb 
Using rocq-prover/rocq#22106
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Sep 7, 2026
@SkySkimmer
Fix phase separation for lib:qid syntax
de0f1e4 
Using rocq-prover/rocq#22106
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request Sep 7, 2026
@SkySkimmer
Fix phase separation for lib:qid syntax
af5a89f 
Using rocq-prover/rocq#22106
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels

kind: internal API, ML documentation...

Projects

None yet

Milestone

9.4+rc1

Development

Successfully merging this pull request may close these issues.

2 participants

@SkySkimmer @ppedrot