aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-11-05 20:54:57 -0500
committerGravatar Jason Gross <jasongross9@gmail.com>2018-11-06 14:10:15 -0500
commit5cb258c09a602be3a6414b9c70fc7e1ab4b178b8 (patch)
tree427b9362b171fdaed3dc4183c577df8b7242fd4e /src
parentb61866e190f4e82cd133410b9cf89eb2c1bee38e (diff)
Disable very very slow printing
The number of lines of code in the synthesized p256 mulmod went from 2253 to 7575, and the time of printing went from about 161 s to about 3653 s. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------- 5m25.05s | Total | 66m04.61s || -60m39.56s | -91.80% ----------------------------------------------------------------------------------------------------- 5m25.05s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 66m04.62s || -60m39.56s | -91.80%
Diffstat (limited to 'src')
-rw-r--r--src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v b/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v
index b2d76911c..ab005cf27 100644
--- a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v
+++ b/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v
@@ -748,9 +748,9 @@ Module P256_32.
Local Notation "'adc32' '(' c ',' x ',' y ')'" :=
(#(Z_cast2 (uint32, bool)%core) @ (#Z_add_with_get_carry @ #(ident.Literal (t:=base.type.Z) 4294967296) @ c @ x @ y))%expr (at level 50) : expr_scope.
- (* Print is too slow *)
+ (* Print is too slow (it takes about an hour) *)
- Time Print mulmod.
+ (*Time Print mulmod.*)
(*
mulmod =