coq/doc/stdlib/dune, branch master The formal proof system [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.
Build and install refman with Dune. 2020-03-20T09:38:40+00:00 Théo Zimmermann 2020-03-18T15:07:19+00:00 80f3011eb5ca479b9b1f059c0f04e131028d5312 






[build] Consolidate stdlib's .v files under a single directory.
2020-02-13T20:12:03+00:00

Emilio Jesus Gallego Arias

2020-02-05T16:46:07+00:00

9193769161e1f06b371eed99dfe9e90fec9a14a6

Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.

This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.

We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.

Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.

This could also imply a performance gain as we now effectively
traverse less directories when locating a library.

See also discussion in #10003





Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.

This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.

We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.

Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.

This could also imply a performance gain as we now effectively
traverse less directories when locating a library.

See also discussion in #10003







[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]
2020-01-17T17:02:33+00:00

Emilio Jesus Gallego Arias

2020-01-17T00:25:06+00:00

a47e2f6587e3507a12d4d86b9769b93e01023350

This partially fixes #10139 ; we now build the Ltac2 documentation and
deploy it.

The fix here can be used for inspiration to do the make-based part.





This partially fixes #10139 ; we now build the Ltac2 documentation and
deploy it.

The fix here can be used for inspiration to do the make-based part.







[dune] Simple rule to generate Stdlib's documentation.
2019-02-26T20:49:13+00:00

Emilio Jesus Gallego Arias

2019-02-25T08:27:58+00:00

07ce2588740f689fe92a8d00dd1aeccda5255130

Ideally this will be handled by Dune's native library support, but
this could be useful for the likes of #9648.

I am not sure what should be done w.r.t. style files.





Ideally this will be handled by Dune's native library support, but
this could be useful for the likes of #9648.

I am not sure what should be done w.r.t. style files.