Imported Upstream version 8.0pl3upstream/8.0pl3

2 files changed, 54 insertions, 3 deletions

diff --git a/dev/ocamldebug-v7.template b/dev/ocamldebug-v7.template
index 96c53192..1dd625c8 100644
--- a/dev/ocamldebug-v7.template
+++ b/dev/ocamldebug-v7.template
@@ -2,10 +2,10 @@
 
 # wrap around ocamldebug for Coq
 
-export COQTOP=COQTOPDIRECTORY
-export COQLIB=COQLIBDIRECTORY
+export COQTOP='COQTOPDIRECTORY'
+export COQLIB='COQLIBDIRECTORY'
 export COQTH=$COQLIB/theories
-CAMLBIN=CAMLBINDIRECTORY
+CAMLBIN='CAMLBINDIRECTORY'
 OCAMLDEBUG=$CAMLBIN/ocamldebug
 export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
 
diff --git a/dev/perf-analysis b/dev/perf-analysis
new file mode 100644
index 00000000..4295a573
--- /dev/null
+++ b/dev/perf-analysis
@@ -0,0 +1,51 @@
+Performance analysis for V8-0-bugfix branch
+-------------------------------------------
+
+  Dec 27, 2005: contrib Karatsuba added (~ 24s)
+
+Dec 1-14, 2005: benchmarking server down
+
+Nov 29 and Dec 16, 2005: size increase
+  due to new record flag in inductive for extraction
+
+  Oct 6, 2005: contribs IPC and Tait added (~ 22s and ~ 24s)
+ 
+  Aug 1, 2005: contrib Kildall added (~ 64s)
+ 
+Jul 26-Aug 2, 2005: bench down
+
+Jul 14-15, 2005: 4 contribs failed including CoRN
+
+  Jul 7, 2005: adding contrib Fermat4: but not compabible and remove on Jul 8
+
+  Jun 17, 2005: contrib Goodstein extended and moved to CantorOrdinals (~ 28s)
+
+Jun 4, 2005: significant time reduction
+   (e.g. Nijmegen/LinAlg: -15%, Nijmegen/QArith: stable; Nijmegen/CoRN: -1%)
+   only changes are the removal of an assert checking location and
+   the pre-definition of level 200 (could it be just a parsing improvement??)
+
+  May 19, 2005: contrib Goodstein and prfx (~ 9s) added 
+
+Apr 30, 2005: evaluation order of atomic tactics changed
+   (e.g. Nijmegen/CoRN: stable, Nijmegen/QArith: -2%, Nijmegen/LinAlg: +20%) 
+
+Mar 20, 2005: fixed Logic.with_check bug
+  improved whole V8-0-bugfix bench by 4 %
+  (e.g. Nijmegen/CoRN: - 7.5 %, Nijmegen/QARITH: - 1.5 %)
+
+Mar 7-10, 2005: unexplained time reduction 
+  (on Mar 7, changed Ppconstrnew univ printer only)
+  (note also a server upgrade around Mar 10)
+
+Feb 17, 2005: fixed omega bug #922 (wrong STATE dependency):
+  improved whole V8-0-bugfix bench by 2 %
+  (e.g. Nijmegen/CoRN: - 6.5 %, Nijmegen/QARITH: - 3 %)
+
+Feb 2, 2005: fixed ltac var interpretation order
+
+  Jan 13, 2005: contrib SumOfTwoSquare added (~ 37s)
+
+Dec 20-29, 2004: reduced whole V8-0-bugfix due to Berkeley/Godel failure
+
+Nov 27 - Dec 10, 2004: strong instability