coq/tools/coqdoc/dune, branch master The formal proof system [dune] [coqdoc] Install coqdoc.sty also in share/texmf 2021-03-31T17:00:20+00:00 Emilio Jesus Gallego Arias 2021-03-31T17:00:20+00:00 3d40b663fbefecbeb5b23dd9656c5342269c284a 






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







Checking validity of coqdoc file name.
2020-05-11T19:56:00+00:00

Hugo Herbelin

2020-05-07T17:20:39+00:00

632f709b95f4fa47e86e5c498b995eb9c2cf2ff6

This fixes #12265 (javascript injection vulnerability in file name).





This fixes #12265 (javascript injection vulnerability in file name).







[dune] Add `(package coq)` scope to artifacts.
2018-10-03T18:55:47+00:00

Emilio Jesus Gallego Arias

2018-10-03T18:51:05+00:00

dc916f4d475f1661e72ce43a26320c268fcf034c

This will allow us to define extra packages such as `coq-refman`.





This will allow us to define extra packages such as `coq-refman`.







[dune] Install more files from `tools`.
2018-10-02T02:27:15+00:00

Emilio Jesus Gallego Arias

2018-10-02T02:20:33+00:00

b46668fa43bb97f7d696978f687db3c97224ce4f

These are needed for example for the test suite.





These are needed for example for the test suite.







[dune] Improve support for Coq tools.
2018-09-21T14:56:14+00:00

Emilio Jesus Gallego Arias

2018-09-21T02:16:42+00:00

ac38da8efc5bb9d046cb70a886edba8f31fcb600

- Install `CoqMakefile.in`
- Build `coqwc` and `coqdoc`

This allows to build most contribs I've tried with the Dune-based OPAM
package.





- Install `CoqMakefile.in`
- Build `coqwc` and `coqdoc`

This allows to build most contribs I've tried with the Dune-based OPAM
package.