| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
|
| |
lambda is self-quoting, see elisp manual, section 12.7 Anonymous
Functions
|
| |
|
|
| |
The aux file for foo/bar.v is foo/.bar.aux, not .foo/bar.aux.
|
| | |
|
| |
|
|
| |
#3339).
|
| |
|
|
| |
This reverts commit 81c9fa0de99400b51c029cdbd1519b4f724e320a.
|
| | |
|
| |
|
|
|
|
| |
We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Moreover, this commit makes sure that an empty line after a list is always
translated into a break. ("StartLevel 1" was excluded, for some reason.)
It also avoids some code duplication. In particular, "stop_item ()" is
defined as "reach_item_level 0", so there is no reason to handle
"StartLevel 1" specially.
|
| | |
| |
| | |
This gives better behavior both when including the `coq_makefile` `Makefile` into other `Makefile`s and when setting `STDTIME` through an environment variable.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| | |
Coqc now expects physical names for input files, so fix coq_makefile
accordingly.
|
| |\ \
| | |
| | |
| | | |
Was PR#229: Bytecode compilation in a new 'make byte' rule apart from 'make world'
|
| | | |
| | |
| | |
| | |
| | |
| | | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
make install does not install these *.cm(o|a) files either.
You could always do manually :
- make bytefiles : to build the bytecode *.cm(o|a) files
- make install-byte : to install these files
- make byte : to compile the whole development with the bytecode version
of Coq (this builds the *.cm(o|a) files, but also the .vo via coqc -byte).
Technically, the behavior of make is controlled by the OPT variable,
which could be -byte or -opt. For instance, 'make byte' corresponds to a
'make OPT:=-byte'
Note that coqdep is used with the new option "-dyndep var" : when seeing
a Declare ML Module "foo", "coqdep -dyndep var" does not decide whether to
depend on foo.cma or foo.cmxs, but rather use some Makefile variables such
as foo$(DYNLIB), whose content is later set according to $(OPT)
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
The new warnings mechanism may which to forward a location to
IDEs. This also makes sense for other message types.
Next step is to remove redundant MsgError feedback type.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
Since we already have a rule %.cmxs:%.cmxa and the .cmxa depends
already on all the .cmx inside it, no need to state explicitely
that the .cmxs depends on these inner .cmx. Same thing concerning
.cmxs built out of a single .cmx.
|
| |\ \
| | |
| | |
| | | |
Add -o option to coqc
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| |\ \ \ \ \
| | |_|_|/
| |/| | | |
|
| | | | | | |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
For now, the pack name reuse the previous .cma name of the plugin,
(extraction_plugin, etc).
The earlier .mllib files in plugins are now named .mlpack.
They are also handled by bin/ocamllibdep, just as .mllib.
We've slightly modified ocamllibdep to help setting the -for-pack
options: in *.mlpack.d files, there are some extra variables such as
foo/bar_FORPACK := -for-pack Baz
when foo/bar.ml is mentioned in baz.mlpack.
When a plugin is calling a function from another plugin, the name
need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz).
Btw, we discard the generated files plugins/*/*_mod.ml, they are
obsolete now, replaced by DECLARE PLUGIN.
Nota: there's a potential problem in the micromega directory,
some .ml files are linked both in micromega_plugin and in csdpcert.
And we now compile these files with a -for-pack, even if they are
not packed in the case of csdpcert. In practice, csdpcert seems
to work well, but we should verify with OCaml experts.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The COQLIBS variable contains some -Q and -I options, which are not
supported by the checker. So this commit introduces a COQCHKLIBS variable
that contains the proper options for coqchk. For the sake of homogeneity,
the COQDOCLIBS variable is also preprocessed in the same way. This means
that both variables have the same value, but they are kept separate in
case the user would like to override one and not the other.
This commit also removes some deprecated options from "coqchk --help".
They are not removed from coqchk itself to preserve backward compatibility
in the branch.
An open question is whether coqchk should support dummy options such as -Q
(interpreted as -R) or -I (ignored).
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This purely cosmetic effect is obtained by the same variables
$(SHOW) and $(HIDE) as in the main Makefile of Coq.
If you prefer the earlier raw output : make VERBOSE=1
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Without this, dependencies upon a .ml4 (or a .mlpack) won't be handled
correctly.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
https://github.com/coq/coq/pull/150#issuecomment-219141596
```bash
git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i
```
|
| | |/ /
|/| |
| | |
| | |
| | |
| | | |
This add LtacProfiling. Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
#4770).
This also fixes comments not being properly skipped when looking for eol.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
As a side effect, there should be a small speedup when ignoring comments.
This commit also fixes two bugs related to handling "$$" and "#" in
comments.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This eases the task of replacing/improving the serializer, as well as
making it more resistant. See pitfalls below:
Main changes are:
- fold `message` type into `feedback` type
- make messages of type `Richpp.richpp` so we are explicit about the
content being a rich document.
- moved serialization functions for messages and stateid to `Xmlprotocol`
- improved a couple of internal API points (`is_message`).
Tested.
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We're back to a unique build phase (as before e372b72), but without
relying on the awkward include-deps-failed-lets-retry feature of make.
Since PMP has made grammar/ self-contained, we could now build
grammar.cma in a rather straightforward way, no need for
a specific sub-call to $(MAKE) for that. The dependencies between
files of grammar/ are stated explicitely, since .d files aren't
fully available initially.
Some Makefile simplifications, for instance remove the CAMLP4DEPS
shell horror. Instead, we generalize the use of two different
filename extensions :
- a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
- a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
except coqide_main.ml4 and its specific rule
Note that we do not generate .ml4.d anymore (thanks to the .mlp vs.
.ml4 dichotomy)
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Coqdep_boot has almost no dependencies, and hence can be compiled
very early during the build, without relying on .ml.d files.
Some code of system.ml is now in a separate file minisys.ml,
which is also included in system.ml for compatibility.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The -o option lets one put .vo or .vio files in a directory of choice,
i.e. decouple the location of the sources and the compiled files.
This ease the integration of Coq in already existing IDEs that handle
the build process automatically (eg Eclipse) and also enables one to
compile/run at the same time 2 versions of Coq on the same sources.
Example: b.v depending on a.v
coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo
coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo
coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo
coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
|
| | | |
|
Maxime Dénès
Vadim Zaliva
Hendrik Tews
Erik Martin-Dorel
Guillaume Melquiond
Enrico Tassi
Pierre-Marie Pédrot
Jason Gross
Pierre Letouzey
Matthieu Sozeau
Emilio Jesus Gallego Arias
Jason Gross