chore: add commented set_option trace.profiler true for easy logging (l…

…eanprover#202)

### Description:

Add Lean debug logging commands into MemcpyVCG. Disabled by default to
prevent verbosity, but present in the codebase to allow easy
benchmarking.

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine?

Conformance succeeded

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

Co-authored-by: Shilpi Goel <shigoel@gmail.com>

Proofs/Experiments/Memcpy/MemCpyVCG.lean

@@ -441,6 +441,8 @@ end CutTheorems
 section PartialCorrectness
 
 -- set_option skip_proof.skip true in
+-- set_option trace.profiler true in
+-- set_option profiler true in
 set_option maxHeartbeats 0 in
 theorem Memcpy.extracted_2 (s0 si : ArmState)
   (h_si_x0_nonzero : si.x0 ≠ 0)
@@ -482,6 +484,8 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
 
 -- set_option skip_proof.skip true in
 set_option maxHeartbeats 0 in
+-- set_option trace.profiler true in
+-- set_option profiler true in
 theorem Memcpy.extracted_0 (s0 si : ArmState)
   (h_si_x0_nonzero : si.x0 ≠ 0)
   (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
@@ -550,6 +554,9 @@ theorem Memcpy.extracted_0 (s0 si : ArmState)
           }
   · intros n addr hsep
     apply Memcpy.extracted_2 <;> assumption
+
+-- set_option trace.profiler true in
+-- set_option profiler true in
 theorem partial_correctness :
   PartialCorrectness ArmState := by
   apply Correctness.partial_correctness_from_assertions