<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/stm, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>Remove remote counter system</title>
<updated>2021-04-14T10:54:38+00:00</updated>
<author>
<name>Gaëtan Gilbert</name>
</author>
<published>2021-03-26T14:34:59+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=3efee577b4c92b38a987b40e555fae2c0a2023c4'/>
<id>3efee577b4c92b38a987b40e555fae2c0a2023c4</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Make critical sections safe in the presence of exceptions</title>
<updated>2021-04-09T19:05:43+00:00</updated>
<author>
<name>Lasse Blaauwbroek</name>
</author>
<published>2021-04-01T07:18:00+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=520ac61dfe5a6e865cb7b10f4a822c0d72f3ded9'/>
<id>520ac61dfe5a6e865cb7b10f4a822c0d72f3ded9</id>
<content type='text'>
We introduce the `with_lock` combinator that locks a mutex in an atomic fashion.
This ensures that exceptions thrown by signals will not leave the system in a
deadlocked state.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We introduce the `with_lock` combinator that locks a mutex in an atomic fashion.
This ensures that exceptions thrown by signals will not leave the system in a
deadlocked state.
</pre>
</div>
</content>
</entry>
<entry>
<title>Do not match on record types with mutable fields in function arguments.</title>
<updated>2021-03-23T09:26:34+00:00</updated>
<author>
<name>Guillaume Melquiond</name>
</author>
<published>2021-03-23T09:20:10+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=01b061f0082a70f66016e78075a5952af8ed5431'/>
<id>01b061f0082a70f66016e78075a5952af8ed5431</id>
<content type='text'>
This tends to confuse the OCaml compiler, for good reasons. Indeed, if
there are mutable fields, the generated code cannot wait for the function
to be fully applied. It needs to recover the value of the mutable fields
as early as possible, and thus to create a closure.

Example:

    let foo {bar} x = ...

is compiled as

    let foo y = match y with {bar} -&gt; fun x -&gt; ...
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This tends to confuse the OCaml compiler, for good reasons. Indeed, if
there are mutable fields, the generated code cannot wait for the function
to be fully applied. It needs to recover the value of the mutable fields
as early as possible, and thus to create a closure.

Example:

    let foo {bar} x = ...

is compiled as

    let foo y = match y with {bar} -&gt; fun x -&gt; ...
</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>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>make the linter happy</title>
<updated>2021-01-27T08:45:49+00:00</updated>
<author>
<name>Enrico Tassi</name>
</author>
<published>2021-01-06T18:57:08+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=6e258b391363aa2345c4dc265ba381b1712fe083'/>
<id>6e258b391363aa2345c4dc265ba381b1712fe083</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[sysinit] move initialization code from coqtop to here</title>
<updated>2021-01-27T08:45:49+00:00</updated>
<author>
<name>Enrico Tassi</name>
</author>
<published>2021-01-06T13:19:59+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=4c4d6cfacf92b555546055a45edc19b68245b83c'/>
<id>4c4d6cfacf92b555546055a45edc19b68245b83c</id>
<content type='text'>
We also spill (some) non-generic arguments and initialization code
out of coqargs and to coqtop, namely colors for the terminal. There are
more of these, left to later commits.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We also spill (some) non-generic arguments and initialization code
out of coqargs and to coqtop, namely colors for the terminal. There are
more of these, left to later commits.
</pre>
</div>
</content>
</entry>
<entry>
<title>[sysinit] new component for system initialization</title>
<updated>2021-01-27T08:45:49+00:00</updated>
<author>
<name>Enrico Tassi</name>
</author>
<published>2021-01-05T10:34:35+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=4264aec518d5407f345c58e18e014e15e9ae96af'/>
<id>4264aec518d5407f345c58e18e014e15e9ae96af</id>
<content type='text'>
This component holds the code for initializing Coq:
- parsing arguments not specific to the toplevel
- initializing all components from vernac downwards (no stm)

This commit moves stm specific arguments parsing to stm/stmargs.ml
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
This component holds the code for initializing Coq:
- parsing arguments not specific to the toplevel
- initializing all components from vernac downwards (no stm)

This commit moves stm specific arguments parsing to stm/stmargs.ml
</pre>
</div>
</content>
</entry>
<entry>
<title>[vernac] move vernac_classifier to vernac</title>
<updated>2021-01-27T08:45:48+00:00</updated>
<author>
<name>Enrico Tassi</name>
</author>
<published>2020-09-25T12:04:53+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=4390b6907b3d07793c2e8f9e7ad3cc38d9488711'/>
<id>4390b6907b3d07793c2e8f9e7ad3cc38d9488711</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>[ltac] break dependency on the STM</title>
<updated>2021-01-27T08:45:48+00:00</updated>
<author>
<name>Enrico Tassi</name>
</author>
<published>2020-11-17T17:52:30+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=1fd4c22d493715f154f6b79dc7f6e4efd44ff185'/>
<id>1fd4c22d493715f154f6b79dc7f6e4efd44ff185</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
</feed>
