diff options
author | Jason Gross <jgross@mit.edu> | 2016-02-05 15:24:42 -0500 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:39:02 -0400 |
commit | c33166b756b0b6bd8141130bcdf8053ffff790e5 (patch) | |
tree | 3e93aa97f5b2c308c11d9abf94abd86bc8f1cf9b /coqprime/examples/TestLucas.v | |
parent | ceb005a2bfde307ccfe6a3a52efd5f07f5483f84 (diff) |
Update build process to use COQPATH & _CoqProject
Removed all of the files not built by default; they can be resurrected from git
history. _CoqProject is the standard way to list the files in a project and to
give information to coq_makefile. COQPATH is the standard way to make use of
not-yet-installed libraries that are not part of your project (i.e., you don't
want to remove them when you `make clean`, etc.).
Diffstat (limited to 'coqprime/examples/TestLucas.v')
-rw-r--r-- | coqprime/examples/TestLucas.v | 151 |
1 files changed, 0 insertions, 151 deletions
diff --git a/coqprime/examples/TestLucas.v b/coqprime/examples/TestLucas.v deleted file mode 100644 index 370a072f7..000000000 --- a/coqprime/examples/TestLucas.v +++ /dev/null @@ -1,151 +0,0 @@ - -(*************************************************************) -(* 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) - - -*) |