coq/test-suite/Makefile, branch master The formal proof system test-suite: add approve-coqdoc to update all coqdoc output files at once. 2021-04-23T13:00:57+00:00 Hugo Herbelin 2021-04-23T12:56:24+00:00 7e0c8172703111a026477cf704f50af9468f8f0a 






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







Merge PR #13248: Build all_stdlib.v in test suite makefile
2020-11-20T22:02:10+00:00

coqbot-app[bot]

2020-11-20T22:02:10+00:00

5b15fce17d856dfbd51482f724ddf5e5f9646073

Reviewed-by: ejgallego





Reviewed-by: ejgallego







[CI] Deactivate native-compiler for a few tests that fail with it
2020-11-20T18:08:08+00:00

Pierre Roux

2020-11-14T11:25:10+00:00

787c4583d685e4059c2a08cdb9fe0bbfa99e255e












Build all_stdlib.v in test suite makefile
2020-11-20T15:52:58+00:00

Gaëtan Gilbert

2020-10-22T13:30:30+00:00

76ab524320e3d4c006c6c94372e0cfda2b62c76e

instead of recursive make





instead of recursive make







Fix running unit tests with dune compiled coq
2020-11-10T13:25:39+00:00

Gaëtan Gilbert

2020-11-10T13:24:34+00:00

400f852347be1b038369878df997bf537ff1f3d0

(for runs outside dune, ie "make -C test-suite unit-tests" rather than
"dune build @runtest")

Fix #13333





(for runs outside dune, ie "make -C test-suite unit-tests" rather than
"dune build @runtest")

Fix #13333







Updated .csdp.cache.test-suite and minor fixes
2020-09-15T13:56:39+00:00

BESSON Frederic

2020-09-11T15:22:50+00:00

6b379b22f445c970237d815cbbbf9dfa33e055d2

-  merlin.in : added zarith
- test-suite/Makefile remove .csdp.cache on make clean

updated .csdp.cache.test-suite





-  merlin.in : added zarith
- test-suite/Makefile remove .csdp.cache on make clean

updated .csdp.cache.test-suite







Merge PR #12798: Change OUnit package name to ounit2.
2020-08-25T10:54:19+00:00

coqbot-app[bot]

2020-08-25T10:54:19+00:00

ba3ff67b1b680a7deb3fddacb7134d5e38228602

Reviewed-by: ejgallego





Reviewed-by: ejgallego







Merge PR #12835: Slightly reorganising the test suite to follow its documentation
2020-08-24T14:40:58+00:00

Hugo Herbelin

2020-08-24T14:40:58+00:00

d49b9f298e46df177400cae775a1c22879543456

Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: jfehrle





Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: jfehrle







Merge PR #12864: Improve `make approve-output`
2020-08-24T11:49:20+00:00

Gaëtan Gilbert

2020-08-24T11:49:20+00:00

f42b28ed0cfd200395a4a32fd1ebe6a7f73a7ddb

Reviewed-by: SkySkimmer





Reviewed-by: SkySkimmer