Zulip Chat Archive
Stream: condensed mathematics
Topic: blueprint ci
Johan Commelin (Feb 08 2022 at 07:41):
Can someone with knowledge of the blueprint backend and/or github CI please help me figure out why computers are upset with me: https://github.com/leanprover-community/liquid/runs/5105247888?check_suite_focus=true
Patrick Massot (Feb 08 2022 at 08:18):
I think this has nothing to do with the blueprint, it says the project doesn't build
Patrick Massot (Feb 08 2022 at 08:18):
lean --make src is failing
Johan Commelin (Feb 08 2022 at 08:20):
hmm, locally it seems fine
Johan Commelin (Feb 08 2022 at 08:21):
maybe there are conflicting names, caught by all.lean?
Johan Commelin (Feb 08 2022 at 08:21):
Wait, my point is that locally inv web completes without errors
Mauricio Collares (Feb 08 2022 at 12:55):
Patrick Massot said:
lean --make srcis failing
...with exit code 137, so probably lean ran out of memory. GitHub runner VMs have 7GB RAM.
Johan Commelin (Feb 08 2022 at 13:05):
@Mauricio Collares Ooh, interesting! That might indeed explain what's going on.
Johan Commelin (Feb 08 2022 at 13:06):
My desktop in my office also has 8GB and consistently crashes when I try to work on LTE.
Patrick Massot (Feb 08 2022 at 13:11):
Well spotted Mauricio!
Mauricio Collares (Feb 08 2022 at 13:12):
The blueprint/website GH Action seems to have a harder job than the project CI itself because it doesn't pre-download liquid oleans. Does it suffice to run scripts/get-cache.sh before inv decls?
Johan Commelin (Feb 08 2022 at 13:15):
Probably. There is of course a real chance that there are no oleans available yet. But that's something that we can solve by just waiting a couple of minutes
Mauricio Collares (Feb 08 2022 at 13:20):
Oh, good point! I think scripts/fetch_olean_cache.sh has some logic for fetching an older cache, which will probably be enough to fix the problem even if the most recent version has no oleans available.
Johan Commelin (Feb 08 2022 at 13:28):
If you want to PR a better CI script, that would be awesome!
Mauricio Collares (Feb 08 2022 at 13:50):
Johan Commelin said:
If you want to PR a better CI script, that would be awesome!
I submitted a PR to call the already-existing script as part of the blueprint CI. Hopefully that's enough to fix the problem.
Johan Commelin (Feb 08 2022 at 14:00):
Wonderful! Merged.
Johan Commelin (Feb 08 2022 at 14:00):
Let's see what CI does in the next run
Johan Commelin (Feb 08 2022 at 14:06):
It worked! And it's fast! https://leanprover-community.github.io/liquid/dep_graph.html
Patrick Massot (Feb 08 2022 at 14:10):
This graph is becoming a bit too large to be useful :sad:
Johan Commelin (Feb 08 2022 at 14:10):
Yeah, and I fear that it will get quite a bit larger still
Johan Commelin (Feb 08 2022 at 14:11):
I already noticed that I was sometimes merging nodes for the sake of graph clarity. But that doesn't always improve the clarity of the local text.
Patrick Massot (Feb 08 2022 at 14:11):
It means we'll need a way to get a graph per chapter or something like this.
Yaël Dillies (Feb 08 2022 at 14:46):
Some kind of zooming feature, maybe? Like, a graph whose nodes are themselves graphs.
Johan Commelin (Apr 19 2022 at 15:15):
I tried enabling CI again, but I still have an error
git.exc.GitCommandError: Cmd('git') failed due to: exit code(129)
cmdline: git diff --cached --abbrev=40 --full-index --raw
stderr: 'error: unknown option `cached'
Johan Commelin (Apr 19 2022 at 15:15):
See https://github.com/leanprover-community/liquid/runs/6079987783?check_suite_focus=true#step:8:1499
Johan Commelin (Apr 19 2022 at 15:15):
If someone knows how to debug this, that would be cool
Eric Rodriguez (Apr 19 2022 at 15:17):
didn't this happen in flt-regular?
Eric Rodriguez (Apr 19 2022 at 15:17):
I think it was fixed there
Riccardo Brasca (Apr 19 2022 at 15:18):
@Chris Birkbeck
Johan Commelin (Apr 19 2022 at 15:19):
That was some jinja error, I think. This new error is complaining about git.
Chris Birkbeck (Apr 19 2022 at 15:20):
Johan Commelin said:
That was some jinja error, I think. This new error is complaining about git.
Yeah I think this is different.
Johan Commelin (Apr 19 2022 at 15:32):
Locally I get
File "/usr/lib/python3.8/subprocess.py", line 516, in run
raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command '['lean', '--run', '/home/jmc/data/math/lean-liquid/src/list_decls.lean']' died with <Signals.SIGSEGV: 11>.
Mauricio Collares (Apr 19 2022 at 16:51):
This happened in flt-regular too
Mauricio Collares (Apr 19 2022 at 16:52):
Add the two lines that were added in https://github.com/leanprover-community/flt-regular/commit/1d52c0bb2573f2bd391d6525ff1c4e4ba9879799 (ignore the removed lines, I was trying something else before)
Mauricio Collares (Apr 19 2022 at 16:54):
I don't know which of the two added lines did the trick, to be honest (I tried it blindly, since I don't have a testing environment)
Johan Commelin (Apr 19 2022 at 17:34):
@Mauricio Collares Thanks! I've pushed that change. Let's hope it works. If you would like to have push access to the blueprint repo, I'm happy to give it to you.
Mauricio Collares (Apr 19 2022 at 17:51):
It didn't work :( Let me try something, and I'll either submit a PR or ask for access depending on the outcome.
Johan Commelin (Apr 19 2022 at 17:52):
Thanks for your help!
Mauricio Collares (Apr 19 2022 at 18:29):
PR submitted! I had failed to notice a "cd .." in the previous build step, but it should work now. Unfortunately Alpine hasn't updated to Git 2.35.3 yet (it supports adding globs to safe.directories, such as *), so there's no alternative to getting the directory name right
Johan Commelin (Apr 19 2022 at 19:10):
@Mauricio Collares Thanks! I've merged your PR.
Johan Commelin (Apr 19 2022 at 19:30):
Hooray! It worked.
Johan Commelin (Apr 19 2022 at 20:16):
Another green oval (due to Ashvni's contribution proving that the completion of locally_constant is continuous_map): https://leanprover-community.github.io/liquid/dep_graph_section_2.html
Last updated: Dec 20 2023 at 11:08 UTC