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

Move DCPOs and directed families to new domain-theory namespace #1225

Closed
wants to merge 4 commits into from
Closed

Move DCPOs and directed families to new domain-theory namespace #1225

wants to merge 4 commits into from

Conversation

fredrik-bakke
Copy link
Collaborator

No description provided.

@fredrik-bakke fredrik-bakke changed the title Move DCPOs and directed families to new domain-theory chore: Move DCPOs and directed families to new domain-theory Nov 18, 2024
@fredrik-bakke
Copy link
Collaborator Author

Beware that it does not seem like the effort to preserve attributions worked for globular types, so I'm skeptical it will work here either.

@fredrik-bakke fredrik-bakke changed the title chore: Move DCPOs and directed families to new domain-theory chore: Move DCPOs and directed families to new domain-theory namespace Nov 18, 2024
@fredrik-bakke fredrik-bakke mentioned this pull request Nov 18, 2024
Merged
@EgbertRijke
Copy link
Collaborator

Hm... so it is worse than I thought. Even if a file is merely moved, GitHub doesn't track who edited it:(

If this doesn't help to preserve authorship of files, is it still worth it to merge this PR?

@fredrik-bakke
Copy link
Collaborator Author

fredrik-bakke commented Nov 18, 2024 •
edited
Loading

Perhaps the issue is with the chore: prefix of the PR? Let's try merging this one without the prefix, at least it doesn't hurt to try.

@fredrik-bakke fredrik-bakke changed the title chore: Move DCPOs and directed families to new domain-theory namespace Move DCPOs and directed families to new domain-theory namespace Nov 18, 2024
@VojtechStep
Copy link
Collaborator

The issue isn't with the prefix. That's our internal thing. Git straight up doesn't pick up history from the file's previous location

@VojtechStep
Copy link
Collaborator

Apparently git log has a --follow option, but I don't see it available for git shortlog. If we want to fix this behavior, then I'd rather discontinue the Git authorship tracking than try to fix its current state

@fredrik-bakke
Copy link
Collaborator Author

That's unfortunate; then it sounds like it's meaningless to merge this PR. It's still the same for me though, so if @EgbertRijke wants this merged that's totally fine with me.

@EgbertRijke
Copy link
Collaborator

If we both agree that this PR is useless now, because git doesn't track contributor information across moved files, then let's close it. Apologies for the extra work

@fredrik-bakke fredrik-bakke deleted the directed-poset branch November 19, 2024 17:55
@fredrik-bakke
Copy link
Collaborator Author

no problem

EgbertRijke pushed a commit that referenced this pull request Nov 20, 2024
@fredrik-bakke
Two fixed point theorems (#1227)
e392dc5 
Formalizations of the Knaster–Tarski fixed point theorem and Kleene's
fixed point theorem, in addition to the necessary infrastructure.

~Merge after #1225.~
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@EgbertRijke EgbertRijke Awaiting requested review from EgbertRijke

Assignees
No one assigned
Labels
order-theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@fredrik-bakke @EgbertRijke @VojtechStep