| Age | Commit message (Collapse) | Author |
|---|
|
For readers of the changelog: title "Tools" become "Command-line tools".
For developers: changelog categories 07 and 08 are disambiguated.
|
|
|
|
|
|
|
|
Also pass `--output-sync` on the CI, as suggested in
https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect
against this failure mode.
Fixes #13062
|
|
Fixes #12845 (coqchk reports names from inner modules of opaque modules
as axioms)
I don't fully understand the code here, so I can't speak as to its
correctness, but it should be simple enough that reviewers can
understand what it's doing and whether or not it's correct.
This is useful for me in making progress towards
https://github.com/mit-plv/fiat-crypto/issues/736
|
|
The change introduced by 41a1d66 has broken the feature prior to its
initial release. We attempt to fix the issue, and add a comment to
warn feature developers in order to avoid facing the same issue again.
|
|
|
|
|
|
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
|
|
|
|
Fixes #12386
|
|
When encountering
```Coq
Module M : T.
...
Lemma c :...
...
Qed.
...
End M.
```
every field `c` without body in `T` but with a body in `M` is
registered as opacified in a table along with all constants
`opacified(c)` without body in the environment at this point (i.e.,
all axioms potentially used by c).
Then, when printing axioms, if `c` appears in the final environment it
is replaced by `opacified(c)` in the resulting list of axioms.
|
|
This, for example, improves the CI display, so that `$ echo
'end:coq.test'` does not appear on the same line as the end of the
timing table.
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
The Python scripts now support `--no-include-mem` to turn it off, and
also support `--sort-by-mem`.
Closes #11575
|
|
|
|
Reviewed-by: SkySkimmer
|
|
|
|
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.
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
We propose to add an environment to have foldable texts with HTML
output, more precisely:
(*begin details [: An optional summary] *)
some Coq and documentation material
(* end details *)
Currently, only the HTML output is supported. We could treat this
environment in LaTeX output as appendixes to output later.
|
|
Make sure that all initial load vernaculars that were specified on the command line are executed before processing the options set through -set on the command line.
The reason for this is that the load vernacular options can load plugins that define new Goptions. If these plugins are not loaded before the -set flags are processed,
then Goptions will emit a warning that the options of that plugin don't exist and ignore the flag.
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
|
|
|
|
- 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
|
|
|
|
|
|
|
|
(and not just…
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
It seems broken according to unicoq experiences https://gitter.im/coq/coq?at=5e0e3e0005298604982ac3f7
Building cmxa of mlpack is already this way.
|
|
if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
|
|
|
|
|
|
Types of changes are defined in the list defined by Keep a Changelog
1.0.0 (https://keepachangelog.com/en/1.0.0/):
- Added
- Changed
- Deprecated
- Fixed
- Removed
We exclude the type Security for now, even for soundness fixes,
because the process of handling security vulnerabilities is different
from anything we follow right now.
|
|
Close #6460
|
|
|
|
|
