ProfilingCoq
Workspace for the Profiling Coq work group at CIW2018
Objective: write down a tutorial on how to profile Coq to pin point the root cause of an inefficiency.
Plan: split the works in blocks, each with an expert and a tester. The expert documents/explains the tool then the tester validates the documentation and helps putting it in a decent form.
Blocks, sorted by "abstraction" level, descending.
Level: formalization style
- Recurrent problems: term comparison, unification, TC resolution
- Tools: ?, CI/pendulum(per-line-diff)
- Work around: locking, ...?
- Experts: enrico, matthieu
- Tester: anton
Level: Ltac
- Symptoms: slow ltac tactic
- Tools: ltacprof(proof-engine/ltac.rst), time?, Time, CI/pendulum(per-line-diff)
- Experts: enrico
- Tester:
Level: ML
- Problems: slow ML tactic
- Tools: lib/cProfile.ml
- Experts: enrico
- Task: unify ssrcommon.ml/mk_profile and lib/cProfile.ml
- Tester:
Level: VM
- Tools:
- Experts: maxime
- Tester: erik
Level: native compute
- Tools: perf
- Experts: maxime
- Tester:
Level: binary (eventual recompilation)
- Recurrent problems: slowness due to allocations/GC-cycles in tight loops
- Tools: perf + various OCaml branches
- Experts: pierre-marie (dev/doc/profiling.txt)
- Tester:
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.