<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/test-suite/coq-makefile/timing, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>[build] Split stdlib to it's own opam package.</title>
<updated>2021-03-03T15:06:14+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2020-06-22T15:52:18+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=ab98d847d237af3cd0e46edef42218be65cfc98f'/>
<id>ab98d847d237af3cd0e46edef42218be65cfc98f</id>
<content type='text'>
We introduce a new package structure for Coq:

- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`

This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.

The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.

Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.

There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.

This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.

IMHO the plan should work fine.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We introduce a new package structure for Coq:

- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`

This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.

The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.

Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.

There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.

This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.

IMHO the plan should work fine.
</pre>
</div>
</content>
</entry>
<entry>
<title>[CI] Update coq_makefile</title>
<updated>2020-11-20T18:08:08+00:00</updated>
<author>
<name>Pierre Roux</name>
</author>
<published>2020-11-13T11:03:19+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=146415fb624c182493d46413d738a3c2c3f47e02'/>
<id>146415fb624c182493d46413d738a3c2c3f47e02</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Make print-pretty-timed robust against non-output-sync logs</title>
<updated>2020-09-21T16:42:14+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2020-09-21T16:38:25+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=fef5b75e72e1dc2889875616f56332a00dc50534'/>
<id>fef5b75e72e1dc2889875616f56332a00dc50534</id>
<content type='text'>
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
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
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
</pre>
</div>
</content>
</entry>
<entry>
<title>Fix an uncaught python exception in timing</title>
<updated>2020-05-21T22:00:50+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2020-05-21T21:48:02+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=7731b8878d6a8c78874f6657745fa61d2703ee53'/>
<id>7731b8878d6a8c78874f6657745fa61d2703ee53</id>
<content type='text'>
Previously, when either the 'before' or 'after' had no files, we'd get
an uncaught exception:
```
Traceback (most recent call last):
  File "/home/jgross/Documents/repos/coq/tools/make-both-time-files.py", line 16, in &lt;module&gt;
    table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by, include_mem=args.include_mem, sort_by_mem=args.sort_by_mem)
  File "/home/jgross/Documents/repos/coq/tools/TimeFileMaker.py", line 391, in make_diff_table_string
    right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values())
ValueError: max() arg is an empty sequence
```

Fixes #12387
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Previously, when either the 'before' or 'after' had no files, we'd get
an uncaught exception:
```
Traceback (most recent call last):
  File "/home/jgross/Documents/repos/coq/tools/make-both-time-files.py", line 16, in &lt;module&gt;
    table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by, include_mem=args.include_mem, sort_by_mem=args.sort_by_mem)
  File "/home/jgross/Documents/repos/coq/tools/TimeFileMaker.py", line 391, in make_diff_table_string
    right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values())
ValueError: max() arg is an empty sequence
```

Fixes #12387
</pre>
</div>
</content>
</entry>
<entry>
<title>Print a newline at the end of timing tables</title>
<updated>2020-05-20T19:23:14+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2020-05-19T20:09:47+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=0f8de9b967fe82ef8e9eef5e258d9ef96788929e'/>
<id>0f8de9b967fe82ef8e9eef5e258d9ef96788929e</id>
<content type='text'>
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.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
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.
</pre>
</div>
</content>
</entry>
<entry>
<title>Add memory stats to tables by default</title>
<updated>2020-04-24T21:22:33+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2020-02-14T21:57:13+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=d8d0e1164b81d0968c31373de58f8c74bd47119b'/>
<id>d8d0e1164b81d0968c31373de58f8c74bd47119b</id>
<content type='text'>
The Python scripts now support `--no-include-mem` to turn it off, and
also support `--sort-by-mem`.

Closes #11575
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
The Python scripts now support `--no-include-mem` to turn it off, and
also support `--sort-by-mem`.

Closes #11575
</pre>
</div>
</content>
</entry>
<entry>
<title>TIMEFMT: Display the output file name</title>
<updated>2020-04-20T16:32:53+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2020-04-19T18:17:58+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=9849b21d756f2603e57363124be83bd87ff33af6'/>
<id>9849b21d756f2603e57363124be83bd87ff33af6</id>
<content type='text'>
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.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
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.
</pre>
</div>
</content>
</entry>
<entry>
<title>Fix Makefile warning: undefined variable '*'</title>
<updated>2020-04-19T18:43:55+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2020-04-19T18:17:58+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=ff293b3564efec8c911c3df9cd3a71863161d8b3'/>
<id>ff293b3564efec8c911c3df9cd3a71863161d8b3</id>
<content type='text'>
We fix
```
Makefile.build:222: warning: undefined variable '*'
```
by not passing a time format including a Makefile variable when not
inside a target (and whether or not the command succeeds should not
depend on the particular format in any case, and all we are testing for
is whether or not the command exists and supports `-f`).
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We fix
```
Makefile.build:222: warning: undefined variable '*'
```
by not passing a time format including a Makefile variable when not
inside a target (and whether or not the command succeeds should not
depend on the particular format in any case, and all we are testing for
is whether or not the command exists and supports `-f`).
</pre>
</div>
</content>
</entry>
<entry>
<title>Add --fuzz, --real, --user to timing scripts</title>
<updated>2020-02-05T21:55:28+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2019-12-17T20:14:24+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=6799ad6240fa4d233f698c3cfa0bd5417f471bba'/>
<id>6799ad6240fa4d233f698c3cfa0bd5417f471bba</id>
<content type='text'>
- 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
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
- 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
</pre>
</div>
</content>
</entry>
<entry>
<title>Merge PR #11341: Add non-utf8 timing test</title>
<updated>2020-01-08T13:38:18+00:00</updated>
<author>
<name>Pierre-Marie Pédrot</name>
</author>
<published>2020-01-08T13:38:18+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=3cdbd61f3acf0722c92f8192425eb1a677270b08'/>
<id>3cdbd61f3acf0722c92f8192425eb1a677270b08</id>
<content type='text'>
Reviewed-by: ppedrot
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Reviewed-by: ppedrot
</pre>
</div>
</content>
</entry>
</feed>
