diff options
Diffstat (limited to 'coqprime/examples/TestLucas.v')
| -rw-r--r-- | coqprime/examples/TestLucas.v | 151 |
1 files changed, 151 insertions, 0 deletions
diff --git a/coqprime/examples/TestLucas.v b/coqprime/examples/TestLucas.v new file mode 100644 index 000000000..370a072f7 --- /dev/null +++ b/coqprime/examples/TestLucas.v @@ -0,0 +1,151 @@ + +(*************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(*************************************************************) +(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) +(*************************************************************) + +Require Import Lucas. + +Eval vm_compute in 2. + +Time Eval vm_compute in lucas 2. + +Eval vm_compute in 3. + +Time Eval vm_compute in lucas 3. + +Eval vm_compute in 5. + +Time Eval vm_compute in lucas 5. + +Eval vm_compute in 7. + +Time Eval vm_compute in lucas 7. + +Eval vm_compute in 13. + +Time Eval vm_compute in lucas 13. + +Eval vm_compute in 17. + +Time Eval vm_compute in lucas 17. + +Eval vm_compute in 19. + +Time Eval vm_compute in lucas 19. + +Eval vm_compute in 31. + +Time Eval vm_compute in lucas 31. + +Eval vm_compute in 61. + +Time Eval vm_compute in lucas 61. + +Eval vm_compute in 89. + +Time Eval vm_compute in lucas 89. + +Eval vm_compute in 107. + +Time Eval vm_compute in lucas 107. + +Eval vm_compute in 127. + +Time Eval vm_compute in lucas 127. + +Eval vm_compute in 521. + +Time Eval vm_compute in lucas 521. + +Eval vm_compute in 607. + +Time Eval vm_compute in lucas 607. + +Eval vm_compute in 1279. + +Time Eval vm_compute in lucas 1279. + +Eval vm_compute in 2203. + +Time Eval vm_compute in lucas 2203. + +Eval vm_compute in 2281. + +Time Eval vm_compute in lucas 2281. + +Eval vm_compute in 3217. + +Time Eval vm_compute in lucas 3217. + +Eval vm_compute in 4253. + +Time Eval vm_compute in lucas 4253. + +Eval vm_compute in 4423. + +Time Eval vm_compute in lucas 4423. + +(* + = 3 + = 0 +Finished transaction in 0. secs (0.01u,0.s) + = 5 + = 0 +Finished transaction in 0. secs (0.u,0.s) + = 7 + = 0 +Finished transaction in 0. secs (0.u,0.s) + = 13 + = 0 +Finished transaction in 0. secs (0.u,0.s) + = 17 + = 0 +Finished transaction in 0. secs (0.u,0.s) + = 19 + = 0 +Finished transaction in 0. secs (0.u,0.s) + = 31 + = 0 +Finished transaction in 0. secs (0.u,0.s) + = 61 + = 0 +Finished transaction in 0. secs (0.01u,0.s) + = 89 + = 0 +Finished transaction in 0. secs (0.02u,0.s) + = 107 + = 0 +Finished transaction in 0. secs (0.02u,0.s) + = 127 + = 0 +Finished transaction in 0. secs (0.04u,0.s) + = 521 + = 0 +Finished transaction in 2. secs (1.85u,0.01s) + = 607 + = 0 +Finished transaction in 3. secs (2.78u,0.07s) + = 1279 + = 0 +Finished transaction in 21. secs (20.21u,0.26s) + = 2203 + = 0 +Finished transaction in 94. secs (89.1u,1.05s) + = 2281 + = 0 +Finished transaction in 102. secs (97.59u,1.1s) + = 3217 + = 0 +Finished transaction in 244. secs (237.65u,2.39s) + = 4253 + = 0 +Finished transaction in 506. secs (494.09u,4.65s) + = 4423 + = 0 +Finished transaction in 572. secs (563.27u,5.45s) + + +*) |