| Commit message (Collapse) | Author | Age |
... | |
| |_|/ / / /
|/| | | | | |
|
| | |_|_|/
| |/| | |
| | | | |
| | | | | |
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
|
|\ \ \ \ |
|
| |/ / /
|/| | | |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| | | | | | |
|
| | |/ / /
| |/| | | |
|
|/ / / / |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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).
|
|/ / / |
|
|\ \ \
| |/ /
|/| | |
|
| |/
|/| |
|
|\ \ |
|
|\ \ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
|\ \ \ \ |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
CAMLPKGS is now used to hold extra findlib -packages
The previous solution was to use CAMLFLAGS but since 4.05 an
invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx`
fails saying that `useless.cmxa` is not a compilation unit description.
CAMLPKGS is used in all `ocamlopt` invocations but for the one
performing the packing.
|
| |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The build chain is always
ml -> cmo -> cma
ml -> cmx -> cmxa -> cmxs
If we are packing, then it becomes
ml -> cmo \
ml -> cmo --> cmo -> cma
ml -> cmo /
ml -> cmxo \
ml -> cmxo --> cmxo -> cmxa -> cmxs
ml -> cmxo /
The interest of always having a .cma or .cmxa is that such file can
carry linking flags, that in findlib terms means which
-package was use to build the plugin.
|
| | | |
| | | |
| | | |
| | | | |
Fixes BZ#5700
|
| | |/ |
|
| |/
|/|
| |
| | |
URLs on Windows are the same as on Unix, they use / not \.
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
wrongly tagged as keywords
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Make sure that when plugin writer does not use -bypass-API,
API is opened by default.
|
| |/ /
|/| |
| | |
| | | |
On NixOS in particular, /usr/bin/time doesn't exist.
|