Skip to content

Factorizing universe treatment for Definition, Theorem and Fixpoint (part of CEP #89) - #19322

Merged
coqbot-app[bot] merged 5 commits into
rocq-prover:masterfrom
herbelin:master+declare-make-univs-late
Oct 11, 2024
Merged

Factorizing universe treatment for Definition, Theorem and Fixpoint (part of CEP #89)#19322
coqbot-app[bot] merged 5 commits into
rocq-prover:masterfrom
herbelin:master+declare-make-univs-late

Conversation

@herbelin

@herbelin herbelin commented Jul 4, 2024 •
edited
Loading

Copy link
Copy Markdown
Member

The PR introduces a sharing of universe treatment across Definition, Theorem and Co/Fixpoint.

In particular, this means that when it willl be possible to declare opaque immediate forms of Definition, Fixpoint or CoFixpoint, they will take automatically benefit of the ability to use private universes.

This is part of rocq-prover/rfcs#89. Integrating Derive in the process is done in #19578. Then, Program and Equations could also be considered.

Depends on:

@herbelin herbelin added kind: cleanup Code removal, deprecation, refactorings, etc. part: universes The universe system. needs: merge of dependency This PR depends on another PR being merged first. part: gallina The gallina commands labels Jul 4, 2024
@herbelin herbelin added this to the 8.21+rc1 milestone Jul 4, 2024
@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 Jul 4, 2024
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 17, 2024
@herbelin
herbelin force-pushed the master+declare-make-univs-late branch from 97b3f09 to 31924c2 Compare July 24, 2024 12:53
@coqbot-app coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 24, 2024
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jul 25, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 3, 2024
@herbelin
herbelin force-pushed the master+declare-make-univs-late branch from 31924c2 to a9c73c1 Compare August 3, 2024 08:35
@coqbot-app coqbot-app Bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. 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 Aug 3, 2024
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 27, 2024
@herbelin
herbelin force-pushed the master+declare-make-univs-late branch from a9c73c1 to ca4dad1 Compare September 17, 2024 19:01
@coqbot-app coqbot-app Bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Sep 17, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 19, 2024
@herbelin
herbelin force-pushed the master+declare-make-univs-late branch from ca4dad1 to 797494c Compare September 19, 2024 10:45
@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 Sep 19, 2024
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 19, 2024
@coqbot-app

coqbot-app Bot commented Sep 19, 2024

Copy link
Copy Markdown
Contributor

🔴 CI failure at commit 797494c without any failure in the test-suite

✔️ Corresponding job for the base commit 47de0c7 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-elpi_test
  • You can also pass me a specific list of targets to minimize as arguments.

@herbelin herbelin mentioned this pull request Sep 20, 2024
Merged
@herbelin herbelin added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. request: full CI Use this label when you want your next push to trigger a full CI. labels Sep 20, 2024
@herbelin
herbelin force-pushed the master+declare-make-univs-late branch from 797494c to 73677a0 Compare September 20, 2024 07:35
@coqbot-app coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 20, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 30, 2024
@herbelin
herbelin force-pushed the master+declare-make-univs-late branch from 4a0dcc9 to f1821bd Compare September 30, 2024 12:49
@coqbot-app coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Sep 30, 2024
@herbelin herbelin removed the needs: merge of dependency This PR depends on another PR being merged first. label Sep 30, 2024
@herbelin herbelin mentioned this pull request Oct 3, 2024
Open
SkySkimmer
SkySkimmer reviewed Oct 3, 2024
View reviewed changes
Comment thread vernac/declare.ml Outdated
Comment thread vernac/declare.ml Outdated
SkySkimmer
SkySkimmer reviewed Oct 3, 2024
View reviewed changes
Comment thread vernac/declare.ml
let uctx_body = UState.restrict uctx used_univs in
UState.check_mono_univ_decl uctx_body udecl in
initial_euctx, utyp, Default { body = (body, eff); opaque = Opaque ubody }
initial_euctx, utyp, used_univs, Default { body = (body, eff); opaque = Opaque ubody }

@SkySkimmer SkySkimmer Oct 3, 2024

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

The returned tuple is getting big, maybe define a record type for it?

@herbelin herbelin Oct 4, 2024

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

I think I'm fine as it is (especially since the tupling is immediately destructed by the caller) but I can use a tuple if your question leans on the side of an assertion.

@SkySkimmer
SkySkimmer requested a review from a team October 3, 2024 12:27
@SkySkimmer

SkySkimmer commented Oct 3, 2024

Copy link
Copy Markdown
Contributor

Incidentally fixes #19593.

Were you not adding a test? I don't see it.

@herbelin

herbelin commented Oct 3, 2024 •
edited
Loading

Copy link
Copy Markdown
Member Author

Incidentally fixes #19593.

Were you not adding a test? I don't see it.

Again a mistake: it is #19301 which fixes #19593. Fixed

@herbelin
herbelin force-pushed the master+declare-make-univs-late branch from f1821bd to d0e343f Compare October 4, 2024 10:40
@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 Oct 4, 2024
herbelin
herbelin commented Oct 4, 2024
View reviewed changes

@herbelin herbelin left a comment

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

Thanks for your review.

Comment thread vernac/declare.ml Outdated
Comment thread vernac/declare.ml Outdated
Comment thread vernac/declare.ml
let uctx_body = UState.restrict uctx used_univs in
UState.check_mono_univ_decl uctx_body udecl in
initial_euctx, utyp, Default { body = (body, eff); opaque = Opaque ubody }
initial_euctx, utyp, used_univs, Default { body = (body, eff); opaque = Opaque ubody }

@herbelin herbelin Oct 4, 2024

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

I think I'm fine as it is (especially since the tupling is immediately destructed by the caller) but I can use a tuple if your question leans on the side of an assertion.

SkySkimmer
SkySkimmer reviewed Oct 8, 2024
View reviewed changes
Comment thread vernac/declare.ml Outdated
SkySkimmer
SkySkimmer reviewed Oct 8, 2024
View reviewed changes
Comment thread vernac/declare.ml Outdated
@herbelin
herbelin force-pushed the master+declare-make-univs-late branch from 691b188 to b20eab4 Compare October 8, 2024 10:24
herbelin and others added 3 commits October 8, 2024 18:44
@herbelin @SkySkimmer
Add ability to accumulate used universes in make_univs_immediate.
b7e7a6a 
This will allow to deal with multiple (non-recursive) dependent
entries, as in Derive, where the n-th constant depends on the
universes of the p-th constants for p<n.

Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
@herbelin
Merging declare_definition and declare_mutual_definitions with declar…
1940ea6 
…e_possibly_mutual_definitions
@herbelin
Move declare_definition to export section.
603db3d
@herbelin
herbelin force-pushed the master+declare-make-univs-late branch from b20eab4 to 603db3d Compare October 8, 2024 16:44
@SkySkimmer SkySkimmer self-assigned this Oct 9, 2024
@SkySkimmer

SkySkimmer commented Oct 9, 2024

Copy link
Copy Markdown
Contributor

@coqbot run full ci

@coqbot-app coqbot-app Bot removed 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 Oct 9, 2024
@SkySkimmer

SkySkimmer commented Oct 11, 2024

Copy link
Copy Markdown
Contributor

@coqbot merge now

@coqbot-app
coqbot-app Bot merged commit cb7bd30 into rocq-prover:master Oct 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels

kind: cleanup Code removal, deprecation, refactorings, etc. part: gallina The gallina commands part: universes The universe system.

Projects

None yet

Milestone

9.0+rc1

Development

Successfully merging this pull request may close these issues.

2 participants

@herbelin @SkySkimmer