Skip to content

[nametab] Introduce type of imperative nametabs, unify API #16767

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
Closed
wants to merge 4 commits into from
Closed

[nametab] Introduce type of imperative nametabs, unify API #16767

wants to merge 4 commits into from

Conversation

ejgallego
Copy link
Member

This is both a cleanup and a step towards pushing the state upwards, and handling the nametabs functionally.

Related to #16746 and rocq-prover/rfcs#65

Overlays:

@ejgallego ejgallego requested review from a team as code owners November 2, 2022 19:23
@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 Nov 2, 2022
SkySkimmer
SkySkimmer reviewed Nov 2, 2022
View reviewed changes
SkySkimmer
SkySkimmer reviewed Nov 2, 2022
View reviewed changes
Copy link
Contributor

@SkySkimmer SkySkimmer left a comment

Choose a reason for hiding this comment

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

Why the new module type S instead of using nametree?

@SkySkimmer SkySkimmer removed request for a team November 2, 2022 19:30
@ejgallego ejgallego marked this pull request as draft November 2, 2022 19:36
@ejgallego
Copy link
Member Author

Why the new module type S instead of using nametree?

Because S is the imperative API, NAMETREE the functional one. Maybe we can get rid of S, but we need to see.

Sorry for not marking this a draft by the way.

@gares
Copy link
Member

gares commented Nov 2, 2022 •
edited
Loading

Would you mind separating commits doing just alpha renaming so that the pr is easy to review?

@coqbot-app coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Jan 25, 2023
@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 Feb 10, 2023
@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 Mar 3, 2023
@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 Mar 7, 2023
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Apr 6, 2023

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app bot added the stale This PR will be closed unless it is rebased. label Apr 6, 2023
@coqbot-app coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Apr 13, 2023
@SkySkimmer
Copy link
Contributor

I think comments from november got confused somehow into thinking this PR does more than it does. AFAICT it is mostly alpha renaming.

Is there a reason to keep the PR as draft?

@ejgallego
Copy link
Member Author

I think comments from november got confused somehow into thinking this PR does more than it does. AFAICT it is mostly alpha renaming.

Yes, the PR is mostly redoing the API into a module, plus a couple of very minor cleanups that should not be behavior-changing. But the idea of this PR is not to alter behavior, but allow subsequent PRs to profit from the new uniform API (so objects declaration can be functors over nametab modules).

Is there a reason to keep the PR as draft?

  • I'm not sure I have converged yet on the API
  • The overlays needs preparation

But indeed it seems to me the PR is close to be unmarked as draft.

@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 Apr 26, 2023
@ejgallego ejgallego mentioned this pull request Apr 26, 2023
Merged
@coqbot-app
Copy link
Contributor

coqbot-app bot commented May 26, 2023

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app bot added the stale This PR will be closed unless it is rebased. label May 26, 2023
ejgallego added 4 commits June 23, 2023 18:11
@ejgallego
[nametab] Introduce type of imperative nametabs, unify API
e1ebe61 
This is both a cleanup and a step towards pushing the state upwards,
and handling the nametabs functionally.

Related to rocq-prover#16746 and
rocq-prover/rfcs#65
@ejgallego
[nametab] Remove seldom used helper function
808a50d 
It should be expressed as a combinator, with better signalling than a
`Not_found`, but for now we preserve the semantics.
@ejgallego
[nametab] Small API Leaning
b56ce6a 
We resort to `Libnames` functions to manipulate their objects,
reducing the API a bit and getting more orthogonality.
@ejgallego
[nametab] Remove unused [full_name_cci]
4b7591b
@coqbot-app coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Jun 23, 2023
@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 10, 2023
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Aug 9, 2023

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app bot added the stale This PR will be closed unless it is rebased. label Aug 9, 2023
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 8, 2023

This PR was not rebased after 30 days despite the warning, it is now closed.

@coqbot-app coqbot-app bot closed this Sep 8, 2023
@ejgallego ejgallego mentioned this pull request Apr 11, 2025
Merged
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

Assignees
No one assigned
Labels
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. stale This PR will be closed unless it is rebased.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@ejgallego @gares @SkySkimmer