Zulip Chat Archive
Stream: general
Topic: last commit which compiles with no errors
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?
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
Mario Carneiro (Apr 21 2019 at 00:58):
it's also not hard to bisect based on the commit times
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.
Mario Carneiro (Apr 21 2019 at 01:01):
does your leanpkg.toml have commit SHAs in it?
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
Mario Carneiro (Apr 21 2019 at 01:03):
if this matters for your application you should use commit references rather than branch references
Simon Hudon (Apr 21 2019 at 01:03):
Can't you use both?
Mario Carneiro (Apr 21 2019 at 01:04):
?
Simon Hudon (Apr 21 2019 at 01:05):
both a commit and a branch reference?
Mario Carneiro (Apr 21 2019 at 01:07):
what does that mean?
Keeley Hoek (Apr 21 2019 at 01:08):
like this?
[dependencies]
mathlib = {git = "https://github.com/leanprover/mathlib", branch = "master", rev = "c1aff1b5c52b7996d69da2d2522cd696d811ed06"}
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
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.
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
Mario Carneiro (Apr 21 2019 at 01:33):
or you could PR some stuff...
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
Kevin Buzzard (Apr 21 2019 at 01:41):
simp, dsimp, simp, dsimp I ask you. Is all that nonsense fixed in the fork?
Mario Carneiro (Apr 21 2019 at 01:43):
no one's touched simp... yet
Simon Hudon (Apr 21 2019 at 01:44):
What is broken about simp?
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?
Mario Carneiro (Apr 21 2019 at 02:09):
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: Dec 20 2023 at 11:08 UTC