| Commit message (Collapse) | Author | Age |
|\
| |
| |
| | |
camlp4
|
| |
| |
| |
| | |
longer use camlp4.
|
|\ \ |
|
| |/ |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This fixes #6350 (and even comes with a test case).
Refering to other directories as `-R … ""` is maybe not best practice,
but some people out there do it, so as long as it does not cause too
much trouble, we can continue to support it.
|
|\ \ \
| |/ /
|/| |
| | | |
links (#6697)
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| |
| | |
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.
As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
|
|/ |
|
|\ |
|
| | |
|
| | |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
This should help with #5675, in particular with
https://github.com/coq/coq/issues/5675#issuecomment-349716292
|
|/ /
| |
| |
| |
| | |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
|\ \
| | |
| | |
| | | |
possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
|
| | | |
|
| |/
|/| |
|
| |
| |
| |
| |
| | |
This allows to fix the non-printing of error messages produced when
parsing arguments.
|
| |
| |
| |
| | |
This was apparently either silently doing nothing or failing.
|
| |
| |
| |
| |
| |
| |
| |
| | |
Nevertheless making option -o of coq_makefile recommended as discussed
in PR#6040.
This is one way to resolve the inconsistency with the usage which says
that all arguments are optional.
|
|\ \ |
|
| | | |
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
`make clean`.
|
| |_|/ / / /
|/| | | | | |
|
| | |_|_|/
| |/| | |
| | | | |
| | | | | |
Was lost during the coq_makefile 1 -> 2 translation.
|
| |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
|\ \ \ |
|
| |_|/
|/| | |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | | |
Fixes #6120.
|
|/ / /
| | |
| | |
| | | |
Previously, it was reverse-ordering timing diffs.
|
| |/
|/|
| |
| | |
Fixes #4988.
|
|/
|
|
|
|
|
| |
As it is, running a `Makefile.coq` on Windows produces the following error:
`cut: ': No such file or directory`
Changing to double quotes fixes this.
|
|
|
|
| |
4.02.3 has been the minimal OCaml version for a while now.
|
|\
| |
| |
| | |
directory` on every execution
|
| |
| |
| |
| | |
execution
|
|\ \ |
|
| |/ |
|
|/
|
|
|
|
|
|
|
| |
We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:
```
./configure -flambda-opts "-O3 -unbox-closures"
```
|
|
|
|
|
| |
This allows the timing aggregation scripts to handle logs from Travis,
which, for some reason, seems to insert trailing spaces.
|
|\
| |
| |
| | |
to escape non-UTF-8 file names)
|
|\ \
| | |
| | |
| | | |
coq_makefile are in sync (supersed #1039)…
|
| | | |
|
|\ \ \
| | | |
| | | |
| | | | |
proof for coqwc
|
|\ \ \ \ |
|