Timings for AllLogits.v

  1. /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-neural-net-interp-computed.dev/./theories/MaxOfTwoNumbers/Computed/AllLogits.v.timing
  2. /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-neural-net-interp-computed.dev/./theories/MaxOfTwoNumbers/Computed/AllLogits.v.timing
From NeuralNetInterp.MaxOfTwoNumbers Require Import Model.
From NeuralNetInterp.Torch Require Import Tensor.
From NeuralNetInterp.Util Require Import Pointed ValueExtraction.
Set NativeCompute Timing.
(*Set NativeCompute Profiling.*) (* expected: about 45 minutes in vm, about 19 minutes in native *)
Time Local Definition all_tokens_logits_concrete_value := native_compute logits_all_tokens_concrete_opt.
Time Definition all_tokens_logits_concrete : PArray.concrete_tensor _ _ := (*Eval native_compute in pre *)Eval hnf in extract all_tokens_logits_concrete_value.
Time Definition all_tokens_logits_concrete_eq : all_tokens_logits_concrete = logits_all_tokens_concrete_opt := extract_eq all_tokens_logits_concrete_value.
(* Proof. native_cast_no_check (eq_refl logits_all_tokens_concrete). Time Qed.*)
Definition all_tokens_logits : tensor _ _ := PArray.reabstract (fun _ => logits_all_tokens) all_tokens_logits_concrete.
Lemma all_tokens_logits_eq idxs : all_tokens_logits idxs = logits_all_tokens idxs.
Proof.
cbv [all_tokens_logits].
rewrite PArray.reabstract_ext_correct; [ reflexivity | ].
rewrite all_tokens_logits_concrete_eq, logits_all_tokens_concrete_opt_eq.
reflexivity.
Qed.