| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Up to this point the `lib` directory contained two different library
archives, `clib.cma` and `lib.cma`, which a rough splitting between
Coq-specific libraries and general-purpose ones.
We know split the directory in two, as to make the distinction clear:
- `clib`: contains libraries that are not Coq specific and implement
common data structures and programming patterns. These libraries
could be eventually replace with external dependencies and the rest
of the code base wouldn't notice much.
- `lib`: contains Coq-specific common libraries in widespread use
along the codebase, but that are not considered part of other
components. Examples are printing, error handling, or flags.
In some cases we have coupling due to utility files depending on Coq
specific flags, however this commit doesn't modify any files, but only
moves them around, further cleanup is welcome, as indeed a few files
in `lib` should likely be placed in `clib`.
Also note that `Deque` is not used ATM.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Enable builds on Windows by removing Windows-style endings where it impacts make.
The fix in Makefile.build is a band-aid fix; maximedenes said he would remove the dependency on sed and awk here.
|
| | |/ / |
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
We move the main async flags to the STM in preparation for
more state encapsulation.
There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
When statically linking plugins, the "DECLARE PLUGIN" macro takes care
of properly setting up the loaded module table.
This setup was also done by `coqmktop`, thus in order to ease
bisecting, we didn't take care of it in the `coqmktop` deprecation.
Fixes #6364.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.
This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.
An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.
We also perform some smaller cleanups taking profit from ocamlfind.
|
| |/
|
|
|
| |
This allows us to enforce that it works without breaking the build
when it doesn't.
|
| |
|
|
| |
Mismatch probably caused by c5aca4005.
|
| |\
| |
| |
| | |
structure.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The test was abandoned at the time of merging subdirectory browsing
between coqdep and coqtop, and to limit at the same time the
dependency of coqdep in files such as unicode.cmo.
But checking ident validity speeds up browsing in arbitrary directory
structure and we restore it for this reason.
(One could also say that browsing arbitrary directory structures is
not intended, but in practice this may happen, as e.g. reported in
BZ#5734.)
|
| |/
|
|
|
|
|
|
|
| |
We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:
```
./configure -flambda-opts "-O3 -unbox-closures"
```
|
| |
|
|
|
|
|
| |
Specifically since e88dfedd99a84e9e375f3583be6fd1de3de36c72.
There seem to have been no actual errors due to this, only ocaml
complaining about missing .cmi files.
|
| |\
| |
| |
| | |
to escape non-UTF-8 file names)
|
| | |
| |
| |
| |
| |
| | |
E.g. -safe-string is set by configure.ml and made available to
both make (via config/Makefile) and coq_makefile (via
config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in).
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| | |/
|/|
| |
| | |
coq-makefile's tests do depend on this
|
| | |
| |
| |
| | |
On NixOS in particular, /usr/bin/time doesn't exist.
|
| |/
|
|
|
|
|
|
| |
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
|
| |\ |
|
| |\ \ |
|
| | |/
|/|
| |
| | |
It is empty and not used anymore.
|
| | | |
|
| |\ \ |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This commit adds timing scripts from
https://github.com/JasonGross/coq-scripts/tree/master/timing into the
tools folder, and integrates them into coq_makefile and Coq's makefile.
The main added makefile targets are:
- the `TIMING` variable - when non-empty, this creates for each built
`.v` file a `.v.timing` variable (or `.v.before-timing` or
`.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively)
- `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of
sorted timings at the end, saving it to `time-of-build-pretty.log`
- `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after
TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file
`time-of-build-before.log` or `time-of-build-after.log`, respectively
- `print-pretty-timed-diff` - prints a table with the difference between
the logs recorded by `make-pretty-timed-before` and
`make-pretty-timed-after`, saving the table to
`time-of-build-both.log`
- `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a
table with the differences between two `.v.timing` files, and saves
the output to `time-of-build-pretty.log`
- `*.v.timing.diff` - this saves the result of
`print-pretty-single-time-diff` for each target to the
`.v.timing.diff` file
- `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's
own Makefile) - makes all `*.v.timing.diff` targets
N.B. We need to make `make pretty-timed` fail if `make` fails. To do
this, we need to get around the fact that pipes swallow exit codes.
There are a few solutions in
https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make;
we choose the temporary file rather than requiring the shell of the
makefile to be bash.
|
| |/ /
| |
| |
| | |
This closes [bug #5596](https://coq.inria.fr/bugs/show_bug.cgi?id=5596).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This should help preventing weird compilation failures due to leftover
object files after deleting or moving some source files
By the way:
- use plain $(filter-out ...) instead of a 'diff' macro (thanks Jason
for the suggestion)
- rename FIND_VCS_CLAUSE into FIND_SKIP_DIRS since it contains more
than version control stuff nowadays
|
| |/
|
|
| |
This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619)
|
| |
|
|
|
|
|
|
| |
Due to the recent conversion of many .mli-only files into .ml files
(hugely debatable impact of the API introduction), parallel make may
fail badly again (always the same race between ocamlc and ocamlopt for .cmi).
Still working on a proper fix, but meanwhile let's reintroduce the
old hacks against these corruptions.
|
| |
|
|
|
|
|
| |
of this file
There is now a warning if the content of micromega.ml isn't what MExtraction.v would
produce.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
| |
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
|
| |
|
|
| |
generate them later.
|
| |\ |
|
| | | |
|
| |\ \
| | |
| | |
| | | |
"plugins/micromega/MExtraction.v"
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
"plugins/micromega/MExtraction.v"
|
| |/ / |
|
| | |
| |
| |
| |
| |
| |
| | |
This allows to grant a wish by Hugo: to build coqtop.byte and prelude
with it, you could do:
make -j BEST=byte states
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
On a machine for which ocamlopt is available, the make world will now
perform bytecode compilation only in grammar/ (up to the syntax
extension grammar.cma), and then exclusively use ocamlopt.
In particular, make world do not build bin/coqtop.byte.
A separate rule 'make byte' does it, as well as bytecode plugins and
things like dev/printers.cma.
'make install' deals only with the part built by 'make', while a new
rule 'make install-byte' installs the part built by 'make byte'.
IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any
parallel mix of native and byte rules. These are known to crash sometimes,
see below. Instead, do rather 'make -j && make -j byte'.
Indeed, apart from marginal compilation speed-up for users not interested
in byte versions, the main reason for this commit is to discourage any
simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and
ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli,
and in case of parallel build this may happen at the very moment another
ocaml(c|opt) is accessing this .cmi. Until now, this issue has been
handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in
Makefile.build). But these hacks weren't obvious to extend to ocamlopt
-pack vs. ocamlopt -pack.
coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML
Module influences the .v.d dependency file. Possible values are:
-dyndep opt : regular situation now, depends only on .cmxs
-dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a)
-dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs
-dyndep none : interesting for coqtop with statically linked plugins
-dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d
instead of extensions .cm*, so that the choice is made in the rest of the
makefile (see a future commit about coq_makefile)
NB: two extra mli added to avoid building unecessary .cmo during 'make world',
without having to use the ocamldep -native option.
NB: we should state somewhere that coqmktop -top won't work unless
'make byte' was done first
|
Enrico Tassi
Emilio Jesus Gallego Arias
Maxime Dénès
Jim
Gaëtan Gilbert
Hugo Herbelin
Théo Zimmermann
Matej Košík
Jason Gross
Pierre Letouzey
Matej Kosik
Gaëtan Gilbert