| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
- Remove inclusion of the `tactics` directory, this is coming from a
time loadable modules were found there, now all are under `plugins`.
- Remove 2 dependencies so we can bootstrap coqdep earlier.
- Use `Format` instead of `Printf` for printing.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
| |
Was introduced in 5268efdef, reverted then readded in 1be9c4d.
|
| |
|
|
|
|
|
|
|
| |
This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing
changes made to da99355b4d6de31aec5a660f7afe100190a8e683.
Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 next commit about coq_makedile)
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
|
| |\ |
|
| | | |
|
| |\|
| |
| |
| |
| | |
- Had to add a Sigma.to_evar_map
- Had to rework coqdep_common.ml{,i} and coqdep.ml
|
| | |
| |
| |
| |
| |
| |
| | |
Like coqc: detect if the current directory was set by options, if not: add
it with empty logical path.
TODO: check if coq_makefile is still correct wrt to this modification, I
think yes, actually it should end being more correct.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
The quadratic behaviour of list searching probably appears with small
enough samples. With the advent of usable libraries in Coq, and thus many
possible dependencies, better be safe than sorry.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
The search algorithm is not satisfactory though, as it crawls through
all known files to find the proper one. We should rather use some trie-based
data structure, but I'll leave this for a future commit.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error),
- uniformly expecting paths in Unix format and warning otherwise.
|
| | |
| |
| |
| |
| |
| | |
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
|
| |/
|
|
|
|
|
| |
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error).
|
| | |
|
| |
|
|
|
|
|
|
| |
to the first -I option.
Fortunately, with -I option, only one file can be found by occurrence
of the option, so on the contrary of -Q/-R options for v files, the
order is not file-system dependent.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
-I is (only) the ml one
-I -as is fixed
-Q is understood
-R is not a recursive ml include anymore
$COQENV, user_contrib, ... are not recursively included
coqlib/theories and coqlib/plugins are still recursively included (for now). (This
may deserves an option)
Closes Bug 2910: If there is a "Require a." in a b.v and a a.vo in path but no a.v,
coqdep does not complains about a missing a.v.
|
| |
|
|
|
|
| |
considered files.
Original patch by Guillaume Allais.
|
| | |
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16431 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
Sequel to commit 14476 : in fact, even with "tools" in .PHONY,
we still may have coqdep stuff being recompiled in a "make"
that follows a successful "make". This seems to related to
the hacks I've introduced to prevent ocamlopt from erasing
and recreating .cmi when there's no .mli around
(cf. comment around line 823 in Makefile.build).
Scenario:
- First we build coqdep_boot directly out of coqdep_lexer.ml and co.
When ocamlopt is around, this creates some .cmx and .cmi,
but no .cmo.
- Later we build coqdep, which need coqdep_lexer.cmx and co.
Now "make" checks whether these .cmx are up-to-date.
But our hacks made these .cmx depend on the corresponding .cmi.
Then "make" checks whether these .cmi are up-to-date.
But our hacks made these .cmi depend on the corresponding .cmo.
These .cmo doesn't exist yet, we run ocamlc, which recreates
the .cmi with same content but a different timestamp.
For some strange reason, even with refreshed .cmi, the .cmx
are not remade by this run, but will be on the next run.
Conclusion: what a mess. Implicit rules about .cmx / .cmo / .cmi
should be improved, but I see currently no simple solution.
In the meantime, an simple ad-hoc fix is to create these two .mli ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14479 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Emilio Jesus Gallego Arias
Théo Zimmermann
Pierre-Marie Pédrot
Pierre Letouzey
Hugo Herbelin
Maxime Dénès
Pierre Courtieu
Pierre Boutillier
letouzey
herbelin