<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/test-suite/coq-makefile, 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>[test-suite] Ensure copies of files are writable</title>
<updated>2020-05-18T15:53:04+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2020-05-18T15:34:27+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=17de81c8c006e89088b2173d1aeaae24b4c09cfa'/>
<id>17de81c8c006e89088b2173d1aeaae24b4c09cfa</id>
<content type='text'>
This is needed for the case the sources are set to read-only mode, for
example when using Dune &gt;= 2.5 [needed for the global cache support]

Fixes #12264

Co-authored-by: Ignat Insarov &lt;kindaro@gmail.com&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This is needed for the case the sources are set to read-only mode, for
example when using Dune &gt;= 2.5 [needed for the global cache support]

Fixes #12264

Co-authored-by: Ignat Insarov &lt;kindaro@gmail.com&gt;
</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>Ignore -native-compiler option when disabled</title>
<updated>2020-04-15T14:38:24+00:00</updated>
<author>
<name>Pierre Roux</name>
</author>
<published>2020-04-10T15:49:03+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=88b1f400ef05142a1f05cd7dcb34a4c682b7ab83'/>
<id>88b1f400ef05142a1f05cd7dcb34a4c682b7ab83</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
</feed>
