| Age | Commit message (Collapse) | Author |
|---|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
- Add a `--fuzz` option to `make-both-single-timing-files.py`
Passing `--fuzz=N` allows differences in character locations of up to
`N` characters when matching lines in per-line timing diffs.
The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`.
See also the discussion at
https://github.com/coq/coq/pull/11076#pullrequestreview-324791139
- Allow passing `--real` to per-file timing scripts and `--user` to
per-line timing script.
This allows easily comparing real times instead of user ones (or vice
versa).
- Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build
- We also now use argparse rather than a hand-rolled argument parser;
there were getting to be too many combinations of options.
- Fix the ordering of columns in Coq's build system; this is the
equivalent of #8167 for Coq's build system.
Fixes #11301
Supersedes / closes #11022
Supersedes / closes #11230
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
- The cutting plane has been (sometimes) improved to generate stronger
cuts.
- There is now some support for profiling the Simplex
see documentation for Show Lia Profile.
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: gares
|
|
This seems seldom used and I think in general instrumentation this way
is pretty limited (usually better to use the build system to tweak)
It thus seems worth removing as to simplify `Mltop` a bit, but of
course comments are welcome.
|
|
This is the smallest possible change to clarify the text without making it
even more formal.
|
|
|
|
Otherwise you need a few feedback loops to install all dependencies.
|
|
I lacked this package, and got:
``` $ make -j2 COQ_USE_DUNE=1 refman-html
[...]
env doc/sphinx_build (exit 2)
(cd _build/default/doc && /usr/bin/env COQLIB=.. sphinx-build -j4 -W -b html -d sphinx_build/doctrees sphinx sphinx_build/html)
Running Sphinx v2.1.2
Extension error:
Could not import extension sphinxcontrib.bibtex (exception: No module named 'sphinxcontrib.bibtex')
make: *** [refman-html] Error 1
```
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: maximedenes
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
|
|
|
|
- Mention Guillaume Claret among maintainers of the OPAM repository
(as suggested by Karl Palmskog).
- Update links to the documentation to avoid being outdated.
- Mention sections beyond the one on 8.11+beta1.
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
Ack-by: maximedenes
|
|
cons and nil
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
|
|
This partially fixes #10139 ; we now build the Ltac2 documentation and
deploy it.
The fix here can be used for inspiration to do the make-based part.
|
|
Reviewed-by: maximedenes
|
|
Fixes #3907: CoqIDE File->Revert all buffers does not work.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Partial fix of #11219: CoqIDE tactics and templates menus are out of sync.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
|
|
Reviewed-by: ppedrot
|
|
decorations
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
|
|
|
|
Fixes #10909: Set Default Proof Mode is not documented.
|
|
OCaml's string type
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: herbelin
Ack-by: maximedenes
Reviewed-by: pi8027
|
|
We make a temporary directory for these files and cleanup at process
exit. The temporary directory means we don't have to guess what
extensions ocaml will produce, we can just delete everything there.
We use Lazy to avoid spamming unused directories when ahead-of-time
compiling without actually using native casts / nativenorm (typically
stdlib files).
Sadly ocaml has "create temp file" but not "create temp dir", so we
have to copy the name generation code.
Fix #10495
|
|
(and not just…
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
The command `Set NativeCompute Timing` causes calls to `native_compute`
(as well as kernel calls to the native compiler) to emit separate timing
information about compilation, execution, and reification. This allows
more fine-grained timing of the native compiler without needing to set
the `-debug` flag.
|
|
Close #11036
|
|
|
|
|
|
|
