<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/tools, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>Merge PR #14024: [coqdep] error on non-existent and unreadable files</title>
<updated>2021-04-13T14:10:33+00:00</updated>
<author>
<name>coqbot-app[bot]</name>
</author>
<published>2021-04-13T14:10:33+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=ea62d1e19f2ba565ea3a18ba3709a06af5c845ac'/>
<id>ea62d1e19f2ba565ea3a18ba3709a06af5c845ac</id>
<content type='text'>
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: ejgallego
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: ejgallego
</pre>
</div>
</content>
</entry>
<entry>
<title>[coqdep] error on non-existent and unreadable files</title>
<updated>2021-04-12T19:31:12+00:00</updated>
<author>
<name>Hendrik Tews</name>
</author>
<published>2021-03-28T20:06:03+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=e1793962bebf1401026ed961ecc15b7eb60d57f5'/>
<id>e1793962bebf1401026ed961ecc15b7eb60d57f5</id>
<content type='text'>
Print an error message and return non-zero status for
non-existing or unreadable files. Unknown options produce a
warning and are otherwise ignored.
Fixes #14023
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Print an error message and return non-zero status for
non-existing or unreadable files. Unknown options produce a
warning and are otherwise ignored.
Fixes #14023
</pre>
</div>
</content>
</entry>
<entry>
<title>Merge PR #14038: [dune] [coqdoc] Install coqdoc.sty also in share/texmf</title>
<updated>2021-04-12T14:21:34+00:00</updated>
<author>
<name>coqbot-app[bot]</name>
</author>
<published>2021-04-12T14:21:34+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=bba57138fcb0badf307fb00b97d73b4933e3022b'/>
<id>bba57138fcb0badf307fb00b97d73b4933e3022b</id>
<content type='text'>
Reviewed-by: Zimmi48
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Reviewed-by: Zimmi48
</pre>
</div>
</content>
</entry>
<entry>
<title>Remove the omega tactic and related options</title>
<updated>2021-04-03T01:52:59+00:00</updated>
<author>
<name>Jim Fehrle</name>
</author>
<published>2021-01-11T22:47:13+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=d3a51ac24244f586dfeff1a93b68cb084370534e'/>
<id>d3a51ac24244f586dfeff1a93b68cb084370534e</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] [coqdoc] Install coqdoc.sty also in share/texmf</title>
<updated>2021-03-31T17:00:20+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2021-03-31T17:00:20+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=3d40b663fbefecbeb5b23dd9656c5342269c284a'/>
<id>3d40b663fbefecbeb5b23dd9656c5342269c284a</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<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>Get rid of the compilation date from the binaries to make them more stable.</title>
<updated>2021-02-16T08:02:37+00:00</updated>
<author>
<name>Guillaume Melquiond</name>
</author>
<published>2021-02-16T08:02:37+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=31e205ae752c5189143ef9ce87a3536db0cdeb62'/>
<id>31e205ae752c5189143ef9ce87a3536db0cdeb62</id>
<content type='text'>
Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".
</pre>
</div>
</content>
</entry>
<entry>
<title>Remove the SearchHead command</title>
<updated>2021-01-25T18:26:13+00:00</updated>
<author>
<name>Jim Fehrle</name>
</author>
<published>2021-01-19T19:55:49+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=3d46bed76e656d6a0e4d87320e4d0fd67d1211c2'/>
<id>3d46bed76e656d6a0e4d87320e4d0fd67d1211c2</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Avoid using "subgoals" in the UI, it means the same as "goals"</title>
<updated>2021-01-13T23:24:23+00:00</updated>
<author>
<name>Jim Fehrle</name>
</author>
<published>2020-12-17T23:04:36+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=3da2dbe9728ae7f5b1860a8e3a6c458e6d976f84'/>
<id>3da2dbe9728ae7f5b1860a8e3a6c458e6d976f84</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Fix broken HTML rendering of inference rules (fix #12783).</title>
<updated>2020-12-28T10:26:54+00:00</updated>
<author>
<name>Guillaume Melquiond</name>
</author>
<published>2020-12-28T09:29:34+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=aed648afd2cf8b09d67fb39c9672b71166089395'/>
<id>aed648afd2cf8b09d67fb39c9672b71166089395</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
</feed>
