coq/engine, branch master The formal proof system More efficient variable membership check for Logic.move. 2021-04-20T08:54:34+00:00 Pierre-Marie Pédrot 2020-12-24T19:27:42+00:00 9caadc38de0e1c7b3362081da9482fc4455220a7 Instead of repeatedly crawling the same hypothesis again and again we only iter the term once. 
Instead of repeatedly crawling the same hypothesis again and again we
only iter the term once.
Remove remote counter system 2021-04-14T10:54:38+00:00 Gaëtan Gilbert 2021-03-26T14:34:59+00:00 3efee577b4c92b38a987b40e555fae2c0a2023c4 






Put async worker id in universe names
2021-04-14T10:54:05+00:00

Gaëtan Gilbert

2021-04-01T17:35:27+00:00

004bf5770bdcdd1b35dd27f683c733505823e741

This removes the need for the remote counter.





This removes the need for the remote counter.







Remove unused UnivProblem.Set.subst_univs
2021-04-06T11:30:13+00:00

Gaëtan Gilbert

2021-04-06T11:30:13+00:00

e7c29762b995827288f09f7ad736185fb090d39c












Fix a bug in UnivProblem
2021-03-31T23:33:33+00:00

Matthieu Sozeau

2021-03-31T23:33:33+00:00

65f0b34c9740788270b48700a7ce2b5338ba1f64












[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.







Further simplification of the term replacing code.
2021-03-12T12:39:03+00:00

Pierre-Marie Pédrot

2021-03-06T22:32:45+00:00

285419e99996354ad2056bc38725c7a592124e7c

We factorize the code for replace and subst, since it seems there is no
reason to keep them separate, not even performance. Some static invariants are
made explicit in the API.





We factorize the code for replace and subst, since it seems there is no
reason to keep them separate, not even performance. Some static invariants are
made explicit in the API.







Algorithmically faster algorithm for term replacing.
2021-03-12T12:37:37+00:00

Pierre-Marie Pédrot

2021-03-06T21:54:16+00:00

93ea9206cbf29617feb23646f95e794b11e87793

Instead of recomputing the n-th lifts of terms for every subterm under a context,
we introduce a table storing the value of this lift across contexts. While not
the most efficient algorithmically, it is still much more efficient in practice and
does not exhibit the exponential behaviour of replacing under different subcontexts.

In an ideal world we would have an equality function on terms that allows to compute
equality up to lifts, which would prevent having to even compute the lift at all, but
the current fix has the advantage to be self-contained and not require dangerous
tweaking of an equality function which is already complex enough as it is.

Fixes #13896: cbn very slow.





Instead of recomputing the n-th lifts of terms for every subterm under a context,
we introduce a table storing the value of this lift across contexts. While not
the most efficient algorithmically, it is still much more efficient in practice and
does not exhibit the exponential behaviour of replacing under different subcontexts.

In an ideal world we would have an equality function on terms that allows to compute
equality up to lifts, which would prevent having to even compute the lift at all, but
the current fix has the advantage to be self-contained and not require dangerous
tweaking of an equality function which is already complex enough as it is.

Fixes #13896: cbn very slow.







[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.







Use make_case_or_project in auto_ind_decl
2021-02-17T12:56:27+00:00

Gaëtan Gilbert

2021-02-17T12:56:27+00:00

441bace297a4c31e5003cec93e46e6a47fa684d3

Towards #5154 (but insufficient)





Towards #5154 (but insufficient)