Closed JasonGross closed 2 years ago
I blindly created https://github.com/mit-plv/fiat-crypto/pull/1428, does our CI show enough info to see how much that helps?
Yes, the CI should show a table of time and memory usage at the bottom of each step
This is better (thanks!), but I think we need to be under 3.5GB for Coq's CI
I created https://github.com/mit-plv/fiat-crypto/pull/1431 but I don't think it'll do it either. But wait, Coq CI got almost to the end of the file previously, to the large lemma that is now replaced with something hopefully very small?
I bumped coq-scripts to have the newly written script etc/coq-scripts/timing/exec-insert-mem-and-timings.sh
. Running etc/coq-scripts/timing/exec-insert-mem-and-timings.sh "coqc" -time -q '-w' '+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,unsupported-attributes' -w -notation-overridden,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths,-masking-absolute-name "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I /home/jgross/fiat-crypto/rewriter/src/Rewriter/Util/plugins -Q /home/jgross/fiat-crypto/coqprime/src/Coqprime Coqprime -Q /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil -Q /home/jgross/fiat-crypto/rupicola/src/Rupicola Rupicola -Q /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2 bedrock2 -Q /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples bedrock2Examples -Q /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler compiler -Q /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv riscv -Q /home/jgross/fiat-crypto/rewriter/src/Rewriter Rewriter -R src Crypto src/Bedrock/End2End/X25519/GarageDoor.v
gives
The heaviest individual lines, memoy-wise, are
42240 kb 4.905879629s: Chars 34517 - 34626 [(seprewrite_in_by~~~(fun~x~=>~...] 4.904 secs (4.901u,0.s)
43032 kb 2.331045788s: Chars 11906 - 12121 [(rewrite~word.unsigned_ltu,~?w...] 2.33 secs (2.309u,0.019s)
43560 kb 4.935696629s: Chars 34374 - 34483 [(seprewrite_in_by~~~(fun~x~=>~...] 4.934 secs (4.931u,0.s)
43824 kb 3.953769337s: Chars 20868 - 20946 [(eexists~_,_,_;~ssplit;~try~ec...] 3.952 secs (3.9u,0.049s)
44880 kb 4.940760959s: Chars 34231 - 34340 [(seprewrite_in_by~~~(fun~x~=>~...] 4.939 secs (4.905u,0.029s)
46200 kb 7.395484587s: Chars 44876 - 44880 [Qed.] 7.327 secs (7.325u,0.s)
48312 kb 9.864910226s: Chars 34067 - 34176 [(seprewrite_in_by~~~(fun~x~=>~...] 9.863 secs (9.826u,0.029s)
50424 kb 2.078699421s: Chars 16113 - 16251 [(destr~Z.eqb;~rewrite~?word.un...] 2.078 secs (2.067u,0.01s)
52800 kb 2.545997135s: Chars 13830 - 14046 [(rewrite~word.unsigned_ltu,~?w...] 2.545 secs (2.524u,0.019s)
53064 kb 6.149520842s: Chars 38911 - 39015 [(seprewrite_in_by~(fun~xs~ys~=...] 6.149 secs (6.134u,0.009s)
59400 kb 2.071407786s: Chars 15099 - 15237 [(destr~Z.eqb;~rewrite~?word.un...] 2.071 secs (2.059u,0.01s)
60828 kb .064876508s: Chars 66 - 99 [Require~Import~Coq.ZArith.ZArith.] 0.072 secs (0.051u,0.02s)
62300 kb .177013846s: Chars 211 - 244 [Require~Import~compiler.Pipeline.] 0.182 secs (0.161u,0.021s)
67056 kb 9.888231819s: Chars 38162 - 38266 [(seprewrite_in_by~(fun~xs~ys~=...] 9.887 secs (9.88u,0.s)
71544 kb .068535884s: Chars 100 - 138 [Require~Import~Crypto.Spec.Cur...] 0.068 secs (0.058u,0.009s)
85008 kb 9.671959878s: Chars 34660 - 34769 [(seprewrite_in_by~~~(fun~x~=>~...] 9.671 secs (9.633u,0.029s)
87384 kb 9.669767850s: Chars 34803 - 34912 [(seprewrite_in_by~~~(fun~x~=>~...] 9.668 secs (9.641u,0.019s)
101112 kb 38.786915628s: Chars 12819 - 12886 [Import~SetEvars~coqutil.Tactic...] 0. secs (0.u,0.s)
113256 kb 14.096241184s: Chars 37520 - 37624 [(seprewrite_in_by~(fun~xs~ys~=...] 14.095 secs (14.085u,0.s)
122232 kb 15.267297091s: Chars 37413 - 37517 [(seprewrite_in_by~(fun~xs~ys~=...] 15.266 secs (15.195u,0.059s)
144936 kb 14.457730528s: Chars 42268 - 42303 [all:~(try~SepAutoArray.listZnW...] 14.47 secs (14.409u,0.049s)
148896 kb 18.932911278s: Chars 37323 - 37410 [(seprewrite_in_by~(fun~xs~ys~=...] 18.932 secs (18.888u,0.029s)
188040 kb .206445801s: Chars 0 - 34 [Require~Import~Coq.Strings.Str...] 0.123 secs (0.081u,0.042s)
192716 kb .422204029s: Chars 401 - 460 [Require~Import~Crypto.Bedrock....] 0.421 secs (0.35u,0.07s)
241304 kb 67.127166250s: Chars 42304 - 42308 [Qed.] 67.135 secs (67.034u,0.069s)
412264 kb 1.635113554s: Chars 461 - 530 [Require~Import~Crypto.Bedrock....] 1.634 secs (1.514u,0.119s)
Timewise, the slowest lines are
4.350693476 s 0 kb: Chars 37734 - 37838 [(seprewrite_in_by~(fun~xs~ys~=...] 4.35 secs (4.347u,0.s)
4.905879629 s 42240 kb: Chars 34517 - 34626 [(seprewrite_in_by~~~(fun~x~=>~...] 4.904 secs (4.901u,0.s)
4.935696629 s 43560 kb: Chars 34374 - 34483 [(seprewrite_in_by~~~(fun~x~=>~...] 4.934 secs (4.931u,0.s)
4.940760959 s 44880 kb: Chars 34231 - 34340 [(seprewrite_in_by~~~(fun~x~=>~...] 4.939 secs (4.905u,0.029s)
5.244336293 s 16632 kb: Chars 43232 - 43403 [(repeat~eapply~recvEthernet_ok...] 5.243 secs (5.24u,0.s)
5.790857036 s 6072 kb: Chars 19052 - 19072 [(repeat~straightline).] 5.79 secs (5.787u,0.s)
6.149520842 s 53064 kb: Chars 38911 - 39015 [(seprewrite_in_by~(fun~xs~ys~=...] 6.149 secs (6.134u,0.009s)
6.606412111 s 0 kb: Chars 33925 - 34034 [(seprewrite_in_by~~~(fun~x~=>~...] 6.606 secs (6.601u,0.s)
6.653652514 s 0 kb: Chars 33847 - 33922 [(seprewrite_in_by~(@bytearray_...] 6.653 secs (6.648u,0.s)
7.395484587 s 46200 kb: Chars 44876 - 44880 [Qed.] 7.327 secs (7.325u,0.s)
8.736204370 s 7128 kb: Chars 44749 - 44760 [(vm_compute).] 8.76 secs (8.749u,0.009s)
8.968542306 s 18480 kb: Chars 46337 - 46580 [(eapply~lan9250_init_ok;~~~try...] 9.029 secs (9.013u,0.009s)
9.669767850 s 87384 kb: Chars 34803 - 34912 [(seprewrite_in_by~~~(fun~x~=>~...] 9.668 secs (9.641u,0.019s)
9.671959878 s 85008 kb: Chars 34660 - 34769 [(seprewrite_in_by~~~(fun~x~=>~...] 9.671 secs (9.633u,0.029s)
9.771183834 s 0 kb: Chars 37948 - 38052 [(seprewrite_in_by~(fun~xs~ys~=...] 9.77 secs (9.763u,0.s)
9.829626488 s 0 kb: Chars 38055 - 38159 [(seprewrite_in_by~(fun~xs~ys~=...] 9.829 secs (9.822u,0.s)
9.864910226 s 48312 kb: Chars 34067 - 34176 [(seprewrite_in_by~~~(fun~x~=>~...] 9.863 secs (9.826u,0.029s)
9.888231819 s 67056 kb: Chars 38162 - 38266 [(seprewrite_in_by~(fun~xs~ys~=...] 9.887 secs (9.88u,0.s)
11.407465406 s 8976 kb: Chars 13436 - 13555 [rewrite_strat~bottomup~(terms~...] 11.435 secs (11.415u,0.009s)
13.028313825 s 26400 kb: Chars 37627 - 37731 [(seprewrite_in_by~(fun~xs~ys~=...] 13.027 secs (13.008u,0.009s)
14.096241184 s 113256 kb: Chars 37520 - 37624 [(seprewrite_in_by~(fun~xs~ys~=...] 14.095 secs (14.085u,0.s)
14.457730528 s 144936 kb: Chars 42268 - 42303 [all:~(try~SepAutoArray.listZnW...] 14.47 secs (14.409u,0.049s)
15.267297091 s 122232 kb: Chars 37413 - 37517 [(seprewrite_in_by~(fun~xs~ys~=...] 15.266 secs (15.195u,0.059s)
18.932911278 s 148896 kb: Chars 37323 - 37410 [(seprewrite_in_by~(fun~xs~ys~=...] 18.932 secs (18.888u,0.029s)
38.786915628 s 101112 kb: Chars 12819 - 12886 [Import~SetEvars~coqutil.Tactic...] 0. secs (0.u,0.s)
67.127166250 s 241304 kb: Chars 42304 - 42308 [Qed.] 67.135 secs (67.034u,0.069s)
https://gitlab.com/coq/coq/-/jobs/3168928488 is a CI job off of https://github.com/coq/coq/pull/16648 . I restarted the pipeline before merging https://github.com/mit-plv/fiat-crypto/pull/1431 but as the particular job hasn't started I'd guess it'll pick up fiat-crypto master anyway. If it passes, I think we're "good" on this issue.
It passes at https://github.com/coq/coq/pull/16648/checks?check_run_id=8884687370
Thanks all!
GarageDoor uses too much RAM for Coq's CI. Either we should provide a target that excludes only GarageDoor and it's reverse dependencies, or we should perfomance-optimize GarageDoor.
https://github.com/coq/coq/runs/8838127340 https://github.com/coq/coq/pull/16638#issuecomment-1275905636
cc @andres-erbsen