<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/.gitignore, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>Gitignore update for doc_grammar.</title>
<updated>2021-04-12T14:38:24+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2021-04-12T14:38:24+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=906b88c665d12f31aa9cd584fc2c7c66edef434f'/>
<id>906b88c665d12f31aa9cd584fc2c7c66edef434f</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>Add a file coq_arity.h generated by genOpcodeFiles.ml.</title>
<updated>2021-02-19T10:17:26+00:00</updated>
<author>
<name>Guillaume Melquiond</name>
</author>
<published>2021-02-17T11:09:00+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=c7bbe4729dc53ddf3a02a7ae3816ec3c146d452e'/>
<id>c7bbe4729dc53ddf3a02a7ae3816ec3c146d452e</id>
<content type='text'>
This avoids forgetting to add opcodes to coq_fix_code.c, and thus prevents
arities being mistakenly set to zero.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This avoids forgetting to add opcodes to coq_fix_code.c, and thus prevents
arities being mistakenly set to zero.
</pre>
</div>
</content>
</entry>
<entry>
<title>Add kernel/float64.ml to gitignore</title>
<updated>2020-11-04T19:14:46+00:00</updated>
<author>
<name>Pierre Roux</name>
</author>
<published>2020-10-30T14:15:09+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=814c16e348165cb19f70105dcf5d47e28f02c25e'/>
<id>814c16e348165cb19f70105dcf5d47e28f02c25e</id>
<content type='text'>
This is a generated file since #13147
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This is a generated file since #13147
</pre>
</div>
</content>
</entry>
<entry>
<title>Remove outdated references to productionlist.</title>
<updated>2020-09-11T10:39:39+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2020-09-11T10:39:39+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=795af932ef6606ba8385448244f60c728e9abdbd'/>
<id>795af932ef6606ba8385448244f60c728e9abdbd</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Fix .gitignore after the merge of #12849.</title>
<updated>2020-08-27T15:01:59+00:00</updated>
<author>
<name>Pierre-Marie Pédrot</name>
</author>
<published>2020-08-27T15:01:59+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=dac417a38dee2ce5800e8f66406bd08838535dc0'/>
<id>dac417a38dee2ce5800e8f66406bd08838535dc0</id>
<content type='text'>
A stray generated file was forgotten.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
A stray generated file was forgotten.
</pre>
</div>
</content>
</entry>
<entry>
<title>Add a generated file to .gitignore</title>
<updated>2020-06-21T04:19:03+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2020-06-21T04:19:03+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=6e60934263e8e52fc6212a7c9fc0d6b243098b09'/>
<id>6e60934263e8e52fc6212a7c9fc0d6b243098b09</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Move CoqIDE to its own folder</title>
<updated>2020-06-02T16:53:33+00:00</updated>
<author>
<name>Maxime Dénès</name>
</author>
<published>2020-05-16T15:07:37+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=33021618a06a94563d28691940f02a55bd9d358d'/>
<id>33021618a06a94563d28691940f02a55bd9d358d</id>
<content type='text'>
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
</pre>
</div>
</content>
</entry>
<entry>
<title>[dune] [stdlib] Build the standard library natively with Dune.</title>
<updated>2020-04-11T21:45:18+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2019-03-22T05:33:49+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=5db591257070734439dd5550995d6d3f497256c0'/>
<id>5db591257070734439dd5550995d6d3f497256c0</id>
<content type='text'>
This completes a pure Dune bootstrap of Coq.

There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.

TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.

Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This completes a pure Dune bootstrap of Coq.

There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.

TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.

Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?
</pre>
</div>
</content>
</entry>
<entry>
<title>Merge PR #11633: Add doc/unreleased.rst to .gitignore.</title>
<updated>2020-02-20T12:59:44+00:00</updated>
<author>
<name>Gaëtan Gilbert</name>
</author>
<published>2020-02-20T12:59:44+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=01f8d7666b282b0913ddc266d842d986e12976fa'/>
<id>01f8d7666b282b0913ddc266d842d986e12976fa</id>
<content type='text'>
Reviewed-by: SkySkimmer
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Reviewed-by: SkySkimmer
</pre>
</div>
</content>
</entry>
</feed>
