You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Dune doesn't know about the .timing files generated by Coq with -time.
We do however have a makefile, so I could imagine a sandboxed rule that copies all the .v files and runs make timings on them to generate the timing files and move them to a special directory target. It would be a bit hacky, but cleaner than running make yourself.
I'm creating this issue as a reminder for trying this.
The text was updated successfully, but these errors were encountered:
Dune doesn't know about the .timing files generated by Coq with
-time
.We do however have a makefile, so I could imagine a sandboxed rule that copies all the .v files and runs
make timings
on them to generate the timing files and move them to a special directory target. It would be a bit hacky, but cleaner than running make yourself.I'm creating this issue as a reminder for trying this.
The text was updated successfully, but these errors were encountered: