<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/test-suite/dune, 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>[dune] [test-suite] pass BIN= as the regular makefile does</title>
<updated>2020-12-04T14:05:40+00:00</updated>
<author>
<name>Enrico Tassi</name>
</author>
<published>2020-12-04T14:05:40+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=9fb840fa5f33f593bc204765a13c027155559c2e'/>
<id>9fb840fa5f33f593bc204765a13c027155559c2e</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[test-suite] Fix printers test</title>
<updated>2019-06-24T11:14:45+00:00</updated>
<author>
<name>Gaëtan Gilbert</name>
</author>
<published>2019-06-19T12:44:29+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=a3549bef1b4d4498f91e6ad35ae65b48a2fb302f'/>
<id>a3549bef1b4d4498f91e6ad35ae65b48a2fb302f</id>
<content type='text'>
- fix the printers themselves after discharge was moved to the kernel

- change the test to make it more robust
  In addition to checking that there is no "Error|Unbound" in the
  output, ensure that the "go" function at the end of base_include
  is defined. If there are any errors in base_include it won't be defined.

This makes us find out that the test was silently failing in all CI
jobs except trunk+make. It failed to find the "include" file and so
failed with "could not find file include.", which we didn't detect.
To fix this:

- change automatically included paths in Coqinit.init_ocaml_path to be
  based on coqlib instead of coqroot. This way top_printers.ml and
  base_include can find the compiled ml objects.

- fix for dune: adapt the script to use include_dune when INSIDE_DUNE,
  add dependencies to test-suite/dune.

  The dependencies should be calculated automatically once Dune has
  better support for debug, or we implement proper support for test
  printers.

Co-authored-by: Emilio Jesus Gallego Arias &lt;e+git@x80.org&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
- fix the printers themselves after discharge was moved to the kernel

- change the test to make it more robust
  In addition to checking that there is no "Error|Unbound" in the
  output, ensure that the "go" function at the end of base_include
  is defined. If there are any errors in base_include it won't be defined.

This makes us find out that the test was silently failing in all CI
jobs except trunk+make. It failed to find the "include" file and so
failed with "could not find file include.", which we didn't detect.
To fix this:

- change automatically included paths in Coqinit.init_ocaml_path to be
  based on coqlib instead of coqroot. This way top_printers.ml and
  base_include can find the compiled ml objects.

- fix for dune: adapt the script to use include_dune when INSIDE_DUNE,
  add dependencies to test-suite/dune.

  The dependencies should be calculated automatically once Dune has
  better support for debug, or we implement proper support for test
  printers.

Co-authored-by: Emilio Jesus Gallego Arias &lt;e+git@x80.org&gt;
</pre>
</div>
</content>
</entry>
<entry>
<title>Fix dependencies of new test file.</title>
<updated>2019-05-22T18:09:33+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2019-05-14T11:49:00+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=056d1c3a9f5e220c2ad9877c87a559fc454b7d0f'/>
<id>056d1c3a9f5e220c2ad9877c87a559fc454b7d0f</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Add a test that unreleased changelog of released versions is empty.</title>
<updated>2019-05-08T18:51:31+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2019-05-08T18:51:31+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=963b950f201614078a432d1ac7568e8757d8df19'/>
<id>963b950f201614078a432d1ac7568e8757d8df19</id>
<content type='text'>
This test is active only when configure `is_a_released_version` is set
to true. In this case, to pass the test-suite, there must be no
unreleased changelog entries left, i.e. `doc/changelog/*/` must only
contain `00000-title.rst` files.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This test is active only when configure `is_a_released_version` is set
to true. In this case, to pass the test-suite, there must be no
unreleased changelog entries left, i.e. `doc/changelog/*/` must only
contain `00000-title.rst` files.
</pre>
</div>
</content>
</entry>
<entry>
<title>Set COQLIB so the test suite will run locally on Windows.</title>
<updated>2019-03-01T18:24:22+00:00</updated>
<author>
<name>Jim Fehrle</name>
</author>
<published>2019-02-27T05:53:25+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=7b3779b27be9221def05a341d79ddd45540b4280'/>
<id>7b3779b27be9221def05a341d79ddd45540b4280</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[azure] [ci] Build on Windows using Dune.</title>
<updated>2019-02-20T12:34:15+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2019-02-17T00:03:12+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=565a30614c6df16466f66cac1e517f9202612709'/>
<id>565a30614c6df16466f66cac1e517f9202612709</id>
<content type='text'>
We may want to keep the make-based and Dune job, however the
make-based setup is tested by the INRIA workers so it may not be
needed.

In order for some test to run well, we always run in Dune with an
absolute path. The easiest way to get a portable absolute path is to
use OCaml itself so we introduce a small executable to do that.

While we are at it, we do some cleanup of the test-suite `dune` file,
in particular we remove useless comments, set `--no-buffer` so results
can be seen in real time, and recognize the `NJOBS` variable as we
have moved to a Dune version that supports env vars.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We may want to keep the make-based and Dune job, however the
make-based setup is tested by the INRIA workers so it may not be
needed.

In order for some test to run well, we always run in Dune with an
absolute path. The easiest way to get a portable absolute path is to
use OCaml itself so we introduce a small executable to do that.

While we are at it, we do some cleanup of the test-suite `dune` file,
in particular we remove useless comments, set `--no-buffer` so results
can be seen in real time, and recognize the `NJOBS` variable as we
have moved to a Dune version that supports env vars.
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] [gitlab] Test OCaml trunk.</title>
<updated>2018-12-14T15:04:35+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2018-10-25T11:05:36+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=85b91b71abe7e60a9096ae31b9d0b4afda2189bb'/>
<id>85b91b71abe7e60a9096ae31b9d0b4afda2189bb</id>
<content type='text'>
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`]

CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit`
cannot be currently installed, thus we have to add a switch to the
test suite to disable `unit-tests`.

Many deprecation warnings happened in 4.08 so we use the `release`
profile to make them not fatal. Using a 4.08 build profile would be an
option too.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`]

CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit`
cannot be currently installed, thus we have to add a switch to the
test suite to disable `unit-tests`.

Many deprecation warnings happened in 4.08 so we use the `release`
profile to make them not fatal. Using a 4.08 build profile would be an
option too.
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] [test-suite] Support for running the test suite with Dune.</title>
<updated>2018-10-11T12:32:33+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2018-09-26T20:49:20+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=9e39d88ffb5829a9e2c82fbf54c0765a819b3e5e'/>
<id>9e39d88ffb5829a9e2c82fbf54c0765a819b3e5e</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
</feed>
