Coq CI Targets? #1549
Comments
|
I've suggested dropping Java targets before. I am adamant that we should keep GarageDoor. We might consider dropping Curves, or splitting it out to a separate Coq CI job. Overall, this question would be much easier to answer if I was able to query "how much time does the following make invocation take" without rebuilding. |
|
The CI job that is timing out is the one that builds only .v files. There is a separate one for making sure the extracted OCaml code compiles which builds
You can get the timing data from the bottom of Here is the timing table from the most recent successful Coq CI run of fiat-crypto. Note that we're just 3 minutes under the 3h timeout there. The slowest files on Coq's CI
I don't think the Coq devs will be happy with this solution. The 3h timeout is set by the devs, and see, e.g., coq/coq#16968 (comment) |
|
I would like to keep this, because not many developments test Extraction. (And plausibly we should ask the Coq devs to speed up extraction?). We might be able to build the extraction files in parallel though.
Pierre Marie recently had to disable The other points sound good, can we make some relevant targets? |
|
I think we should stop pretending these targets make any sense and just have a |
|
Build time visualization: https://andres.systems/tmp/time.html Script: import sys
def parsetime(s):
try:
return float(s)
except:
pass
m, s = s.split('m')
if s.endswith('s'): s = s[:-1]
return float(m)*60+float(s)
def parsemem(s):
assert s.endswith(' ko')
return 1024 * float(s[:-3])
names = []
values = []
parents = []
started = False
for line in sys.stdin:
try:
time, mem, path = [s.strip() for s in line.split(' | ')]
if path.strip() in ['File Name', 'Total Time / Peak Mem']:
continue
time = parsetime(time.strip())
mem = parsemem(mem.strip())
print (time, mem, path)
except:
continue
names.append(path)
values.append(time)
parents.append(path.rsplit('/', 1)[0] if '/' in path else '')
while parents[-1] not in names:
path = parents[-1]
names.append(path)
values.append(0)
parents.append(path.rsplit('/', 1)[0] if '/' in path else '')
print (list(zip(names, parents)))
import plotly.graph_objects as go
fig = go.Figure(go.Treemap(ids=names, labels=names, parents=parents, values=values, branchvalues="remainder", textinfo="label+value+percent parent+percent entry+percent root"))
fig.update_layout(margin = dict(t=50, l=25, r=25, b=25))
fig.show()I think for the testing of Coq, it is a good idea to include a small slice of each major category. |
|
Do you think Fancy code is valuable enough as a fiat-crypto test even to justify maintaining and building it just for that purpose? |
We've been timing out a bunch on Coq's CI recently, and I imagine #368 makes things a bit worse (though not much worse). Perhaps we should offer some target that does not build everything for Coq's CI to use? Thoughts? (@andres-erbsen ?)
The text was updated successfully, but these errors were encountered: