Josh Chen (Jul 09 2020 at 10:50): Josh Chen (Jul 09 2020 at 10:50):Does anyone have any experience setting up CI for Isabelle with GitHub?
Manuel Eberl (Jul 09 2020 at 10:57):I vaguely seem to recall that Lars Hupel tried it once, but found that GitHub's free CI is not beefy enough for Isabelle.
Manuel Eberl (Jul 09 2020 at 10:57):Might depend on what you're trying to build exactly though.
Josh Chen (Jul 09 2020 at 11:00):Oh I just want to set up CI for the Isabelle/HoTT logic and theories. As a non-CS person by training it's new to me :D
Josh Chen (Jul 09 2020 at 11:02):I found https://github.com/isabelle-prover/admin, but I can't yet make sense of it.
Manuel Eberl (Jul 09 2020 at 11:04):I would recommend to just as Lars Hupel. He knows about this kind of stuff.
Simon Hudon (Jul 09 2020 at 12:46):@Manuel Eberl What do you mean by not beefy? Lean / Mathlib uses it + Bors and we managed to process a whole lot of PRs while making sure everything builds
Manuel Eberl (Jul 09 2020 at 15:23):I think he said something like there's a time and/or memory limit and it's just not enough to build reasonably-sized Isabelle sessions. Although I don't quite remember what he said; maybe the basic HOL session was still okay, but something like HOL-Analysis probably not. That one can take something like 60 CPU minutes. In any case, I might be mistaken altogether – I think this was a conversation we had some 3 years ago or so.
Manuel Eberl (Jul 09 2020 at 15:26):For Isabelle distribution + AFP CI on every push, we have a 64 core, 512 GB build server. And that even excludes some of the ‘very slow’ sessions; these are built on some TUM VMs every night. And then there's the macOS tests on some old Macbooks and the testboard for experimental changes on another pretty big (but older) build server.
Manuel Eberl (Jul 09 2020 at 15:27):Isabelle + AFP is /really/ big. But yeah Isabelle/HoTT is probably much more feasible.
Simon Wimmer (Jul 15 2020 at 13:57):So, Lars helped me do this once for my repository: https://github.com/wimmers/munta/blob/master/.travis.yml
Simon Wimmer (Jul 15 2020 at 13:58):The timeout is like 20 min on a single core, and that's just not enough time to finish building the HOL image, then some sessions from the AFP, and any session of this project on top.
Simon Wimmer (Jul 15 2020 at 13:59):For your project, I could however imagine if it still works because you do not need much underlying material, right?
Simon Wimmer (Jul 15 2020 at 14:00):Also, Travis is just the simplest way. You can also have the Github CI on your own hardware, and then it's a different story of course.
Manuel Eberl (Jul 15 2020 at 14:25):This actually downloads Isabelle anew every time the CI is run, right?
Manuel Eberl (Jul 15 2020 at 14:25):Or is there some kind of persistency?
Simon Hudon (Jul 15 2020 at 14:25):With Travis, we managed to get the timeout up to 50 min. 20 min is the maximum without response but you can pretend to be responsive every minute
Simon Hudon (Jul 15 2020 at 14:26):With Travis, you can cache the setup
Manuel Eberl (Jul 15 2020 at 14:31):I think the Isabelle process emits random text to stdout frequently enough.
Simon Hudon (Jul 15 2020 at 14:34):You should be able to go up to 50 min then. Actually, with staged builds, we managed to get about 4x 50 minutes
Simon Wimmer (Jul 15 2020 at 14:35):It does download it anew every time. So, yeah, it's not very good :D
Simon Wimmer (Jul 15 2020 at 14:36):But that sounds interesting, Simon. Maybe I should give it another shot.
Simon Hudon (Jul 15 2020 at 14:38):There's a lot that we managed to do with Travis but, disclaimer, we started feeling constrained in the last 6 months and moved to Github CI. There, we met new challenges as we had multiple PRs everyday that we needed to build and the build taking over an hour, it took a long time before entering the queue and getting a build machine. So we started batching the builds using a tool called bors
Simon Hudon (Jul 15 2020 at 14:39):I say we but I was mostly hands off in that process
Simon Hudon (Jul 15 2020 at 14:39):@Rob Lewis did a lot of heavy lifting, if I'm not mistaken
Simon Wimmer (Jul 15 2020 at 14:44):Interesting. The setup that Lars did for Isabelle is also quite involved. And builds are not triggered from Github but Mercurial repositories, of course ;)
Simon Hudon (Jul 15 2020 at 14:48):Shows what I know! I wasn't even aware that Mercurial was preferred in Isabelle projectts
Manuel Eberl (Jul 15 2020 at 14:49):Depends on what you mean by "Isabelle projects". There's the Isabelle distribution and the AFP, each in its own Mercurial repository. We thought about switching the AFP to Git when Bitbucket kicked out Mercurial, but ultimately decided against it.
Manuel Eberl (Jul 15 2020 at 14:50):For most of us, Mercurial over Git has historic reasons only. Makarius, however, is very adamant about Mercurial being the superior system and I don't think anyone cares enough about the whole Git vs. Mercurial discussion to go against him, since he's the one who makes things work behind the scenes at the end of the day.
Simon Hudon (Jul 15 2020 at 14:54):That's fair. I also don't know enough about the difference to pass judgement. Git is getting ubiquitous so I usually default to git.
Manuel Eberl (Jul 15 2020 at 14:55):Yeah me, too. I am equally incompetent at using both systems, so I don't really care.
Rob Lewis (Jul 15 2020 at 18:12):Gabriel Ebner did more heavy lifting than I did in moving mathlib from Travis to GH Actions. But from my perspective, Actions has been a lot more pleasant to deal with than Travis was. And using Bors would have been necessary either way; Actions wasn't slower than Travis, if anything I think it was a bit faster. Of course, this is all irrelevant to you guys if you're not using GitHub!
Lukas Stevens (Jul 15 2020 at 18:13):I just want to drop the idea to use Gitlab CI with a VM hosted at TUM. I found it really easy to set up and you won't have resource problems once properly set up.
Lukas Stevens (Jul 15 2020 at 18:16):Gitlab CI supports caching
Manuel Eberl (Jul 15 2020 at 18:50):Does the LRZ Gitlab support CI?
Manuel Eberl (Jul 15 2020 at 18:50):You could also add your stuff to the distribution, then you also get CI for free. ;)
Kevin Kappelmann (Jul 15 2020 at 18:52):I'd rather urge people to get stuff out of the distribution :D
Lukas Stevens (Jul 15 2020 at 18:52):You just have to install the gitlab CI runner on the VM and register it with the LRZ Gitlab
Lukas Stevens (Jul 15 2020 at 18:53):but any Gitlab instance would work. One can probably also mirror a Github repository on Gitlab and still run the CI on the Gitlab mirror if you want to have your project on Github
Lukas Stevens (Jul 15 2020 at 18:55):I'd rather urge people to get stuff out of the distribution :D
“The standard library is where modules go to die.” -- Kenneth Reitz
Manuel Eberl (Jul 15 2020 at 19:04):Well, something like an entirely new logic definitely fits into the distribution.
Manuel Eberl (Jul 15 2020 at 19:04):In the context of Isabelle, I'd argue that "outside the distribution/AFP is where developments go to die".
Lukas Stevens (Jul 15 2020 at 19:04):In the long term that is probably true.
Manuel Eberl (Jul 15 2020 at 19:05):How many Isabelle developments older than 5 years outside the distribution + AFP do you know that are still actively developed? How many of them still work with Isabelle2020?
Manuel Eberl (Jul 15 2020 at 19:05):auto2 only still lives because Kevin fixed it. If it had been inactive for a few years more than that, the effort to fix it could have been so big it might not have been worth it.
Manuel Eberl (Jul 15 2020 at 19:06):Some major developments like Avigad's Prime Number Theorem have already succumbed to bit rot indefinitely.
Manuel Eberl (Jul 15 2020 at 19:07):But yeah there's a lot of ancient crap in the distribution that really shouldn't be there.
Manuel Eberl (Jul 15 2020 at 19:08):Some people (including me) have suggested moving that into the AFP, but that was rejected on the basis that this stuff is actually not in a good enough state to go to the AFP (and never will be).
Manuel Eberl (Jul 15 2020 at 19:08):These things date back to times when there was no AFP.
Kevin Kappelmann (Jul 15 2020 at 19:10):Then at some point, I hope they also will not be good enough for the distro anymore ^^
Manuel Eberl (Jul 15 2020 at 19:11):I fear they might be of too much historic interest for that.
Manuel Eberl (Jul 15 2020 at 19:12):(aka "nostalgia")
Manuel Eberl (Jul 15 2020 at 19:12):Show some respect, some of these developments are probably older than you. :P
Max W. Haslbeck (Jul 18 2020 at 09:20):I played around with Github Actions this week. Now I let my heap images be built by github instead of straining my precious iMac :D
https://github.com/ammbauer/mirror-afp-2020/tree/9b95659af13b5fdbea1dc7a7a27ab90762865a1c/.github/workflows
https://github.com/ammbauer/mirror-afp-2020/actions/runs/172340567
Kevin Kappelmann (Jul 18 2020 at 11:43):Cool, that's nice! :) That's also what the lean people do for mathlib btw. When you checkout a version, it downloads the pre-built object files so you can start proving straight away. Would be nice to have this for the AFP too
Josh Chen (Jul 18 2020 at 19:04):NIce! I got something working too. Is the upload-artifact action in your workflow for caching the heap images?
Lukas Stevens (Jul 19 2020 at 09:32):I think it declares the heap image as a build artifact. You can download it here https://github.com/ammbauer/mirror-afp-2020/actions/runs/172340567
Lukas Stevens (Jul 19 2020 at 09:33):Under build artifacts and then click on skip_list_heaps
Rob Lewis (Jul 19 2020 at 11:41):Kevin Kappelmann said:
Cool, that's nice! :) That's also what the lean people do for mathlib btw. When you checkout a version, it downloads the pre-built object files so you can start proving straight away. Would be nice to have this for the AFP too
At least at the time we set it up, there was no API to map a git commit hash to the corresponding Actions artifact. So our CI script uploads the build somewhere else with a URL completely determined by the hash. It is (was?) an annoying limitation of the Actions setup, but IIRC changing it was on their to-do list.
Max W. Haslbeck (Jul 21 2020 at 08:33):Josh Chen said:
NIce! I got something working too. Is the
upload-artifactaction in your workflow for caching the heap images?
I used it to test if I can download and use the heap images. In this action I use the .isabelle/Isabelle2020/etc/settings file that I also have on my macs. I can then download the heap images, copy them to .isabelle/Isabelle2020/heaps/ and directly use them with isabelle jedit -l Skip_Lists.
pandaman (Sep 21 2020 at 04:48):Hi! I was looking for a CI solution for an Isabelle project and finally managed to create an Isabelle GitHub Action with heap cache enabled: https://github.com/pandaman64/isabelle-action
Example workflow: https://github.com/pandaman64/sabi/blob/master/.github/workflows/build.yml
This build.yml builds heap images of your sessions and caches dependencies on rebuild.
I hope this helps!
Last updated: Dec 21 2024 at 12:33 UTC