Skip to content

Factorization of close_proof and close_future_proof in declare.ml #19320

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 6 commits into from
Sep 30, 2024
Merged

Factorization of close_proof and close_future_proof in declare.ml #19320

merged 6 commits into from
Sep 30, 2024

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented Jul 4, 2024

This PR starts moving the universe treatment in declare.ml close to the final declaration of constant, as in rocq-prover/rfcs#89.

At this stage, it introduces a new type distinguishing between future-based proofs and non-future-based proofs, then moves the closed_proof_output -> pproof_entry phase out of closed_proof and close_future_proof.

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
@herbelin herbelin requested a review from a team as a code owner July 4, 2024 07:02
@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
@herbelin herbelin mentioned this pull request Jul 4, 2024
Merged
@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 21, 2024
@herbelin herbelin force-pushed the master+factorization-close-proof-close-future-proof branch from ccb07f8 to d41458b Compare July 24, 2024 12:48
@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+factorization-close-proof-close-future-proof branch from d41458b to 066120b Compare August 3, 2024 06:40
@herbelin herbelin requested a review from a team as a code owner August 3, 2024 06:40
@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. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. 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 added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 28, 2024
@herbelin herbelin force-pushed the master+factorization-close-proof-close-future-proof branch from 066120b to 2243a9d Compare August 28, 2024 15:32
@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. labels Aug 28, 2024
@herbelin herbelin requested a review from a team as a code owner August 28, 2024 16:27
@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 Aug 28, 2024
@herbelin herbelin force-pushed the master+factorization-close-proof-close-future-proof branch from 29a6295 to 2243a9d Compare August 28, 2024 17:00
@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 5, 2024
@mattam82 mattam82 removed the needs: merge of dependency This PR depends on another PR being merged first. label Sep 9, 2024
mattam82
mattam82 approved these changes Sep 9, 2024
View reviewed changes
Copy link
Member

@mattam82 mattam82 left a comment

Choose a reason for hiding this comment

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

The factorization looks good to me, and this does not change the interface, so unless this breaks CI, I think we can merge. Can you explain why you did the change in vernacstate.ml though?

@herbelin herbelin force-pushed the master+factorization-close-proof-close-future-proof branch from 2243a9d to d780de7 Compare September 9, 2024 08:51
@herbelin herbelin force-pushed the master+factorization-close-proof-close-future-proof branch from d780de7 to 8842018 Compare September 17, 2024 17:43
@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 Sep 17, 2024
@SkySkimmer
Copy link
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 Sep 18, 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
@herbelin herbelin force-pushed the master+factorization-close-proof-close-future-proof branch from 8842018 to 41c02eb Compare September 19, 2024 18:21
@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 19, 2024
@herbelin
Copy link
Member Author

I rebased wrt #19545 but note that part of the job of the newly-profiled close_proof (namely the make_univ and declare_entry part) is now done by process_proof. I don't know if the latter is worth an explicit profiling.

@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 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 20, 2024
@herbelin herbelin force-pushed the master+factorization-close-proof-close-future-proof branch from 41c02eb to c50c721 Compare September 20, 2024 17:30
@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 Sep 20, 2024
@SkySkimmer SkySkimmer added the needs: fixing The proposed code change is broken. label Sep 23, 2024
@SkySkimmer
Copy link
Contributor

base+async failure looks real

@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 29, 2024
@herbelin
Moving declare_parameter next to its with-body sibling declare_entry.
309703c
@herbelin
Preparing moving MutualEntry.declare_possibly_mutual_definitions clos…
02de160 
…er to declare_entry.
@herbelin
Moving MutualEntry.declare_possibly_mutual_definitions closer to decl…
972a58d 
…are_entry.

This will allow to let declare_mutual_definition depend on it.

Note: The converse would be more difficult because
declare_possibly_mutual_definitions works from the beginning on Future
computations while declare_mutual_definition currently move to a
Future computation only after some time.
@herbelin
Declare.ml: more structure in prepare_proof.
bdeb71f
@herbelin
Adjust return_proof to prepare_proof
735f895
@herbelin
Factorization of close_proof and close_future_proof via some "process…
f2ac5c3 
…_proof".
@herbelin herbelin force-pushed the master+factorization-close-proof-close-future-proof branch from c50c721 to f2ac5c3 Compare September 29, 2024 10:02
@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 Sep 29, 2024
@herbelin
Copy link
Member Author

base+async failure looks real

Should be fixed (was not the correct type to associate to the initial uctx).

I realized in passing that base+async seems to be the only regression test about delayed "future" proofs (besides test-suite/stm), good to know.

@herbelin herbelin removed the needs: fixing The proposed code change is broken. label Sep 29, 2024
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit debc475 into rocq-prover:master Sep 30, 2024
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer left review comments

@mattam82 mattam82 mattam82 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.
3 participants
@herbelin @SkySkimmer @mattam82