Zulip Chat Archive

Stream: general

Topic: last commit which compiles with no errors


view this post on Zulip Kevin Buzzard (Apr 21 2019 at 00:57):

I have a Lean 3.4.2 project with a mathlib dependency. The last time I edited leanpkg.html was about four days ago; after that point, mathlib doesn't move any more. Since then, the project has sometimes compiled and sometimes not compiled. How do I find the "last" time that the project compiled with that particular lean and mathlib?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:58):

you can ask git for where a branch lived at some point in the past, I think

view this post on Zulip Mario Carneiro (Apr 21 2019 at 00:58):

it's also not hard to bisect based on the commit times

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 01:00):

Is there some automation I can use? Assume my history is completely linear. I want to know the last time leanpkg build built my repo within some commit range.

view this post on Zulip Mario Carneiro (Apr 21 2019 at 01:01):

does your leanpkg.toml have commit SHAs in it?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 01:02):

this is actually why leanpkg didn't support branch references for a while... they are not reproducible - you can build the exact same project on two days and get a different result

view this post on Zulip Mario Carneiro (Apr 21 2019 at 01:03):

if this matters for your application you should use commit references rather than branch references

view this post on Zulip Simon Hudon (Apr 21 2019 at 01:03):

Can't you use both?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 01:04):

?

view this post on Zulip Simon Hudon (Apr 21 2019 at 01:05):

both a commit and a branch reference?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 01:07):

what does that mean?

view this post on Zulip Keeley Hoek (Apr 21 2019 at 01:08):

like this?

[dependencies]
mathlib = {git = "https://github.com/leanprover/mathlib", branch = "master", rev = "c1aff1b5c52b7996d69da2d2522cd696d811ed06"}

view this post on Zulip Simon Hudon (Apr 21 2019 at 01:09):

That would mean that, if you do leanpkg configure, it checks out the commit. If you do leanpkg update it gets the head of the branch, replace the sha commit with the new one and does the rest of the expected stuff

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 01:31):

So I could imagine Lean schemes tracking a perfectoid branch of mathlib, which Scott updates occasionally. This system makes that easy.

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 01:32):

We're basically forking mathlib and claiming that our version is better than yours because it contains some high-risk category theory code

view this post on Zulip Mario Carneiro (Apr 21 2019 at 01:33):

or you could PR some stuff...

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 01:40):

Right, I could add my crappy code to Scott's branch and he could just accept it and hang the quality control if he felt it was the most fun way to proceed

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 01:41):

simp, dsimp, simp, dsimp I ask you. Is all that nonsense fixed in the fork?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 01:43):

no one's touched simp... yet

view this post on Zulip Simon Hudon (Apr 21 2019 at 01:44):

What is broken about simp?

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 02:08):

Scott sometimes has to iterate simp and dsimp to make progress, in his perfectoid branch. Or at least he had to. Scott and Reid were talking about some subtle tweak to simp which might make things better, but it was above my head. The discussion was on Zulip though. IIRC it was left undecided about whether simp could do what they wanted, or not. Mario, can you find a link to the conversation?

view this post on Zulip Mario Carneiro (Apr 21 2019 at 02:09):

this? https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.23886.20presheaves/near/162782481

view this post on Zulip Kevin Buzzard (Apr 21 2019 at 02:12):

Dumb question, veering a little more back towards the topic: if I decide to change my leanpkg.toml so that it tracks some random branch of mathlib, then can I no longer use update-mathlib?


Last updated: May 08 2021 at 10:12 UTC