search

project-everest / everest-ci

CI scripts for project everest
3 stars 8 forks source link

Stats for individual queries using `--hint_info` output #88

Closed s-zanella closed 7 years ago

s-zanella commented 7 years ago

(Stemming from discussion in https://github.com/mitls/hacl-star/issues/13.)

It would be very useful for the dashboard to report statistics about individual queries, in addition to overall per-module verification times (https://github.com/project-everest/everest-ci/issues/56).

This requires passing --hint_info to F*, which generates much longer logs. If this is too much, we could restrict the more detailed stats to nightly builds.

msprotz commented 7 years ago

https://github.com/project-everest/everest-ci/blob/master/ci#L493 from this line, it seems like this is already happening for nightlies

s-zanella commented 7 years ago

Great, then no reason not to have detailed stats.

msprotz commented 7 years ago

However, it seems like OTHERFLAGS is not passed properly to sub-commands in nightlies...

msprotz commented 7 years ago

Scrap that, OTHERFLAGS is working, I just got confused.... closing.