## 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.

#### Johan Commelin (May 07 2019 at 04:57):

I guess you can also kill compiles that are taking a very long time (like Travis does)

oh.... I'm dumb.

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

Are the cache files just named after the commit hash?

I think so, yes

They are

#### Simon Hudon (May 07 2019 at 05:00):

My idea would be to just have travis push its build results

#### Simon Hudon (May 07 2019 at 05:00):

Travis does a lot of work already, reusing it can some you a bunch of trouble

#### Scott Morrison (May 07 2019 at 05:42):

That sounds great too. However, I didn't want to learn how to make travis push to my machine or S3. :-)

#### Simon Hudon (May 07 2019 at 05:45):

I can give you hand. But for now, it's time for bed

#### Simon Hudon (May 07 2019 at 14:55):

@Scott Morrison How do you access your S3 account?

#### Scott Morrison (May 07 2019 at 14:58):

Using the secret access key. I think at some point I sent you another one.

#### Scott Morrison (May 08 2019 at 03:15):

Okay, https://tqft.net/lean/mathlib/ seems to be working. It polls github once a minute, compiles any new commits, and posts olean caches.

#### Johan Commelin (May 08 2019 at 03:22):

@Scott Morrison Cool! Thanks a lot for this effort

#### Simon Hudon (May 08 2019 at 16:40):

Coming soon in cache-olean: a link to https://tqft.net/lean/mathlib/

#### Scott Morrison (May 21 2019 at 01:02):

@Simon Hudon I am having such trouble with git. What should I be doing to pull every branch??

#### Scott Morrison (May 21 2019 at 01:04):

Ahh... maybe worked it out.

#### Scott Morrison (May 21 2019 at 01:04):

Let me try one more time, after which I will send you my build script and some logs :-)

Last updated: May 15 2021 at 23:13 UTC