LFTCM2020 bump

Stream: general

[Patrick Massot]

I just fixed lftcm2020 linear algebra examples to work now that vector_space and semimodule are gone. I also tried to fix some comments, but I think @Anne Baanen should take a closer look.

[Anne Baanen]

Thank you for the reminder, I am planning to look at it sometime next week, also the linear algebra library overview :+1:

[Patrick Massot]

And linear algebra in LFTCM2020 is broken again...

[Johan Commelin]

It's time for a new workshop, so that we can freeze that repo :sweat_smile:

[Patrick Massot]

And category theory too. At least it's taking forever (I mean it's even slower than usual). @Scott Morrison could you have a look? You need to leanproject up after pulling to see the issue.

[Patrick Massot]

It seems solutions/thursday/category_theory/exercise2.lean is taking forever.

[Patrick Massot]

This is probably a good opportunity to thank @Rob Lewis again for his upgrade GitHub action. It's a miracle that this lftcm repo is still up to date and this miracle wouldn't be possible without the bumping bot.

[Scott Morrison]

I've had a look at exercise2.lean. Something unpleasant has happened and it is indeed really slow. The first two definitions I can make compile by avoiding using tidy, but commute seems to have some slow unification problem that I'm both sad about, and not very excited about diagnosing...

[Anne Baanen]

I finished some small changes to the linear algebra examples. Thanks @Patrick Massot for doing the big fixes!

[Anne Baanen]

Also updated the linear algebra theory docs: leanprover-community.github.io#185

[Sebastien Gouezel]

It looks like the automatic upgrade is not firing any more on LFTCM2020: there is no build failure, but still it does not get updated to the latest mathlib version...

[Riccardo Brasca]

The same is happening with Flt-regular

[Eric Wieser]

Is the bot just dead again due to inactivity?

[Riccardo Brasca]

Hmm.. how can I check that?

[Eric Wieser]

Nevermind, the bot is being triggered just fine but there is a failure

[Eric Wieser]

https://github.com/leanprover-community/lftcm2020/actions/runs/3852065363/jobs/6563858951

[Eric Wieser]

I have no idea what's going wrong

[Eric Wieser]

I attempted a manual upgrade in leanprover-community/lftcm2020#148, but the manifold stuff is failing and I'm not really qualified to fix it. @Heather Macbeth, I seem to remember you refactored tangent bundles recently?

[Heather Macbeth]

Yes, with @Floris van Doorn. I am on holiday over Easter but can look in a week, or maybe Floris can get to it sooner.

[Eric Wieser]

No rush :)

[Floris van Doorn]

I fixed the manifold solutions file. Where is the script to generate the exercise file for that (or can you do that for me)?

[Eric Wieser]

./mk_exercises.py in the root

[Eric Wieser]

But I can run that for you

[Floris van Doorn]

:face_palm: I was looking for a scripts folder

[Sebastien Gouezel]

I've made a final fix. Now the branch builds without error on my computer, but it doesn't build on CI. Any idea?

[Alex J. Best]

Says it failed with code 137: "A 137 code is issued when a process is terminated externally because of its memory consumption" so maybe something is taking a lot of memory, can you reproduce that on your machine?

[Eric Wieser]

I think I've resolved this by discarding the docker container and doing everything within the regular worker

[Eric Wieser]

Yep, all working now; I took the liberty of merging

[Eric Wieser]

I've opened https://github.com/leanprover-community/lftcm2020/pull/150 with a bump to the port-complete tag

[Patrick Massot]

I'm afraid that so many things changed since 2020 that bumping this would be very difficult. Already many previous bumps created inconsistencies between text and code.

[Patrick Massot]

Really all this should be subsumed by MIL, but I heard the authors are pretty slow...

[Eric Wieser]

The bumps are actually all pretty easy, other than the mystery memory error that stumped us for 6 months.

[Eric Wieser]

I agree that the text inevitably diverges from the code; perhaps once everything is bumped the thing to do is add some explanation to the readme about how things may be out of sync with the 2020 version and it may not be the best resource