From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- dev/doc/build-system.dev.txt | 70 ++++++++++ dev/doc/build-system.txt | 299 +++++++++++++++++++++++++++++++++++++++++++ dev/doc/changes.txt | 33 +++++ dev/doc/header | 7 - dev/doc/notes-on-conversion | 73 +++++++++++ dev/doc/perf-analysis | 80 +++++++++++- 6 files changed, 551 insertions(+), 11 deletions(-) create mode 100644 dev/doc/build-system.dev.txt create mode 100644 dev/doc/build-system.txt delete mode 100644 dev/doc/header create mode 100644 dev/doc/notes-on-conversion (limited to 'dev/doc') diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt new file mode 100644 index 00000000..c825f088 --- /dev/null +++ b/dev/doc/build-system.dev.txt @@ -0,0 +1,70 @@ +Since July 2007, Coq features a build system overhauled by Pierre +Corbineau and Lionel Elie Mamane. + +This file documents internals of the implementation of the build +system. For what a Coq developer needs to know about the build system, +see build-system.txt . + +.ml4 files +---------- + +.ml files corresponding to .ml4 files are created to keep ocamldep +happy only. To ensure they are not used for compilation, they contain +invalid OCaml. + +multi-stage build +----------------- + +Le processus de construction est séparé en trois étapes qui correspondent +aux outils nécessaires pour calculer les dépendances de cette étape: + +stage1: ocamldep, sed , camlp4 sans fichiers de Coq +stage2: camlp4 avec grammar.cma et/ou q_constr.cmo +stage3: coqdep (.vo) + +Le Makefile a été séparé en plusieurs fichiers : + +- Makefile: coquille vide qui délègue les cibles à la bonne étape sauf + clean et les fichiers pour emacs (car ils sont en quelque sorte en + "stage0": aucun calcul de dépendance nécessaire). +- Makefile.common : définitions des variables (essentiellement des + listes de fichiers) +- Makefile.build : les règles de compilation sans inclure de + dépendances +- Makefile.stage* : fichiers qui incluent les dépendances calculables + à cette étape ainsi que Makefile.build. + +The build needs to be cut in stages because make will not take into +account one include when making another include. + +Parallélisation +--------------- + +Le découpage en étapes veut dire que le makefile est un petit peu +moins parallélisable que strictement possible en théorie: par exemple, +certaines choses faites en stage2 pourraient être faites en parallèle +avec des choses de stage1. Nous essayons de minimiser cet effet, mais +nous ne l'avons pas complètement éliminé parce que cela mènerait à un +makefile très complexe. La minimisation est principalement que si on +demande un objet spécifique (par exemple "make parsing/g_constr.cmx"), +il est fait dans l'étape la plus basse possible (simplement), mais si +un objet est fait comme dépendance de la cible demandée (par exemple +dans un "make world"), il est fait le plus tard possible (par exemple, +tout code OCaml non nécessaire pour coqdep ni grammar.cma ni +q_constr.cmo est compilé en stage3 lors d'un "make world"; cela permet +le parallélisme de compilation de code OCaml et de fichiers Coq (.v)). + +Le "(simplement)" ci-dessus veut dire que savoir si un fichier non +nécessaire pour grammar.cma/q_constr.cmo peut en fait être fait en +stage1 est compliqué avec make, alors nous retombons en général sur le +stage2. La séparation entre le stage2 et stage3 est plus facile, donc +l'optimisation ci-dessus s'y applique pleinement. + +En d'autres mots, nous avons au niveau conceptuel deux assignations +d'étape pour chaque fichier: + + - l'étape la plus petite où nous savons qu'il peut être fait. + - l'étape la plus grande où il peut être fait. + +Mais seule la première est gérée explicitement, la seconde est +implicite. diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt new file mode 100644 index 00000000..c9571f7c --- /dev/null +++ b/dev/doc/build-system.txt @@ -0,0 +1,299 @@ +Since July 2007, Coq features a build system overhauled by Pierre +Corbineau and Lionel Elie Mamane. + +This file documents what a Coq developer needs to know about the build +system. If you want to enhance the build system itself (or are curious +about its implementation details), see build-system.dev.txt . + +The build system is not at its optimal state, see TODO section. + +Stages in build system +---------------------- + +The build system is separated into three stages, corresponding to the +tool(s) necessary to compute the dependencies necessary at this stage: + +stage1: ocamldep, sed, camlp4 without Coq extensions +stage2: camlp4 with grammar.cma and/or q_constr.cmo +stage3: coqdep (.vo) + +The file "Makefile" itself serves as minimum stage for targets that +should not need any dependency (such as *clean*). + +Changes (for old-timers) +------------------------ + +The contents of the old Makefile has been mostly split into: + + - variable declarations for file lists in Makefile.common. + + These declarations are now static (for faster Makefile execution), + so their definitions are order-dependent. + + - actual building rules and compiler flags variables in + Makefile.build + + +The handling of globals is now: the globals of FOO.v are in FOO.glob +and the global glob.dump is created by concatenation of all .glob +files. In particular, .glob files are now always created. + +See also section "cleaning targets" + +Reducing build system overhead +------------------------------ + +When you are actively working on a file in a "make a change, make to +test, make a change, make to test", etc mode, here are a few tips to +save precious time: + + - Always ask for what you want directly (e.g. bin/coqtop, + foo/bar.cmo, ...), don't do "make world" and interrupt + it when it has done what you want. This will try to minimise the + stage at which what you ask for is done (instead of maximising it + in order to maximise parallelism of the build process). + + For example, if you only want to test whether bin/coqtop still + builds (and eventually start it to test your bugfix or new + feature), don't do "make world" and interrupt it when bin/coqtop is + built. Use "make bin/coqtop" or "make coqbinaries" or something + like that. This will avoid entering the stage 3, and cut build + system overhead by 50% (1.2s instead of 2.4 on writer's machine). + + - You can turn off rebuilding of the standard library each time + bin/coqtop is rebuilt with NO_RECOMPILE_LIB=1. + + - If you want to avoid all .ml4 files being recompiled only because + grammar.cma was rebuilt, do "make ml4depclean" once and then use + NO_RECOMPILE_ML4=1. + + - The CM_STAGE1=1 option to make will build all .cm* files mentioned + as targets on the command line in stage1. Whether this will work is + your responsibility. It should work for .ml files that don't depend + (nor directly nor indirectly through transitive closure of the + dependencies) on any .ml4 file, or where those dependencies can be + safely ignored in the current situation (e.g. all these .ml4 files + don't need to be recompiled). + + This will avoid entering the stage2 (a reduction of 33% in + overhead, 0.4s on the writer's machine). + + - To jump directly into a stage (e.g. because you know nothing is to + be done in stage 1 or (1 and 2) or because you know that the target + you give can be, in this situation, done in a lower stage than the + build system dares to), use GOTO_STAGE=n. This will jump into stage + n and try to do the targets you gave in that stage. + + - To disable all dependency recalculation, use the NO_RECALC_DEPS=1 + option. It disables REcalculation of dependencies, not calculation + of dependencies. In other words, if a .d file does not exist, it is + still created, but it is not updated every time the source file + (e.g. .ml) is changed. + +General speed improvements: + + - When building both the native and bytecode versions, the + KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time + by running camlp4o only once on every .ml4 file, at the expense of + readability of compilation error messages for .ml4 files. + +Dependencies +------------ + +There are no dependencies in the archive anymore, they are always +bootstrapped. The dependencies of a file FOO are in FOO.d . This +enables partial recalculation of dependencies (only the dependencies +of changed files are recomputed). + +If you add a dependency to a Coq camlp4 extension (grammar.cma or +q_constr.cmo), then see sections ".ml4 files" and "new files". + +Cleaning Targets +---------------- + +Targets for cleaning various parts: + + - distclean: clean everything; must leave only what should end up in + distribution tarball and/or is in a svn checkout. + + - clean: clean everything except effect of "./configure" and documentation. + + - cleanconfig: clean effect of "./configure" only + + - archclean: remove all architecture-dependent generated files + - indepclean: remove all architecture-independent generated files + (not documentation) + + - objclean: clean all generated files, but not Makefile meta-data + (e.g. dependencies), nor debugging/development information nor + other cruft (e.g. editor backup files), nor documentation + + - docclean: clean documentation + +.ml4 files +---------- + +The camlp4-preprocessed version of FOO.ml4 is FOO.ml4-preprocessed and +can be obtained with: + make FOO.ml4-preprocessed + +If a .ml4 file uses a grammar extension from Coq (such as grammar.cma +or q_constr.cmo), it must contain a line like: + (*i camlp4deps: "grammar.cma q_constr.cmo" i*) + +If it uses a standard grammar extension, it must contain a line like: + (*i camlp4use: "pa_ifdef.cmo" i*) + +It can naturally contain both a camlp4deps and a camlp4use line. Both +are used for preprocessing. It is thus _not_ necessary to add a +specific rule for a .ml4 file in the Makefile.build just because it +uses grammar extensions. + +By default, the build system is geared towards development that may +use the Coq grammar extensions, but not development of Coq's grammar +extensions themselves. This means that .ml4 files are compiled +directly (using ocamlc/opt's -pp option), without use of an +intermediary .ml (or .ml4-preprocessed) file. This is so that if a +compilation error occurs, the location in the error message is a +location in the .ml4 file. If you are modifying the grammar +extensions, you may be more interested in the location of the error in +the .ml4-preprocessed file, so that you can see what your new grammar +extension made wrong. In that case, use the KEEP_ML4_PREPROCESSED=1 +option. This will make compilation of a .ml4 file a two-stage process: + +1) create the .ml4-preprocessed file with camlp4o +2) compile it with straight ocamlc/opt without preprocessor + +and will instruct make not to delete .ml4-preprocessed files +automatically just because they are intermediary files, so that you +can inspect them. + +If you add a _new_ grammar extension to Coq: + + - if it can be built at stage1, that is the .ml4 file does not use a + Coq grammar extension itself, then add it, and all .cmo files it + needs to STAGE1_TARGETS and STAGE_ML4 in Makefile.common. See the + handling of grammar.cma and q_constr.cmo for an example. + + - if it cannot be built at stage1, that is the .ml4 file itself needs + to be preprocessed with a Coq camlp4 grammar extension, then, + congratulations, you need to add a new stage between stage1 and + stage2. + +New files +--------- + +For a new file, in most cases, you just have to add it to the proper +file list(s) in Makefile.common, such as ARITHVO or TACTICS. + +The list of all ml4 files is not handled manually anymore. + +Exceptions are: + + - The file is necessary at stage1, that it is necessary to build the + Coq camlp4 grammar extensions. In this case, make sure it ends up + in STAGE1_CMO and (for .ml4 files) STAGE1_ML4. See the handling of + grammar.cma and/or q_constr.cmo for an example. + + - if the file needs to be compiled with -rectypes, add it to + RECTYPESML in Makefile.common. If it is a .ml4 file, implement + RECTYPESML4 or '(*i ocamlflags i*)'; see TODO. + + - the file needs a specific Makefile entry; add it to Makefile.build + + - the files produced from the added file do not match an existing + pattern or entry in "Makefile". (All the common cases of + .ml{,i,l,y,4}, .v, .c, ... files that produces (respectively) + .cm[iox], .vo, .glob, .o, ... files with the same basename are + already covered.) In this case, see section "New targets". + +New targets +----------- + +If you want to add: + + - a new PHONY target to the build system, that is a target that is + not the name of the file it creates, + + - a normal target is not already mapped to a stage by "Makefile" + + then: + + - add the necessary rule to Makefile.build, if any + - add the target to STAGEn_TARGETS, with n being the smallest stage + it can be built at, that is: + * 1 for OCaml code that doesn't use any Coq camlp4 grammar extension + * 2 for OCaml code that uses (directly or indirectly) a Coq + camlp4 grammar extension. Indirectly means a dependency of it + does. + * 3 for Coq (.v) code. + + *or* + + add a pattern matching the target to the pattern lists for the + smallest stage it can be built at in "Makefile". + +TODO +---- + +delegate pa_extend.cmo to camlp4use statements and remove it from +standard camlp4 options. + +maybe manage compilation flags (such as -rectypes or the CoqIDE ones) +from a + (*i ocamlflags: "-rectypes" i*) +statement in the .ml(4) files themselves, like camlp4use. The CoqIDE +files could have + (*i ocamlflags: "${COQIDEFLAGS}" i*) +and COQIDEFLAGS is still defined (and exported by) the Makefile.build. + +Clean up doc/Makefile + +config/Makefile looks like it contains a lot of unused variables, +clean that up (are any maybe used by nightly scripts on +pauillac?). Also, the COQTOP variable from config/Makefile (and used +in contribs) has a very poorly chosen name, because "coqtop" is the +name of a Coq executable! For example, in the Coq makefile it is +immediately clobbered by "bin/coqtop$(EXE)"! Rename it to COQROOT or +COQTREE or COQDIR or ... + +Promote the granular .glob handling to official way of doing things +for Coq developments, that is implement it in coq_makefile and the +contribs. Here are a few hints: + +>> Les fichiers de constantes produits par -dump-glob sont maintenant +>> produits par fichier et sont ensuite concaténés dans +>> glob.dump. Ilsont produits par défaut (avec les bonnes +>> dépendances). + +> C'est une chose que l'on voulait faire aussi. + +(J'ai testé et débogué ce concept sur CoRN dans les derniers mois.) + +> Est-ce que vous sauriez modifier coq_makefile pour qu'il procède de +> la même façon + +Dans cette optique, il serait alors plus propre de changer coqdep pour +qu'il produise directement l'output que nous mettons maintenant dans +les .v.d (qui est celui de coqdoc post-processé avec sed). + +Si cette manière de gérer les glob devient le standard béni +officiellement par "the Coq development team", ne voudrions nous pas +changer coqc pour qu'il produise FOO.glob lors de la compilation de +FOO.v par défaut (sans argument "-dump-glob")? + +> et que la production de a.html par coqdoc n'ait une dépendance qu'en +> les a.v et a.glob correspondant ? + +Je crois que coqdoc exige un glob-dump unique, il convient donc de +concaténer les .glob correspondants. Soit un glob-dump global par +projet (par Makefile), soit un glob-dump global par .v(o), qui +contient son .glob et ceux de tous les .v(o) atteignables par le +graphe des dépendances. CoRN contient déjà un outil de calcul de +partie atteignable du graphe des dépendances (il y est pour un autre +usage, pour calculer les .v à mettre dans les différents tarballs sur +http://corn.cs.ru.nl/download.html; les parties partielles sont +définies par liste de fichiers .v + toutes leurs dépendances +(in)directes), il serait alors adéquat de le mettre dans les tools de +Coq. + diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 90e29496..b7545e09 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,3 +1,36 @@ +========================================= += CHANGES BETWEEN COQ V8.1 AND COQ V8.2 = +========================================= + +A few differences in Coq ML interfaces between Coq V8.1 and V8.2 +================================================================ + +** Datatypes + +List of occurrences moved from "int list" to "Termops.occurrences" (an +alias to "bool * int list"). + +** Functions + +Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply +Tactics: apply_with_bindings -> apply_with_bindings_wo_evars +Eauto.simplest_apply -> Hiddentac.h_simplest_apply +Evarutil.define_evar_as_arrow -> define_evar_as_product + +** Universe names (univ.mli) + + base_univ -> type0_univ (* alias of Set is the Type hierarchy *) + prop_univ -> type1_univ (* the type of Set in the Type hierarchy *) + neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *) + is_base_univ -> is_type1_univ + is_empty_univ -> is_lower_univ + +** Sort names (term.mli) + + mk_Set -> set_sort + mk_Prop -> prop_sort + type_0 -> type1_sort + ========================================= = CHANGES BETWEEN COQ V8.0 AND COQ V8.1 = ========================================= diff --git a/dev/doc/header b/dev/doc/header deleted file mode 100644 index 57945e47..00000000 --- a/dev/doc/header +++ /dev/null @@ -1,7 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* nat := + match n0 with + | O => S + | S n1 => + fun m : nat => + (fix F0 (n2 : nat) : nat := + match n2 with + | O => F n1 1 + | S n3 => F n1 (F0 n3) + end) m + end) n. + +Notation OMEGA := (ack 4 4). + +Definition f (x:nat) := x. + +(* Evaluation in tactics can somehow be controled *) +Lemma l1 : OMEGA = OMEGA. +reflexivity. (* succeed: identity *) +Qed. (* succeed: identity *) + +Lemma l2 : OMEGA = f OMEGA. +reflexivity. (* fail: conversion wants to convert OMEGA with f OMEGA *) +Abort. (* but it reduces the right side first! *) + +Lemma l3 : f OMEGA = OMEGA. +reflexivity. (* succeed: reduce left side first *) +Qed. (* succeed: expected concl (the one with f) is on the left *) + +Lemma l4 : OMEGA = OMEGA. +assert (f OMEGA = OMEGA) by reflexivity. (* succeed *) +unfold f in H. (* succeed: no type-checking *) +exact H. (* succeed: identity *) +Qed. (* fail: "f" is on the left *) + +(* This example would fail whatever the preferred side is *) +Lemma l5 : OMEGA = f OMEGA. +unfold f. +assert (f OMEGA = OMEGA) by reflexivity. +unfold f in H. +exact H. +Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *) + +(**********************************************************************) +(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *) +(* (proof of span_ind_uninject_prop *) + +In the proof, a problem of the form (Equal S t1 t2) +is "simpl"ified, then "red"uced to (Equal S' t1 t1) +where the new t1's are surrounded by invisible coercions. +A reflexivity steps conclude the proof. + +The trick is that Equal projects the equality in the setoid S, and +that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)). + +At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1) +and the algorithm is to first compare S and S', and t1 and t2. +Unfortunately it does not work, and since t1 and t2 involve concrete +instances of algebraic structures, it takes a lot of time to realize that +it is not convertible. + +The only hope to improve this problem is to observe that S' hides +(behind two indirections) a Setoid constructor. This could be the +argument to solve the problem. + + diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis index f4cb3bff..8e481544 100644 --- a/dev/doc/perf-analysis +++ b/dev/doc/perf-analysis @@ -1,13 +1,79 @@ -Performance analysis for V8-0 branch ------------------------------------- +Performance analysis (trunk repository) +--------------------------------------- -Oct 29, 2006: polymorphism on definitions (+ 4%) +May 21, 2008: New version of CoRN + (needs +84% more time to compile) + +Apr 25-29, 2008: Temporary attempt with delta in eauto (Matthieu) + (+28% CoRN) + +Apr 17, 2008: improvement probably due to commit 10807 or 10813 (bug + fixes, control of zeta in rewrite, auto (??)) + (-18% Buchberger, -40% PAutomata, -28% IntMap, -43% CoRN, -13% LinAlg, + but CatsInZFC -0.5% only, PiCalc stable, PersistentUnionFind -1%) + +Mar 11, 2008: + (+19% PersistentUnionFind wrt Mar 3, +21% Angles, + +270% Continuations between 7/3 and 18/4) + +Mar 7, 2008: + (-10% PersistentUnionFind wrt Mar 3) + +Feb 20, 2008: temporary 1-day slow down + (+64% LinAlg) + +Feb 14, 2008: + (-10% PersistentUnionFind, -19% Groups) + +Feb 7, 8, 2008: temporary 2-days long slow down + (+20 LinAlg, +50% BDDs) + +Feb 2, 2008: many updates of the module system + (-13% LinAlg, -50% AMM11262, -5% Goedel, -1% PersistentUnionFind, + -42% ExactRealArithmetic, -41% Icharate, -42% Kildall, -74% SquareMatrices) + +Jan 1, 2008: merge of TypeClasses branch + (+8% PersistentUnionFind, +36% LinAlg, +76% Goedel) + +Nov 16, 17, 2007: + (+18% Cantor, +4% LinAlg, +27% IEEE1394 on 2 days) + +Nov 8, 2007: + (+18% Cantor, +16% LinAlg, +55% Continuations, +200% IEEE1394, +170% CTLTCTL, + +220% SquareMatrices) + +Oct 29, V8.1 (+ 3% geometry but CoRN, Godel, Kildall, Stalmark stables) + +Between Oct 12 and Oct 27, 2007: inefficiency temporarily introduced in the + tactic interpreter (from revision 10222 to 10267) + (+22% CoRN, +10% geometry, ...) + +Sep 16, 2007: + (+16% PersistentUnionFind on 3 days, LinAlg stable, + +Sep 4, 2007: + (+26% PersistentUnionFind, LinAlg stable, + +Jun 6, 2007: optimization of the need for type unification in with-bindings + (-3.5% Stalmark, -6% Kildall) + +May 20, 21, 22, 2007: improved inference of with-bindings (including activation + of unification on types) + (+4% PICALC, +5% Stalmark, +7% Kildall) + +May 11, 2007: added primitive integers (+6% CoLoR, +7% CoRN, +5% FSets, ...) + +Between Feb 22 and March 16, 2007: bench temporarily moved on JMN's + computer (-25% CoRN, -25% Fairisle, ...) + +Oct 29 and Oct 30, 2006: abandoned attempt to add polymorphism on definitions + (+4% in general during these two days) Oct 17, 2006: improvement in new field [r9248] (QArith -3%, geometry: -2%) Oct 5, 2006: fixing wrong unification of Meta below binders - (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, + (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, LinAlg: +7%, DISTRIBUTED_REFERENCE_COUNTING: +10%, CoLoR: +1%) Sep 26, 2006: new field [r9178-9181] @@ -17,11 +83,17 @@ Sep 26, 2006: new field [r9178-9181] Aug 12, 2006: Rocq/AREA_METHOD added (~ 480s) May 30, 2006: Nancy/CoLoR added (~ 319s) +May 23, 2006: new, lighter version of polymorphic inductive types + (CoRN: -27%, back to Mar-24 time) + May 17, 2006: changes in List.v (DISTRIBUTED_REFERENCE_COUNTING: -) May 5, 2006: improvement in closure (array instead of lists) (e.g. CatsInZFC: -10%, CoRN: -3%, +May 23, 2006: polymorphic inductive types (precise, heavy algorithm) + (CoRN: +37%) + Dec 29, 2005: new test and use of -vm in Stalmarck Dec 27, 2005: contrib Karatsuba added (~ 30s) -- cgit v1.2.3