diff options
| author | Maxime Dénès | 2019-02-01 12:55:59 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-01 12:55:59 +0100 |
| commit | aa2394d4ee6525b811db1e1eb58573c2f7aa749c (patch) | |
| tree | 8c1da5d75a777e5113d47804ced049bbb4ed3946 /dev | |
| parent | f6f9cf742ee5894be65d6e2de527e3ab5a643491 (diff) | |
| parent | d9fb8db86d5b4ddc79a207c5f0ac32eb98215e78 (diff) | |
Merge PR #9095: [toplevel] Deprecate `-compile` flag in favor of `coqc`
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/profiling.txt | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 29e87df6b8..8455d13377 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -10,7 +10,7 @@ In Coq source folder: opam switch 4.05.0+trunk+fp ./configure -local -debug make -perf record -g bin/coqtop -compile file.v +perf record -g bin/coqc file.v perf report -g fractal,callee --no-children To profile only part of a file, first load it using @@ -96,7 +96,7 @@ https://github.com/mshinwell/opam-repo-dev ### For memory dump: -CAMLRUNPARAM=T,mj bin/coqtop -compile file.v +CAMLRUNPARAM=T,mj bin/coqc file.v In another terminal: @@ -112,7 +112,7 @@ 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 +CAMLRUNPARAM=T,gr bin/coqc file.v In another terminal: |