Skip to content
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

Deprecating change directory #17403

Merged
merged 3 commits into from Apr 19, 2024
Merged

Deprecating change directory #17403

merged 3 commits into from Apr 19, 2024

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented Mar 17, 2023 •
edited

In case there is a wish to eventually remove Cd (which does not make sense is a relocatable document).

Closes #16119.

Depends on #17392 (merged) and #16126 (merged).

  • Added changelog.

@herbelin herbelin added the part: vernac High level command interpretation. label Mar 17, 2023
@herbelin herbelin added this to the 8.18+rc1 milestone Mar 17, 2023
@herbelin herbelin requested review from a team as code owners March 17, 2023 19:08
@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 Mar 17, 2023
@jfehrle
Copy link
Member

jfehrle commented Mar 17, 2023

This has a lot more than just a deprecation, which is just the last commit. Do you expect the others will be committed before this one in other PRs?

@jfehrle
Copy link
Member

jfehrle commented Mar 17, 2023

The doc for Cd should mention the deprecation. Also needs a changelog.

Alizter
Alizter reviewed Mar 17, 2023
View reviewed changes
lib/system.ml Outdated Show resolved Hide resolved
@herbelin
Copy link
Member Author

Do you expect the others will be committed before this one in other PRs?

Yes, the other ones justify that we may eventually remove Cd.

The doc for Cd should mention the deprecation. Also needs a changelog.

Yes, it has to be done. I will do eventually, when the decisions taken about the other PRs are clearer.

@ppedrot ppedrot added the needs: merge of dependency This PR depends on another PR being merged first. label Mar 18, 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 31, 2023
@coqbot-app
Copy link
Contributor

coqbot-app bot commented May 1, 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 1, 2023
@coqbot-app
Copy link
Contributor

coqbot-app bot commented May 31, 2023

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

@coqbot-app coqbot-app bot closed this May 31, 2023
@coqbot-app coqbot-app bot removed this from the 8.18+rc1 milestone May 31, 2023
@herbelin herbelin reopened this Jul 6, 2023
@herbelin herbelin mentioned this pull request Jul 6, 2023
Merged
@herbelin herbelin force-pushed the master+deprecating-change-directory branch from 8fdb07a to 512562b Compare July 6, 2023 10:04
@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 Jul 6, 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 Dec 11, 2023
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented Jan 10, 2024

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 Jan 10, 2024
@herbelin herbelin force-pushed the master+deprecating-change-directory branch from 512562b to 6ddf78d Compare January 10, 2024 10:05
@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 Jan 10, 2024
@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 Mar 4, 2024
@herbelin herbelin mentioned this pull request Mar 4, 2024
Closed
@herbelin herbelin added the kind: deprecation Deprecation label Mar 28, 2024
herbelin added a commit to herbelin/github-coq that referenced this pull request Mar 29, 2024
@herbelin
Change log for coq#17403
58962be
@herbelin herbelin force-pushed the master+deprecating-change-directory branch from 188a60c to 58962be Compare March 29, 2024 09:11
@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 Mar 29, 2024
@herbelin
Copy link
Member Author

Changelog added

herbelin added a commit to herbelin/github-coq that referenced this pull request Apr 2, 2024
@herbelin @jfehrle
Change log for coq#17403
c4b0719 
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
@herbelin herbelin force-pushed the master+deprecating-change-directory branch from d7d5cc6 to c4b0719 Compare April 2, 2024 11:11
jfehrle
jfehrle reviewed Apr 4, 2024
View reviewed changes
vernac/synterp.ml Outdated Show resolved Hide resolved
herbelin added a commit to herbelin/github-coq that referenced this pull request Apr 5, 2024
@herbelin @jfehrle
Change log for coq#17403
a42a55b 
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
@herbelin herbelin force-pushed the master+deprecating-change-directory branch from c4b0719 to a42a55b Compare April 5, 2024 07:49
@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 Apr 17, 2024
SkySkimmer
SkySkimmer approved these changes Apr 17, 2024
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.

We may also want to change ppvernac to produce Pwd instead of Cd from VernacChdir None and maybe also warn on argument-less Cd (but not Pwd?)
But this doesn't need to be done in this PR.

@SkySkimmer SkySkimmer self-assigned this Apr 17, 2024
herbelin added a commit to herbelin/github-coq that referenced this pull request Apr 18, 2024
@herbelin @jfehrle
Change log for coq#17403
c490724 
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
@herbelin herbelin force-pushed the master+deprecating-change-directory branch from a42a55b to c490724 Compare April 18, 2024 12:04
@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 Apr 18, 2024
@herbelin
Copy link
Member Author

We may also want to change ppvernac to produce Pwd instead of Cd from VernacChdir None and maybe also warn on argument-less Cd (but not Pwd?)

I added a commit for it (but ok also to have this commit in an other PR).

herbelin and others added 2 commits April 18, 2024 15:20
@herbelin herbelin force-pushed the master+deprecating-change-directory branch from c490724 to 516fc03 Compare April 18, 2024 13:21
@SkySkimmer SkySkimmer 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 Apr 19, 2024
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 9082a98 into coq:master Apr 19, 2024
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jfehrle jfehrle jfehrle left review comments

@Alizter Alizter Alizter left review comments

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: deprecation Deprecation part: vernac High level command interpretation.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@herbelin @jfehrle @SkySkimmer @Alizter @ppedrot