| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #10704
|
|
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
|
|
CoqMakefile.
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
|
|
The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.
|
|
|
|
|
|
|
|
section.
|
|
The Python scripts now support `--no-include-mem` to turn it off, and
also support `--sort-by-mem`.
Closes #11575
|
|
We now use `$@` rather than `$*` so that we display the output target
rather than the stem of the rule. This is more consistent for rules
that users add (where the pattern variable might be something
insufficiently identifying), and also generalizes more nicely to mixing
multiple compilers (we get a clear difference between producing OCaml
files and producing .vo files, even if the filename is the same up to
the suffix). The result is that it's easy to describe what the timing
information of the build log records: each time comes with a label which
is a file name, and the time is the time it takes to produce that file.
|
|
|
|
(It was moved out onto a separate page.)
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
There is not need for coqdep to ship an `ocamldep` replacement, in
particular:
- not used in the main build since a long time
- not tested
- not kept up to date with upstream
This allows for a significant reduction of `coqdep` code, including
some duplicated code from `ocamllibdep`.
`coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files,
so it has then to be installed.
We also remove the residual `-slash` option.
|
|
|
|
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
|
|
document « Property »
more documentation fixes
[doc] destructed → destructured
[doc] another le_minus→lt_1_r
[doc] @jfehrle suggestions
[doc] more minor fixes
|
|
|
|
This improves error reporting. Addendum to #10515
|
|
|
|
Note that this description is identical to that of R. R should maybe start with the word "Recursively"?
|
|
The amount of dangerous warnings in plugins is out of hand, including
some very serious ones.
As Coq developers are maintaining plugins these days it makes sense to
require the contributions to follow the same coding discipline as in
the main tree, thus we require the set of warnings fatal warnings to
be the same in Coq and in plugins.
We don't mark deprecation as fatal as to allow time for migration.
Fixes #6974
|
|
|
|
We follow Proof General documentation, section 11.2 "Using the Coq
project file".
|
|
|
|
|
|
make make-pretty-timed- after -> make make-pretty-timed-after (remove
space between - and after) (and reflow paragraph)
Fix spacing around :: in print-pretty-single-time-diff
Closes #8396
|
|
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
|
|
'CoqIDE' of the Reference Manual.
|
|
Reference Manual.
|
|
Most existing uses of .. example did not use the first line as a title, so this
commit also adds appropriate blank lines.
|
|
|
|
They are not used anymore.
People should use Proof-General (and optionally Company-Coq) instead.
|
|
|
|
|
|
|
|
|
|
Including cross-reference TODOs.
I took down the number of warnings from 300 to 50.
|
|
Thanks to Laurent Théry for porting this chapter.
|
|
|
