<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/config/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: pass -bin-annot to configure</title>
<updated>2020-09-09T13:18:49+00:00</updated>
<author>
<name>Gaëtan Gilbert</name>
</author>
<published>2020-07-22T11:08:49+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=cbb2efcaecff4e066d8ac37bd049a8e917bec9d6'/>
<id>cbb2efcaecff4e066d8ac37bd049a8e917bec9d6</id>
<content type='text'>
This ends up in coq_makefile's CAMLFLAGS so we need it to make merlin
work properly.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This ends up in coq_makefile's CAMLFLAGS so we need it to make merlin
work properly.
</pre>
</div>
</content>
</entry>
<entry>
<title>Avoid running configure when plugins/ modified</title>
<updated>2020-08-18T13:43:16+00:00</updated>
<author>
<name>Gaëtan Gilbert</name>
</author>
<published>2020-08-18T13:39:57+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=cd7b346ec5485138d93bc6a0308b9b8176d6e71f'/>
<id>cd7b346ec5485138d93bc6a0308b9b8176d6e71f</id>
<content type='text'>
We use an indirection, producing the sorted list of subdirectories of
plugins/, so that dune can recognize it hasn't changed and doesn't
rerun configure. Since configure regenerates a timestamp this avoids
recompiling the stdlib.

Fix #12750.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We use an indirection, producing the sorted list of subdirectories of
plugins/, so that dune can recognize it hasn't changed and doesn't
rerun configure. Since configure regenerates a timestamp this avoids
recompiling the stdlib.

Fix #12750.
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] Fix bug in auto-configure deps.</title>
<updated>2020-03-04T02:38:42+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2020-03-04T02:28:47+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=3940ca86e18e6274719d0b435d769ec8a06af7a7'/>
<id>3940ca86e18e6274719d0b435d769ec8a06af7a7</id>
<content type='text'>
`plugins` needs to be present to coq_makefile variables are properly
initialized.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
`plugins` needs to be present to coq_makefile variables are properly
initialized.
</pre>
</div>
</content>
</entry>
<entry>
<title>[configure] [dune] Fix configure under Dune in 32bit builds.</title>
<updated>2019-12-07T17:33:43+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2019-12-07T17:28:29+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=55e54479837cc70a5c070220a0bf32d0bbf55212'/>
<id>55e54479837cc70a5c070220a0bf32d0bbf55212</id>
<content type='text'>
`dev/header.c` is not registered as a dependency, so the configure
step under dune fails in 32bit builds.

Note we don't detect the problem due to dubious code in configure
ignoring stderr messages on process calls.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
`dev/header.c` is not registered as a dependency, so the configure
step under dune fails in 32bit builds.

Note we don't detect the problem due to dubious code in configure
ignoring stderr messages on process calls.
</pre>
</div>
</content>
</entry>
<entry>
<title>Have only one dune rule calling configure</title>
<updated>2019-11-11T16:43:23+00:00</updated>
<author>
<name>Pierre Roux</name>
</author>
<published>2019-11-10T15:12:04+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=09b39c339dd3fe21a0808097b5f7d1ab8cb47031'/>
<id>09b39c339dd3fe21a0808097b5f7d1ab8cb47031</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] [doc] Support for building the reference manual with Dune.</title>
<updated>2018-12-13T14:40:38+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2018-09-19T00:50:29+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=ddb3fae72826c0da3ba449be4ebc72e44c1ace16'/>
<id>ddb3fae72826c0da3ba449be4ebc72e44c1ace16</id>
<content type='text'>
This is a reduced version of #8503 as to provide a way to build the
reference manual with Dune.

Dune 1.6 supports (experimentally) directories as targets, thus we
introduce a rule that will call `sphinx` to build the manual.

This only provides build, however generation of `.install` rules is
not done, it will be hopefully addressed in #8503.

Note that we set `expire: 1 month` for all the artifacts we build with
Dune. IMHO this makes most sense as not to abuse Gitlab's hosting,
however of course we could consider a different deployment strategy if
wanted.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This is a reduced version of #8503 as to provide a way to build the
reference manual with Dune.

Dune 1.6 supports (experimentally) directories as targets, thus we
introduce a rule that will call `sphinx` to build the manual.

This only provides build, however generation of `.install` rules is
not done, it will be hopefully addressed in #8503.

Note that we set `expire: 1 month` for all the artifacts we build with
Dune. IMHO this makes most sense as not to abuse Gitlab's hosting,
however of course we could consider a different deployment strategy if
wanted.
</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>
<entry>
<title>[configure] [dune] Don't force the Dune user to set envars.</title>
<updated>2018-09-27T14:53:07+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2018-09-26T22:41:39+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=615c29be047eafac1ec1a9a853afe5a577873771'/>
<id>615c29be047eafac1ec1a9a853afe5a577873771</id>
<content type='text'>
In order to support sending the OPAM prefix to configure via Dune, we
introduced a `COQ_CONFIGURE_PREFIX` variable.

However, this had the pitfall that now the developer had to set it or
else face a hanging build due to configure expecting user input.

While we wait for a larger cleanup in `-prefix`, we introduce a
`no-ask` option in `./configure` that will avoid this problem. If
`-no-ask` is passed to `configure` no interactive question or display
will be shown to the user.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
In order to support sending the OPAM prefix to configure via Dune, we
introduced a `COQ_CONFIGURE_PREFIX` variable.

However, this had the pitfall that now the developer had to set it or
else face a hanging build due to configure expecting user input.

While we wait for a larger cleanup in `-prefix`, we introduce a
`no-ask` option in `./configure` that will avoid this problem. If
`-no-ask` is passed to `configure` no interactive question or display
will be shown to the user.
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] [configure] Allow to set prefix using environment variable.</title>
<updated>2018-09-20T23:01:02+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2018-09-10T09:37:09+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=81e4c7152da598c1750e7881b197a6fcf54e818d'/>
<id>81e4c7152da598c1750e7881b197a6fcf54e818d</id>
<content type='text'>
This is a hack to enable correct OPAM building, the medium-term plan
is to avoid having to set a prefix at configure time but instead using
a set of rules to locate the Coq library.

We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This is a hack to enable correct OPAM building, the medium-term plan
is to avoid having to set a prefix at configure time but instead using
a set of rules to locate the Coq library.

We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2
</pre>
</div>
</content>
</entry>
</feed>
