coq/toplevel, branch master The formal proof system Relying on the abstract notion of streams with location for parsing. 2021-04-23T13:34:29+00:00 Hugo Herbelin 2021-04-05T14:40:10+00:00 e07efb3798c7c6ec54aac9093ab50fddfc6c6a5b We also get rid of ploc.ml, now useless, relying a priori on more robust code in lStream.ml for location reporting (see e.g. parse_parsable in grammar.ml). 
We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).
Add test for -schedule-vio-checking 2021-04-14T10:54:40+00:00 Gaëtan Gilbert 2021-04-06T11:26:31+00:00 8df5a37d934b4f862a6183ee451c6bb34ae72d94 Close #14074 
Close #14074
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.
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.
[coqc] Don't allow to pass more than one file to coqc 2021-02-26T21:57:53+00:00 Emilio Jesus Gallego Arias 2021-02-18T18:25:53+00:00 1cffe2f00d91bc9739b40887eb36f4bbad761c5f This has been in the TODO queue for a long time, and indeed I have recently seen some trouble with users passing two .v files to Coq, which it isn't a) tested, b) supported. Moreover, it doesn't even work correctly in 8.13 due to some other changes in the toplevel related to auxiliary files. (*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work 
This has been in the TODO queue for a long time, and indeed
I have recently seen some trouble with users passing two .v files to
Coq, which it isn't a) tested, b) supported.

Moreover, it doesn't even work correctly in 8.13 due to some other
changes in the toplevel related to auxiliary files.

(*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
Merge PR #13863: Get rid of the compilation date from the binaries to make them more stable. 2021-02-25T14:31:29+00:00 coqbot-app[bot] 2021-02-25T14:31:29+00:00 6ef58b0e9348d49ccf456d9fd475368c3dc1aafa Reviewed-by: SkySkimmer Reviewed-by: gares 
Reviewed-by: SkySkimmer
Reviewed-by: gares
Merge PR #13865: [coqtop] be verbose only in interactive mode 2021-02-19T14:37:51+00:00 coqbot-app[bot] 2021-02-19T14:37:51+00:00 a2938972537389b9813794147412f51494f48dd1 Reviewed-by: silene Ack-by: SkySkimmer 
Reviewed-by: silene
Ack-by: SkySkimmer
[coqtop] be verbose only in interactive mode 2021-02-16T18:54:12+00:00 Enrico Tassi 2021-02-16T10:00:47+00:00 57030f36d88800004a5bf9d0581d23f60daddad9 






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