| Commit message (Collapse) | Author | Age |
|\ |
|
| | |
|
|\ \
| |/
|/| |
|
|\ \ |
|
| | | |
|
|/ / |
|
|/ |
|
|\ |
|
| | |
|
|/ |
|
| |
|
| |
|
| |
|
|
|
|
| |
Note that we don't look inside -arg for eg -coqlib.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We fix as suggested by @JasonGross by reading file names from the
_CoqProject when coq_makefile was invoked with one.
I made coqdep only look at the .v files from _CoqProject because it's
easier this way. Since we're going through the _CoqProject parser we
could have coqdep understand more of it but let's leave that to
another PR (and maybe someone else).
Some projects pass vfiles on the command line, we keep the list of
these files to pass them to coqdep via command line even when there is
a _CoqProject.
Multiple project files is probably broken.
|
|\
| |
| |
| | |
camlp4
|
| |
| |
| |
| | |
longer use camlp4.
|
|\ \ |
|
| |/ |
|
|/ |
|
|\ |
|
| |
| |
| |
| |
| | |
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.
|
|\ |
|
| | |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
`make clean`.
|
| |/ / /
|/| | | |
|
| | | |
| | | |
| | | |
| | | | |
Was lost during the coq_makefile 1 -> 2 translation.
|
| |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
|/
|
|
|
|
|
| |
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.
|
|
|
|
| |
execution
|
|\
| |
| |
| | |
coq_makefile are in sync (supersed #1039)…
|
| | |
|
| |
| |
| |
| |
| |
| | |
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.
|
|/ |
|
|\ |
|
| |
| |
| |
| |
| | |
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.
|