Zulip Chat Archive

Stream: general

Topic: 3.4.2 branch


view this post on Zulip Scott Morrison (May 05 2019 at 18:59):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (May 05 2019 at 19:42):

It's merged once a day

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (May 05 2019 at 20:22):

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

view this post on Zulip Scott Morrison (May 05 2019 at 20:22):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip Patrick Massot (May 05 2019 at 20:26):

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

view this post on Zulip Patrick Massot (May 05 2019 at 20:26):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Scott Morrison (May 05 2019 at 22:19):

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

view this post on Zulip Scott Morrison (May 05 2019 at 22:20):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 06 2019 at 20:03):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 06 2019 at 20:04):

crontab -e

view this post on Zulip Johan Commelin (May 06 2019 at 20:06):

*/10 * * * * command to execute

view this post on Zulip Simon Hudon (May 06 2019 at 20:14):

It should probably be integrated into cache-olean

view this post on Zulip Simon Hudon (May 06 2019 at 20:18):

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

view this post on Zulip Johan Commelin (May 06 2019 at 20:19):

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

view this post on Zulip Johan Commelin (May 06 2019 at 20:21):

Alternative catchy names: kangaroo, sandbox, scuba, hey_mate

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 06 2019 at 20:22):

bradwurst?

view this post on Zulip Simon Hudon (May 06 2019 at 20:22):

We could rename it to weizen_bier

view this post on Zulip Simon Hudon (May 06 2019 at 20:23):

Two good choices, I see

view this post on Zulip Simon Hudon (May 06 2019 at 20:23):

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

view this post on Zulip 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)

view this post on Zulip 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)...

view this post on Zulip Scott Morrison (May 07 2019 at 04:56):

Not sure what to do about that.

view this post on Zulip 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. :-)

view this post on Zulip Johan Commelin (May 07 2019 at 04:56):

That sounds like a good idea

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Scott Morrison (May 07 2019 at 04:57):

oh.... I'm dumb.

view this post on Zulip Scott Morrison (May 07 2019 at 04:57):

Are the cache files just named after the commit hash?

view this post on Zulip Johan Commelin (May 07 2019 at 04:58):

I think so, yes

view this post on Zulip Simon Hudon (May 07 2019 at 05:00):

They are

view this post on Zulip Simon Hudon (May 07 2019 at 05:00):

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

view this post on Zulip Simon Hudon (May 07 2019 at 05:00):

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

view this post on Zulip 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. :-)

view this post on Zulip Simon Hudon (May 07 2019 at 05:45):

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

view this post on Zulip Simon Hudon (May 07 2019 at 14:55):

@Scott Morrison How do you access your S3 account?

view this post on Zulip Scott Morrison (May 07 2019 at 14:58):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 08 2019 at 03:22):

@Scott Morrison Cool! Thanks a lot for this effort

view this post on Zulip Simon Hudon (May 08 2019 at 16:40):

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

view this post on Zulip 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??

view this post on Zulip Scott Morrison (May 21 2019 at 01:04):

Ahh... maybe worked it out.

view this post on Zulip 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