diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-11-06 16:56:46 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-11-07 15:34:52 -0500 |
| commit | 10a53166839f97f92b64b353fac01c627e6d8e7c (patch) | |
| tree | e0ce6b33d93a8d275179fcbcec76d06148f6a18b /src | |
| parent | 57f2735df3dbcb3f6045ee47b208239da47c4eb1 (diff) | |
Revert "Disable very very slow printing"
This reverts commit 5cb258c09a602be3a6414b9c70fc7e1ab4b178b8.
Since we fixed adjust_s, we don't actually need to remove the print
statement, as it only takes 3 minutes rather than 50.
After | File Name | Before || Change | % Change
---------------------------------------------------------------------------------------------------
6m12.87s | Total | 3m27.44s || +2m45.43s | +79.74%
---------------------------------------------------------------------------------------------------
6m12.88s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 3m27.45s || +2m45.43s | +79.74%
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v b/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v index ab005cf27..b2d76911c 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 (it takes about an hour) *) + (* Print is too slow *) - (*Time Print mulmod.*) + Time Print mulmod. (* mulmod = |