<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/man, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<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>[coqdep] remove leftover Caml stuff from man page</title>
<updated>2021-03-28T21:19:35+00:00</updated>
<author>
<name>Hendrik Tews</name>
</author>
<published>2021-03-28T21:19:35+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=03fcea3ffd9dc640bb2bbc9be8074beb05e1a7f1'/>
<id>03fcea3ffd9dc640bb2bbc9be8074beb05e1a7f1</id>
<content type='text'>
Dependencies for Caml files was removed in PR #11589, but some
parts of it survived in the man page.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Dependencies for Caml files was removed in PR #11589, but some
parts of it survived in the man page.
</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>Remove (outdated) timestamps from man pages</title>
<updated>2020-05-10T17:12:46+00:00</updated>
<author>
<name>Kartik Singhal</name>
</author>
<published>2020-05-10T17:09:23+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=844142c5412a749921cb755a6a4110af5200742d'/>
<id>844142c5412a749921cb755a6a4110af5200742d</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Minimal fix to man pages.</title>
<updated>2020-04-02T20:14:01+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2020-04-02T13:51:09+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=0c1382bd0a9c41b559a912695e2154b758de7b18'/>
<id>0c1382bd0a9c41b559a912695e2154b758de7b18</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Merge PR #11593: Update bug report address in coqwc man page.</title>
<updated>2020-02-17T14:06:52+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2020-02-17T14:06:52+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=c51323a3cf1f4bb4c1ec170e3a1acfc6f5b1696b'/>
<id>c51323a3cf1f4bb4c1ec170e3a1acfc6f5b1696b</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>[coqdep] Remove support for `-c` ocamldep replacement.</title>
<updated>2020-02-13T21:11:05+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2020-02-12T22:12:26+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=8d73861eeae56321a106f28d07b47d5d6699939d'/>
<id>8d73861eeae56321a106f28d07b47d5d6699939d</id>
<content type='text'>
There is not need for coqdep to ship an `ocamldep` replacement, in
particular:

- not used in the main build since a long time
- not tested
- not kept up to date with upstream

This allows for a significant reduction of `coqdep` code, including
some duplicated code from `ocamllibdep`.

`coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files,
so it has then to be installed.

We also remove the residual `-slash` option.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
There is not need for coqdep to ship an `ocamldep` replacement, in
particular:

- not used in the main build since a long time
- not tested
- not kept up to date with upstream

This allows for a significant reduction of `coqdep` code, including
some duplicated code from `ocamllibdep`.

`coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files,
so it has then to be installed.

We also remove the residual `-slash` option.
</pre>
</div>
</content>
</entry>
<entry>
<title>Update bug report address in coqwc man page.</title>
<updated>2020-02-13T12:53:34+00:00</updated>
<author>
<name>Gaëtan Gilbert</name>
</author>
<published>2020-02-13T12:52:48+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=d6e8a9ff3834d0dad7ac26683fff950f061e08bc'/>
<id>d6e8a9ff3834d0dad7ac26683fff950f061e08bc</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[coqdep] Remove dumpgraph and broken options</title>
<updated>2020-02-07T12:24:53+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2020-02-05T11:53:37+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=fe6d6e9ab1291a03e5fe68287b90ee1b244e8f2d'/>
<id>fe6d6e9ab1291a03e5fe68287b90ee1b244e8f2d</id>
<content type='text'>
We remove the `dumpgraph` option which was causing quite a bit of
duplication, we also clean up options marked as broken `-w/-D`
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We remove the `dumpgraph` option which was causing quite a bit of
duplication, we also clean up options marked as broken `-w/-D`
</pre>
</div>
</content>
</entry>
<entry>
<title>Document -vos flag for coqdep</title>
<updated>2019-11-21T13:31:12+00:00</updated>
<author>
<name>Gaëtan Gilbert</name>
</author>
<published>2019-11-20T14:31:57+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=799bd29627c554f83c1ec9b4a226a739632cbc29'/>
<id>799bd29627c554f83c1ec9b4a226a739632cbc29</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
</feed>
