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

handling "do not port default files" #7

Open
mo271 opened this issue Feb 1, 2023 · 4 comments · May be fixed by #9
Open

handling "do not port default files" #7

mo271 opened this issue Feb 1, 2023 · 4 comments · May be fixed by #9

Comments

@mo271
Copy link
Contributor

mo271 commented Feb 1, 2023

Right now the top of "Unported files" is essentially only ...default files with comment do not port default files, which is not super useful information.

What would be some ways to display more useful results there? Perhaps we could

  • removingdefault results by filtering
  • hide them by adding an extra column and sorting them towards the back?
@eric-wieser
Copy link
Member

Note that there is now a .comments.should_port: false field that we can use to filter these.

mo271 added a commit to mo271/mathlib-port-status that referenced this issue Feb 4, 2023
@mo271
hide if not should_port
a852e87 
Closes leanprover-community#7
@mo271 mo271 linked a pull request Feb 4, 2023 that will close this issue
Open
@mo271
Copy link
Contributor Author

mo271 commented Feb 10, 2023

fyi: I edited the port comments file on the porting wiki to include all default files...

@eric-wieser
Copy link
Member

I think the default files might all have been removed...

@mo271
Copy link
Contributor Author

mo271 commented Feb 10, 2023

Cool, then we can close this, close #9 and perhaps also remove everything about the default files form the port-comments in the wiki?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

hide if not should_port mo271/mathlib-port-status
2 participants
@eric-wieser @mo271