Add porting bots to diagram #8
Conversation
|
|
README.md
Outdated
| @@ -9,6 +9,8 @@ graph LR; | |||
| mathlib3[(mathlib repo)] | |||
| port-comments[/"<a href='https://raw.githubusercontent.com/wiki/leanprover-community/mathlib4/port-comments.md'>port comments</a>"/] | |||
| run_port_status["<a href='https://github.com/leanprover-community/mathlib4/blob/master/scripts/run_port_status.sh'>run_port_status.sh</a><br />(On @jcommelin's server every 30 minutes)"] | |||
| port-grph-bot["On @semorrison's server every 4(?) hours"] | |||
| port-status-bot["On @semorrison's server every day"] | |||
There was a problem hiding this comment.
Are these scripts run from a repo @semorrison, or do they exist only on your hard drive?
There was a problem hiding this comment.
They exist on hard drives. I have a copy.
| port-grph-bot["A bot in the <a href='https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress'>port progress Zulip thread</a><br />On @semorrison's server every 4(?) hours"] | ||
| port-status-bot["A bot in the <a href='https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress'>port progress Zulip thread</a><br />On @semorrison's server every day"] |
There was a problem hiding this comment.
@jcommelin: I added a longer description to these; I don't really understand what the difference between them is. Can you elaborate?
There was a problem hiding this comment.
@eric-wieser One of them generates the graphs (hosted on Scott's server) that you can open by clicking the links in the tables with stats in the port progress thread.
The other bot is responsible for calculating those stats and posting the tables to the zulip thread.
No description provided.