Zulip Chat Archive

Stream: general

Topic: 3.4.2 branch

Scott Morrison (May 05 2019 at 18:59):

The lean-3.4.2 ~~tag~~ branch seems to have fallen behind master.

Simon Hudon (May 05 2019 at 19:02):

We don't use the tag anymore. We use a branch. We've tried over and over to delete the tag but people have a copy on their hard drive and keep pushing it

Simon Hudon (May 05 2019 at 19:02):

The head of the lean-3.4.2 branch is 19 hours old so it's up to date

Scott Morrison (May 05 2019 at 19:38):

Oh, sorry, I meant branch rather than tag --- I guess I was expecting it to catch up to master more quickly. Is this just travis being slow? I'm curious that it has more work to do after the merge with master.

Simon Hudon (May 05 2019 at 19:42):

It's merged once a day

Scott Morrison (May 05 2019 at 20:17):

Would it be possible to merge more often? When PRs are coming in from other repositories, part of the workflow is:
1) PR gets merged to mathlib
2) Go back to other repository, leanpkg upgrade, update-mathlib, and fix up as required.
3) Realise update-mathlib doesn't work yet, and committing the result of leanpkg upgrade will upset collaborators
4) Decide to wait a day
5) Forget what you're doing

Patrick Massot (May 05 2019 at 20:18):

Scott, I'm a bit confused. I think the only reason why we don't update more often is because we wait for the hosting you promise you would be able to offer

Scott Morrison (May 05 2019 at 20:22):

Ah, okay. The hosting is definitely available. The question is how to get stuff to it.

Scott Morrison (May 05 2019 at 20:22):

I would prefer that travis doesn't have push access to my server.

Patrick Massot (May 05 2019 at 20:23):

This is what I meant by waiting for hosting. I meant waiting for you to figure out how you want to do it

Scott Morrison (May 05 2019 at 20:24):

So the options were:
1) I can pay for amazon s3 hosting (as I already do, and this won't be much additional), but someone would have to write a script that posted stuff to it.
2) I can run a cron job on my server that pulls something that travis produces.

Scott Morrison (May 05 2019 at 20:24):

My scripting-fu, particularly once it involves pushing files around, is not very good, and I don't understand the travis workflow completely.

Scott Morrison (May 05 2019 at 20:25):

So I wasn't thinking this was something on my todo list. I was waiting for someone to hand me a script to add to cron on my server. :-)

Patrick Massot (May 05 2019 at 20:26):

I wonder if we are not complicating things by insisting we should reuse Travis work

Patrick Massot (May 05 2019 at 20:26):

If you have computing power you could also compile on your end, and bypass Travis

Patrick Massot (May 05 2019 at 20:27):

Your machine can periodically ask GitHub for new commits (this is trivial compared to anything involving Travis)

Scott Morrison (May 05 2019 at 22:19):

OK: I propose that the following is the easiest to implement (but maybe wasteful of CPU time):

while (true)
  checkout all branches of leanprover-community/mathlib
  run `cache-olean --build-all`
  copy the contents of the `_cache` directory to a webserver

Scott Morrison (May 05 2019 at 22:19):

That should be easy to implement (probably in four lines!)

Scott Morrison (May 05 2019 at 22:20):

Is it actually useful? i.e. can someone work out what URL they need to fetch?

Patrick Massot (May 06 2019 at 06:47):

Yes I think this would be very useful. cache-olean produces file names directly from the git SHA so there would be no issue guessing urls

Patrick Massot (May 06 2019 at 06:49):

We need to check that cache-olean is smart enough to avoid recompiling a commit it already has. Otherwise you'll need to add another line to your loop

Johan Commelin (May 06 2019 at 13:48):

@Scott Morrison At which base URL would you want to serve the caches? I think we can easily update the dev-scripts to point to that URL

Scott Morrison (May 06 2019 at 13:50):

It will probably be https://tqft.net/lean/mathlib/_cache/. I will try to set this up today.

Scott Morrison (May 06 2019 at 20:03):

Getting there: https://tqft.net/lean/mathlib/

Scott Morrison (May 06 2019 at 20:04):

It's not in a crob job yet, but I have a script that seems to do everything required.

Johan Commelin (May 06 2019 at 20:04):

crontab -e

Johan Commelin (May 06 2019 at 20:06):

*/10 * * * * command to execute

Simon Hudon (May 06 2019 at 20:14):

It should probably be integrated into cache-olean

Simon Hudon (May 06 2019 at 20:18):

Do we want a more catchy name than "Scott's server"?

Johan Commelin (May 06 2019 at 20:19):

That's quite an accurate name, I would say...

Johan Commelin (May 06 2019 at 20:21):

Alternative catchy names: kangaroo, sandbox, scuba, hey_mate

Simon Hudon (May 06 2019 at 20:22):

I like kangaroo and hey_mate but what if Scott gets sick of taking care of it and it moves (say) to Germany?

Johan Commelin (May 06 2019 at 20:22):

bradwurst?

Simon Hudon (May 06 2019 at 20:22):

We could rename it to weizen_bier

Simon Hudon (May 06 2019 at 20:23):

Two good choices, I see

Simon Hudon (May 06 2019 at 20:23):

We could call it carmen_sandiego in anticipation of it moving around :P

Simon Hudon (May 06 2019 at 20:24):

(a hot dog is not a bradwurst but I'm just happy you didn't say saurkraut)

Scott Morrison (May 07 2019 at 04:55):

My compiler is running into trouble on some branches. e.g. the calculus branch has lots of errors, and it takes a while to run (even on subsequent runs of leanpkg build)...

Scott Morrison (May 07 2019 at 04:56):

Not sure what to do about that.

Scott Morrison (May 07 2019 at 04:56):

I guess I really need to set things up so that I only rebuild branches that have new commits, rather than just trying to build everything. :-)

Johan Commelin (May 07 2019 at 04:56):

That sounds like a good idea

Scott Morrison (May 07 2019 at 04:57):

@Simon Hudon, any ideas how to achieve that? I would like to go into each branch, and decide if there has been a new commit since the last time the olean cache file for that branch was built.