coq/sysinit, branch master The formal proof system noglob/dumpglob should be in coqc specific usage 2021-03-11T18:57:38+00:00 Gaëtan Gilbert 2021-03-11T18:57:38+00:00 52cc1e4d8574f6738caa1f7bf19bdd1945e5537e Fix #13930 
Fix #13930
[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 #13202: Infrastructure for fine-grained debug flags 2021-02-25T16:46:41+00:00 coqbot-app[bot] 2021-02-25T16:46:41+00:00 24e94b3dac66510e6d57b9f55f9a4e3e84fd6e54 Reviewed-by: gares Ack-by: herbelin Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer Ack-by: ejgallego 
Reviewed-by: gares
Ack-by: herbelin
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Ack-by: ejgallego
Infrastructure for fine-grained debug flags 2021-02-24T14:09:15+00:00 Maxime Dénès 2020-10-15T13:31:51+00:00 068031ff7da092c1e2d35db27d713b9606960c42 






Get rid of the compilation date from the binaries to make them more stable.
2021-02-16T08:02:37+00:00

Guillaume Melquiond

2021-02-16T08:02:37+00:00

31e205ae752c5189143ef9ce87a3536db0cdeb62

Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".





Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".







Merge PR #13821: Properly handle ordering of -w and -native-compiler
2021-02-10T15:05:49+00:00

coqbot-app[bot]

2021-02-10T15:05:49+00:00

7ac95ead2c2c7f905ffbdd395e9ffb1fbf76c4d3

Reviewed-by: gares





Reviewed-by: gares







Remove deprecated -inputstate command line argument
2021-02-04T14:30:30+00:00

Gaëtan Gilbert

2021-02-04T11:25:17+00:00

2edd93eec8e9bd83da2bbb77a904bb290ee7adf3

Deprecated since 6dd9e003c289a79b0656e7c6f2cc59935997370c (2014)





Deprecated since 6dd9e003c289a79b0656e7c6f2cc59935997370c (2014)







Remove deprecated -sprop-cumulative command line argument
2021-02-04T14:30:29+00:00

Gaëtan Gilbert

2021-02-04T11:22:59+00:00

df7d00971e430468cbf57fa6119b7ed5149a9193

Deprecated since #12034 (8.12)





Deprecated since #12034 (8.12)







Properly handle ordering of -w and -native-compiler
2021-02-04T11:21:12+00:00

Gaëtan Gilbert

2021-02-04T11:14:32+00:00

74aabc032014b0b83f2d54996dbb76cb5a78ea4d

Warnings are handled as injection commands, interleaved with options
and requires. Native compiler impacts require, so we must convert
"yes" to "no" before handling injections. As such the semantic
handling of the native command line argument must be separated from
the emission of the warning message, which this PR implements.

Fix #13819

In principle the other 2 cwarning in coqargs
(deprecated spropcumul and inputstate) should be moved to injections
too, but since they're deprecated I can't be bothered.





Warnings are handled as injection commands, interleaved with options
and requires. Native compiler impacts require, so we must convert
"yes" to "no" before handling injections. As such the semantic
handling of the native command line argument must be separated from
the emission of the warning message, which this PR implements.

Fix #13819

In principle the other 2 cwarning in coqargs
(deprecated spropcumul and inputstate) should be moved to injections
too, but since they're deprecated I can't be bothered.







make the linter happy
2021-01-27T08:45:49+00:00

Enrico Tassi

2021-01-06T18:57:08+00:00

6e258b391363aa2345c4dc265ba381b1712fe083