diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-07-18 13:22:21 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-07-18 13:54:14 -0400 |
| commit | 4ca5e88a3b31f81422cee8f861d5efee781ddfd9 (patch) | |
| tree | 2844a1130354d64894665641ca585be8d4191f26 /src | |
| parent | ea70d1b4931765977d67e00cc3f589c11d982fbb (diff) | |
vm_compute in peel_interp_app
With some help from @ppedrot in tracking things down. C.f.
https://github.com/mit-plv/fiat-crypto/pull/394#issuecomment-406010106
After | File Name | Before || Change | % Change
------------------------------------------------------------------------------------------------
8m48.43s | Total | 9m07.60s || -0m19.16s | -3.50%
------------------------------------------------------------------------------------------------
5m35.98s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m45.63s || -0m09.64s | -2.79%
1m29.20s | Experiments/NewPipeline/Toplevel2 | 1m38.67s || -0m09.46s | -9.59%
1m39.78s | Experiments/NewPipeline/Toplevel1 | 1m39.77s || +0m00.00s | +0.01%
0m01.18s | Experiments/NewPipeline/CLI | 0m01.31s || -0m00.13s | -9.92%
0m01.16s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.09s || +0m00.06s | +6.42%
0m01.14s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.14s || +0m00.00s | +0.00%
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 7a90eb5f0..1f86f656f 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -1583,7 +1583,7 @@ Ltac peel_interp_app _ := => reflexivity | [ |- ?R (Interp ?ev) ?c ] => let rc := constr:(GallinaReify.Reify c) in - unify ev rc; reflexivity + unify ev rc; vm_compute; reflexivity end ] ] end. Ltac pre_cache_reify _ := |