Avoid tracking PDF result files in the main github draft repository

[jensmaurer]

From #3313 :

Separately, we should consider not tracking all the papers in the primary git repository; source checkouts of the draft are huge and growing rapidly due to this.

[jensmaurer]

@nemequ said:

The "normal" flow would be to just keep the LaTeX in the repo and attach the PDFs (and Markdown, HTML, etc.) to the releases, preferably automatically generated and deployed by Travis.

[jensmaurer]

Editorial meeting: The purpose of the git repository is for the convenience of the editors. The suggestions do not provide additional convenience. For copies of the resulting PDF draft documents, see the public committee mailings.

[tkoeppe]

Editorial meeting on Friday: We should keep this open, and consider actually purging the PDFs from the repository. This might require something like git filter-branch. To be investigated.

[tkoeppe]

Editorial meeting cnt'd: If if we do a filter-branch, i.e. we rewrite the entire history, we must (in the sense of "shall") keep a record of all the old commit hashes and their corresponding new hashes. This is because we make reference to commit hashes in various places, such as commit messages and github issues. (We should also incrementally update any affected commit messages as we go along.)

[tkoeppe]

A problem with rewriting history is that we have published commit hashes in N-numbered papers (as part of Edtior's Reports).

[tkoeppe]

Idea: clone the repository into a frozen, archival location, so that the commit hashes remain in some sense valid.

[jwakely]

Isn't a branch from current master enough to preserve the hashes?

[jensmaurer]

@jwakely: Yes, but then the total repo size won't shrink (because the PDFs are still present on that other branch).

git filter-branch --index-filter 'git rm --cached --ignore-unmatch papers/*.pdf' filtered
removes the PDFs on a branch "filtered". Seems to work; preserves all merge-commit (which is something we might not want).

[zygoloid]

I wonder if there's anything specific to github that we can do here to preserve the old hashes. Unlike with a stock git repository, git fetch from github does not fetch all history: in particular, it doesn't fetch pull requests. Perhaps we could preserve the history by tracking it as a pull request?