aboutsummaryrefslogtreecommitdiff
path: root/coqprime/examples/TestLucas.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-02-05 15:24:42 -0500
committerGravatar Jason Gross <jgross@mit.edu>2016-02-05 15:24:42 -0500
commita47b49b11d17add5ca1ea5e650d2f344219b4f7e (patch)
tree699bff16674a68d1a5dc059bfdbd2f9ca85e95a7 /coqprime/examples/TestLucas.v
parent1f83ff39458ca80acf3192c938490cf4988b7489 (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.v151
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)
-
-
-*)