<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/plugins/nsatz, 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>Infrastructure for fine-grained debug flags</title>
<updated>2021-02-24T14:09:15+00:00</updated>
<author>
<name>Maxime Dénès</name>
</author>
<published>2020-10-15T13:31:51+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=068031ff7da092c1e2d35db27d713b9606960c42'/>
<id>068031ff7da092c1e2d35db27d713b9606960c42</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>[nsatz] num → zarith</title>
<updated>2020-08-27T17:03:33+00:00</updated>
<author>
<name>Vincent Laporte</name>
</author>
<published>2018-10-16T15:10:45+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=5a28133182c75292d9b2adc7826cba47e6a138a7'/>
<id>5a28133182c75292d9b2adc7826cba47e6a138a7</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[numeral] [plugins] Switch from `Big_int` to ZArith.</title>
<updated>2020-08-27T17:03:33+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2018-10-16T12:55:30+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=094e4649c29e2426daca0476c140439de901dafe'/>
<id>094e4649c29e2426daca0476c140439de901dafe</id>
<content type='text'>
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.

We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.

We thus keep the num library linked for now until all plugins are
ported.

Co-authored-by: Vincent Laporte &lt;Vincent.Laporte@fondation-inria.fr&gt;
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.

We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.

We thus keep the num library linked for now until all plugins are
ported.

Co-authored-by: Vincent Laporte &lt;Vincent.Laporte@fondation-inria.fr&gt;
</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>Update headers in the whole code base.</title>
<updated>2020-03-18T11:15:43+00:00</updated>
<author>
<name>Théo Zimmermann</name>
</author>
<published>2020-03-18T11:14:26+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=a99776e10e0b2198d2b811ad82631111fb450f8a'/>
<id>a99776e10e0b2198d2b811ad82631111fb450f8a</id>
<content type='text'>
Add headers to a few files which were missing them.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Add headers to a few files which were missing them.
</pre>
</div>
</content>
</entry>
<entry>
<title>[build] Consolidate stdlib's .v files under a single directory.</title>
<updated>2020-02-13T20:12:03+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2020-02-05T16:46:07+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=9193769161e1f06b371eed99dfe9e90fec9a14a6'/>
<id>9193769161e1f06b371eed99dfe9e90fec9a14a6</id>
<content type='text'>
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.

This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.

We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.

Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.

This could also imply a performance gain as we now effectively
traverse less directories when locating a library.

See also discussion in #10003
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.

This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.

We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.

Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.

This could also imply a performance gain as we now effectively
traverse less directories when locating a library.

See also discussion in #10003
</pre>
</div>
</content>
</entry>
<entry>
<title>Nsatz: use “lia” rather than “omega”</title>
<updated>2019-11-25T08:40:38+00:00</updated>
<author>
<name>Vincent Laporte</name>
</author>
<published>2019-10-28T12:54:01+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=b3fc3cbd36570b77af9f17237f30713be861c3ed'/>
<id>b3fc3cbd36570b77af9f17237f30713be861c3ed</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[coq] Untabify the whole ML codebase.</title>
<updated>2019-11-21T14:38:39+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2019-11-21T14:38:39+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=d016f69818b30b75d186fb14f440b93b0518fc66'/>
<id>d016f69818b30b75d186fb14f440b93b0518fc66</id>
<content type='text'>
We also remove trailing whitespace.

Script used:

```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We also remove trailing whitespace.

Script used:

```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
</pre>
</div>
</content>
</entry>
</feed>
