ci: run `add_port_comments.py` nightly (#17641)
Since this is modifying lean files and more could go wrong, this does not trigger bors automatically; but instead creates a PR for a human to double-check.
The PR description links to the mathlib4 PRs mentioned in the comments.
If a previous PR is open and not merged, this bot will update that PR. It remains to be seen how this will interact with bors.
