<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/doc/tools/docgram/dune, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<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>[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>Fix dune rules for @check-gram following recent changes.</title>
<updated>2020-11-13T08:20:21+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2020-11-13T08:20:21+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=53aa272821c2cd94e4b05382fa33449e851c7a90'/>
<id>53aa272821c2cd94e4b05382fa33449e851c7a90</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>{new,setoid_}ring -&gt; ring</title>
<updated>2020-10-02T11:23:30+00:00</updated>
<author>
<name>Maxime Dénès</name>
</author>
<published>2020-09-18T12:15:18+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=4476f64dc87fb86738fc4c9f939113b70843c035'/>
<id>4476f64dc87fb86738fc4c9f939113b70843c035</id>
<content type='text'>
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
</pre>
</div>
</content>
</entry>
<entry>
<title>Fix docgram's dune file following #12085.</title>
<updated>2020-09-08T15:24:59+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2020-09-08T15:24:59+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=461e0d6b0e3b17224f23032c82d26fbb0dab4e74'/>
<id>461e0d6b0e3b17224f23032c82d26fbb0dab4e74</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] [docgram] Remove bash hack thanks to new option -no-update.</title>
<updated>2020-03-30T10:24:43+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2020-03-29T20:12:47+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=431541f91a09e9d8fe3b027475975a771d93332a'/>
<id>431541f91a09e9d8fe3b027475975a771d93332a</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>New target check-gram to check if fullGrammar and orderedGrammar are up-to-date.</title>
<updated>2020-03-28T12:59:29+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2020-03-27T15:52:26+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=89a2b709d254aeab2950764a89017cf8424ddfd1'/>
<id>89a2b709d254aeab2950764a89017cf8424ddfd1</id>
<content type='text'>
Use `dune build @check-gram --auto-promote` to automatically update
these two files.  You will need to run it twice if the two files need
to be updated (which is the case most often) as Dune will stop after
the first diff failure.

The rst files are also updated but left in the `_build/` directory as
Dune wouldn't support targets outside the current directory.  You can
just `mv _build/default/doc/sphinx doc` to update them after running
the @check-gram target.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Use `dune build @check-gram --auto-promote` to automatically update
these two files.  You will need to run it twice if the two files need
to be updated (which is the case most often) as Dune will stop after
the first diff failure.

The rst files are also updated but left in the `_build/` directory as
Dune wouldn't support targets outside the current directory.  You can
just `mv _build/default/doc/sphinx doc` to update them after running
the @check-gram target.
</pre>
</div>
</content>
</entry>
<entry>
<title>Dune build rules for doc_grammar and fullGrammar.</title>
<updated>2020-03-12T09:48:33+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2020-03-10T16:40:14+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=6d690bf1ea5ad7fedf91865f52091daedb0cf43c'/>
<id>6d690bf1ea5ad7fedf91865f52091daedb0cf43c</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
</feed>
