coq/clib, branch master The formal proof system 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.
[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.
Fast path in tclPROGRESS. 2020-12-11T17:28:05+00:00 Pierre-Marie Pédrot 2020-12-11T17:21:49+00:00 cade097ff6e5670b5f4c3ea832b593cf88251fbd We first check that the list of goals have the same length before trying to engage into potentially costly equality checks. 
We first check that the list of goals have the same length before trying to
engage into potentially costly equality checks.
Micro-optimizations of the tight loop in Hashset. 2020-11-29T16:34:04+00:00 Pierre-Marie Pédrot 2020-11-28T13:00:17+00:00 d3777b586419c676c0b78fe135cd3d264538fd3c 






Adding Array.iter3.
2020-11-16T19:08:26+00:00

Hugo Herbelin

2020-09-05T17:41:37+00:00

213207a1612d311f2f60d7e498ebd53a13ce039b












Merge PR #13226: Restore the List.Smart.map original implementation.
2020-10-27T20:33:46+00:00

coqbot-app[bot]

2020-10-27T20:33:46+00:00

96354508a50f12a2af49bd95073c6a24cea69713

Reviewed-by: gares





Reviewed-by: gares







Restore the List.Smart.map original implementation.
2020-10-19T13:48:28+00:00

Pierre-Marie Pédrot

2020-10-19T13:44:19+00:00

dcb325fd6ef432cd3717264c1547b94c7da2f396

Commit 56ff0c9 mangled the code claiming to make it tail-rec, but this is not
the case. In addition to make the code convoluted it also over-allocates for
nothing and breaks the write barrier for fun.

We simply rollback to the (slightly cleaned-up) previous code, that was simpler,
likely faster, and as much tail-rec as the one introduced in 56ff0c9.





Commit 56ff0c9 mangled the code claiming to make it tail-rec, but this is not
the case. In addition to make the code convoluted it also over-allocates for
nothing and breaks the write barrier for fun.

We simply rollback to the (slightly cleaned-up) previous code, that was simpler,
likely faster, and as much tail-rec as the one introduced in 56ff0c9.







Avoid magic numbers
2020-10-03T18:53:32+00:00

Jim Fehrle

2020-10-03T18:53:32+00:00

71fe84d0d6dc8e646332cc5790308de2f8f0fdab












[lib] make canonical_path_name always absolute (fix #13031)
2020-09-18T11:59:30+00:00

Enrico Tassi

2020-09-18T11:59:30+00:00

2b258e90df02448341c051ac21b84cf1c7c20428












[numeral] [plugins] Switch from `Big_int` to ZArith.
2020-08-27T17:03:33+00:00

Emilio Jesus Gallego Arias

2018-10-16T12:55:30+00:00

094e4649c29e2426daca0476c140439de901dafe

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 <Vincent.Laporte@fondation-inria.fr>





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 <Vincent.Laporte@fondation-inria.fr>