coq/lib, branch master The formal proof system Locations: Moving functions Ploc.sub and Ploc.after to loc.ml. 2021-04-23T13:34:29+00:00 Hugo Herbelin 2021-04-05T14:24:39+00:00 52a71bf2b1260ce8f8622878c82caec54d298808 






LStream: a library for streams with non-canonical locations.
2021-04-23T13:34:29+00:00

Hugo Herbelin

2021-04-05T14:23:35+00:00

a24d1a15858df9574e491bf952a59e700cc75ecc












Remove remote counter system
2021-04-14T10:54:38+00:00

Gaëtan Gilbert

2021-03-26T14:34:59+00:00

3efee577b4c92b38a987b40e555fae2c0a2023c4












Merge PR #14046: make critical sections safe in the presence of exceptions
2021-04-12T12:34:16+00:00

coqbot-app[bot]

2021-04-12T12:34:16+00:00

271445decd0fc1a37da3009f148f2e68c7168fe1

Reviewed-by: ejgallego
Ack-by: gares
Ack-by: SkySkimmer
Ack-by: gadmm





Reviewed-by: ejgallego
Ack-by: gares
Ack-by: SkySkimmer
Ack-by: gadmm







Make critical sections safe in the presence of exceptions
2021-04-09T19:05:43+00:00

Lasse Blaauwbroek

2021-04-01T07:18:00+00:00

520ac61dfe5a6e865cb7b10f4a822c0d72f3ded9

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.





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.







Make description of Pp.pr_enum more precise + spacing in pp.ml.
2021-04-06T15:40:53+00:00

Hugo Herbelin

2020-10-05T22:42:08+00:00

524eb4e7dcb18d622ebb99648862e5d08a972117












[flags] [profile] Remove bit-rotten CProfile code.
2021-03-30T13:37:00+00:00

Emilio Jesus Gallego Arias

2020-03-10T05:06:34+00:00

5d3c0a0326af68e85f1f1cfc6bfa2214b0052de8

As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.

It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.

We thus remove all bitrotten dead code.





As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.

It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.

We thus remove all bitrotten dead code.







Do not match on record types with mutable fields in function arguments.
2021-03-23T09:26:34+00:00

Guillaume Melquiond

2021-03-23T09:20:10+00:00

01b061f0082a70f66016e78075a5952af8ed5431

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} -> fun x -> ...





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} -> fun x -> ...







Properly support nested timeouts
2021-03-04T19:43:02+00:00

Lasse Blaauwbroek

2020-11-22T10:25:04+00:00

2da1eef317464036e3a122368508a5f3e4d21f6d












[build] Split stdlib to it's own opam package.
2021-03-03T15:06:14+00:00

Emilio Jesus Gallego Arias

2020-06-22T15:52:18+00:00

ab98d847d237af3cd0e46edef42218be65cfc98f

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.





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.