diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dev.txt | 34 | ||||
| -rw-r--r-- | dev/doc/build-system.txt | 15 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 99 | ||||
| -rw-r--r-- | dev/doc/ocamlbuild.txt | 30 | ||||
| -rw-r--r-- | dev/doc/profiling.txt | 76 |
5 files changed, 227 insertions, 27 deletions
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index af1120e97b..fefcb0937a 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -30,6 +30,11 @@ HISTORY: restricted set of .ml4 (see variable BUILDGRAMMAR). - then on the true target asked by the user. +* June 2016 (Pierre Letouzey) + The files in grammar/ are now self-contained, we could compile + grammar.cma (and q_constr.cmo) directly, no need for a separate + subcall to make nor awkward include-failed-and-retry. + --------------------------------------------------------------------------- @@ -59,29 +64,14 @@ Cons: Makefiles hierachy ------------------ -Le Makefile a été séparé en plusieurs fichiers : - -- Makefile: coquille vide qui lançant Makefile.build sauf pour - clean et quelques petites choses ne nécessitant par de calculs - de dépendances. -- Makefile.common : définitions des variables (essentiellement des - listes de fichiers) -- Makefile.build : contient les regles de compilation, ainsi que - le "include" des dépendances (restreintes ou non selon la variable - BUILDGRAMMAR). -- Makefile.doc : regles specifiques à la compilation de la documentation. - - -Parallélisation ---------------- +The Makefile is separated in several files : -Il y a actuellement un double appel interne à "make -f Makefile.build", -d'abord pour construire grammar.cma/q_constr.cmo, puis le reste. -Cela signifie que ce makefile est un petit peu moins parallélisable -que strictement possible en théorie: par exemple, certaines choses -faites lors du second make pourraient être faites en parallèle avec -le premier. En pratique, ce premier make va suffisemment vite pour -que cette limitation soit peu gênante. +- Makefile: wrapper that triggers a call to Makefile.build, except for + clean and a few other little things doable without dependency analysis. +- Makefile.common : variable definitions (mostly lists of files or + directories) +- Makefile.build : contains compilation rules, and the "include" of dependencies +- Makefile.doc : specific rules for compiling the documentation. FIND_VCS_CLAUSE diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 31d9875ad1..4593a6ad5e 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -113,15 +113,20 @@ Targets for cleaning various parts: - docclean: clean documentation -.ml4 files ----------- +.ml4/.mlp files +--------------- -If a .ml4 file uses a grammar extension from Coq (such as grammar.cma -or q_constr.cmo), it must contain a line like: +There is now two kinds of preprocessed files : + - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) + - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), + except coqide_main.ml4 and its specific rule + +This classification replaces the old mechanism of declaring the use +of a grammar extension via a line of the form: (*i camlp4deps: "grammar.cma q_constr.cmo" i*) The use of (*i camlp4use: ... i*) to mention uses of standard -extension such as IFDEF has been discontinued, the Makefile now +extension such as IFDEF has also been discontinued, the Makefile now always calls camlp4 with pa_macros.cmo and a few others by default. For debugging a Coq grammar extension, it could be interesting diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 2f631c6338..4135ddd2db 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,73 @@ = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= +** Notation_ops ** + +Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr. + +** Logging and Pretty Printing: ** + +* Printing functions have been removed from `Pp.mli`, which is now a + purely pretty-printing interface. Functions affected are: + +```` ocaml +val pp : std_ppcmds -> unit +val ppnl : std_ppcmds -> unit +val pperr : std_ppcmds -> unit +val pperrnl : std_ppcmds -> unit +val pperr_flush : unit -> unit +val pp_flush : unit -> unit +val flush_all : unit -> unit +val msg : std_ppcmds -> unit +val msgnl : std_ppcmds -> unit +val msgerr : std_ppcmds -> unit +val msgerrnl : std_ppcmds -> unit +val message : string -> unit +```` + + which are no more available. Users of `Pp.pp msg` should now use the + proper `Feedback.msg_*` function. Clients also have no control over + flushing, the back end takes care of it. + +* Feedback related functions and definitions have been moved to the + `Feedback` module. `message_level` has been renamed to + level. Functions moved from Pp to Feedback are: + +```` ocaml +val set_logger : logger -> unit +val std_logger : logger +val emacs_logger : logger +val feedback_logger : logger +```` + +* We now provide several loggers, `log_via_feedback` is removed in + favor of `set_logger feedback_logger`. Output functions are: + +```` ocaml +val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b +val msg_info : Pp.std_ppcmds -> unit +val msg_notice : Pp.std_ppcmds -> unit +val msg_warning : Pp.std_ppcmds -> unit +val msg_error : Pp.std_ppcmds -> unit +val msg_debug : Pp.std_ppcmds -> unit +```` + + with the `msg_*` functions being just an alias for `logger $Level`. + +* The main feedback functions are: + +```` ocaml +val set_feeder : (feedback -> unit) -> unit +val feedback : ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit +val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit +```` + Note that `feedback` doesn't take two parameters anymore. After + refactoring the following function has been removed: + +```` ocaml +val get_id_for_feedback : unit -> edit_or_state_id * route_id +```` + - The interface of the Context module was changed. Related types and functions were put in separate submodules. The mapping from old identifiers to new identifiers is the following: @@ -81,6 +148,38 @@ define_evar_* mostly used internally in the unification engine. - The Refine module was move out of Proofview. + Proofview.Refine.* ---> Refine.* + +- A statically monotonous evarmap type was introduced in Sigma. Not all the API + has been converted, so that the user may want to use compatibility functions + Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when + needed. Code can be straightforwardly adapted in the following way: + + let (sigma, x1) = ... in + ... + let (sigma, xn) = ... in + (sigma, ans) + + should be turned into: + + open Sigma.Notations + + let Sigma (x1, sigma, p1) = ... in + ... + let Sigma (xn, sigma, pn) = ... in + Sigma (ans, sigma, p1 +> ... +> pn) + +- The Proofview.Goal.*enter family of functions now takes a polymorphic + continuation given as a record as an argument. + + Proofview.Goal.enter begin fun gl -> ... end + + should be turned into + + open Proofview.Notations + + Proofview.Goal.enter { enter = begin fun gl -> ... end } + ========================================= = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = ========================================= diff --git a/dev/doc/ocamlbuild.txt b/dev/doc/ocamlbuild.txt new file mode 100644 index 0000000000..efedbc506e --- /dev/null +++ b/dev/doc/ocamlbuild.txt @@ -0,0 +1,30 @@ +Ocamlbuild & Coq +---------------- + +A quick note in case someone else gets interested someday in compiling +Coq via ocamlbuild : such an experimental build system has existed +in the past (more or less maintained from 2009 to 2013), in addition +to the official build system via gnu make. But this build via +ocamlbuild has been severly broken since early 2014 (and don't work +in 8.5, for instance). This experiment has attracted very limited +interest from other developers over the years, and has been quite +cumbersome to maintain, so it is now officially discontinued. +If you want to have a look at the files of this build system +(especially myocamlbuild.ml), you can fetch : + - my last effort at repairing this build system (up to coqtop.native) : + https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair + - coq official v8.5 branch (recent but broken) + - coq v8.4 branch(less up-to-date, but works). + +For the record, the three main drawbacks of this experiments were: + - recurrent issues with circularities reported by ocamlbuild + (even though make was happy) during the evolution of Coq sources + - no proper support of parallel build + - quite slow re-traversal of already built things +See the two corresponding bug reports on Mantis, or +https://github.com/ocaml/ocamlbuild/issues/52 + +As an interesting feature, I successfully used this to cross-compile +Coq 8.4 from linux to win32 via mingw. + +Pierre Letouzey, june 2016 diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt new file mode 100644 index 0000000000..9d2ebf0d4c --- /dev/null +++ b/dev/doc/profiling.txt @@ -0,0 +1,76 @@ +# How to profile Coq? + +I (Pierre-Marie Pédrot) mainly use two OCaml branches to profile Coq, whether I +want to profile time or memory consumption. AFAIK, this only works for Linux. + +## Time + +In Coq source folder: + +opam switch 4.02.1+fp +./configure -local -debug +make +perf record -g bin/coqtop -compile file.v +perf report -g fractal,callee --no-children + +To profile only part of a file, first load it using + +bin/coqtop -l file.v + +and plug into the process + +perf record -g -p PID + +## Memory + +You first need a few commits atop trunk for this to work. + +git remote add ppedrot https://github.com/ppedrot/coq.git +git fetch ppedrot +git checkout ppedrot/allocation-profiling +git rebase master + +Then: + +opam switch 4.00.1+alloc-profiling +./configure -local -debug +make + +Note that linking the coqtop binary takes quite an amount of time with this +branch, so do not worry too much. There are more recent branches of +alloc-profiling on mshinwell's repo which can be found at: + +https://github.com/mshinwell/opam-repo-dev + +### For memory dump: + +CAMLRUNPARAM=T,mj bin/coqtop -compile file.v + +In another terminal: + +pkill -SIGUSR1 $COQTOPPID +... +pkill -SIGUSR1 $COQTOPPID +dev/decode-major-heap.sh heap.$COQTOPPID.$N bin/coqtop + +where $COQTOPPID is coqtop pid and $N the index of the call to pkill. + +First column is the memory taken by the objects (in words), second one is the +number of objects and third is the place where the objects where allocated. + +### For complete memory graph: + +CAMLRUNPARAM=T,gr bin/coqtop -compile file.v + +In another terminal: + +pkill -SIGUSR1 $COQTOPPID +... +pkill -SIGUSR1 $COQTOPPID +ocaml dev/decodegraph.ml edge.$COQTOPPID.$N bin/coqtop > memory.dot +dot -Tpdf -o memory.pdf memory.dot + +where $COQTOPPID is coqtop pid and $N the index of the call to pkill. + +The pdf produced by the last command gives a compact graphical representation of +the various objects allocated. |