<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/test-suite/coq-makefile/timing/precomputed-time-tests, 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>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>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>
<entry>
<title>[tools] Remove support for python2</title>
<updated>2020-01-03T11:00:04+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2019-12-05T22:44:58+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=aad86c49b55bbdaa916c10b84272bec5a2b6a678'/>
<id>aad86c49b55bbdaa916c10b84272bec5a2b6a678</id>
<content type='text'>
Closes #10491

We re-add the header in doc/tools/coqrst/notations/fontsupport.py
which was removed by accident in 1a9c769ed363ee2f2784e7252af72e6c1e2fbcc6

The fontsupport script itself has been kept for reference, however it
is not involved by any build target as of today.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Closes #10491

We re-add the header in doc/tools/coqrst/notations/fontsupport.py
which was removed by accident in 1a9c769ed363ee2f2784e7252af72e6c1e2fbcc6

The fontsupport script itself has been kept for reference, however it
is not involved by any build target as of today.
</pre>
</div>
</content>
</entry>
<entry>
<title>Add non-utf8 timing test</title>
<updated>2019-12-26T18:52:55+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2019-12-02T20:33:12+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=f6a9b60b28c5cc9feb95d13411941a4604d6cae9'/>
<id>f6a9b60b28c5cc9feb95d13411941a4604d6cae9</id>
<content type='text'>
This should have been running already, but it was forgotten in #9872
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This should have been running already, but it was forgotten in #9872
</pre>
</div>
</content>
</entry>
<entry>
<title>[pretty-timing scripts] Don't barf on non-utf-8</title>
<updated>2019-03-31T18:09:06+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2019-03-31T14:40:56+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=2acd04d6d7d608920dd93b0a602e3214ffeb9ae5'/>
<id>2acd04d6d7d608920dd93b0a602e3214ffeb9ae5</id>
<content type='text'>
This fixes #9767 by silently ignoring input lines which are not valid
UTF-8.  We hereby assume that all file paths are valid UTF-8.

We also now actually test both python2 and python3 on the CI.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This fixes #9767 by silently ignoring input lines which are not valid
UTF-8.  We hereby assume that all file paths are valid UTF-8.

We also now actually test both python2 and python3 on the CI.
</pre>
</div>
</content>
</entry>
</feed>
