coq/Makefile.vofiles, branch master The formal proof system Update headers in the whole code base. 2020-03-18T11:15:43+00:00 Théo Zimmermann 2020-03-18T11:14:26+00:00 a99776e10e0b2198d2b811ad82631111fb450f8a Add headers to a few files which were missing them. 
Add headers to a few files which were missing them.
[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
Merge PR #10977: Remove the incorrect extra space in Makefile.vofiles 2019-12-29T16:02:20+00:00 Enrico Tassi 2019-12-29T16:02:20+00:00 99b064d1079f62bdabfd7374ae77246828e8b08d Reviewed-by: gares 
Reviewed-by: gares
Split up stdlib install command (too long) 2019-12-13T12:12:20+00:00 Gaëtan Gilbert 2019-11-26T22:01:55+00:00 dfb92f3476fff0b329590626790d83a2f9e3e058 






[make] install .vos along with .vo
2019-11-01T11:17:07+00:00

Enrico Tassi

2019-10-28T10:23:54+00:00

69657170aa1ac065765de00411e04400942ae28a












Remove the incorrect extra space in Makefile.vofiles
2019-10-28T03:20:38+00:00

scinart

2019-10-28T03:05:13+00:00

5d143285677704a406b059aba392a5cf304c67d6

Which results in extra space in filenames when compiling.





Which results in extra space in filenames when compiling.







Fix PLUGINSVO computation after ltac2 integration
2019-05-07T12:57:13+00:00

Gaëtan Gilbert

2019-05-07T12:56:51+00:00

86fa401ceaa17bdf1d297808eff3f8c3792d2778

Avoid looking at random installed packages in -local mode.





Avoid looking at random installed packages in -local mode.







Integrate build and documentation of Ltac2
2019-05-07T08:02:56+00:00

Maxime Dénès

2019-04-25T12:09:42+00:00

9779c0bf4945693bfd37b141e2c9f0fea200ba4d

Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.

Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.





Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.

Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.







Makefiles: Fixes for byte compilation
2019-02-06T10:17:49+00:00

Gaëtan Gilbert

2019-02-05T14:34:49+00:00

f29aa6720eba884533972530b4283bf19d8410aa

- default targets don't depend on ocamlopt when it's unavailable
- coqc.byte is built by byte target and coqc by coqbinaries target
- unit tests use best ocaml
- poly-capture-global-univs tests ml compilation with ocamlc
- don't try to install .cmx and native-compute .o files

cf https://github.com/coq/coq/issues/9464





- default targets don't depend on ocamlopt when it's unavailable
- coqc.byte is built by byte target and coqc by coqbinaries target
- unit tests use best ocaml
- poly-capture-global-univs tests ml compilation with ocamlc
- don't try to install .cmx and native-compute .o files

cf https://github.com/coq/coq/issues/9464







[make] support for QUICK
2019-01-10T15:39:49+00:00

Enrico Tassi

2019-01-10T09:45:20+00:00

ac72003e5f068b9cc7f521c45e497736ef4f0560

The variable QUICK enables the quick compilation chain:
- all v files are compiled with -quick to vio files (also
  -native-compiler no, since it is quicker)
- then all vio files are turned to vo files $NJOBS at a time

All occurrences of .vo use now .$(VO) that can be either
.vo or .vio depending of QUICK being defined. Targets that
only make sense for .vo files have to use $(VAR:.$(VO)=.vo)





The variable QUICK enables the quick compilation chain:
- all v files are compiled with -quick to vio files (also
  -native-compiler no, since it is quicker)
- then all vio files are turned to vo files $NJOBS at a time

All occurrences of .vo use now .$(VO) that can be either
.vo or .vio depending of QUICK being defined. Targets that
only make sense for .vo files have to use $(VAR:.$(VO)=.vo)