| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Removed documentation for broken -D -w (but the option are still there).
Fixed documentation of others.
|
|
|
|
|
|
Conflicts:
lib/cSig.mli
|
|
In OCaml 3.x, the toploop of OCaml was accessible from toplevellib.cma. In
OCaml 4.x, it was replaced by compiler-libs. However, linking with
compiler-libs produces a warning (fatal with OCaml 4.03) as soon as we have a
file named errors.ml or lexer.ml...
The only satisfactory solution seems to be to "pack" compiler libs. But it is
not done currently in the OCaml distribution, and implementing it in coqmktop
at this point would be too risky. So for now, I am disabling the warning until
we hear from the OCaml team. In principle, this clash of modules names can
break OCaml's type safety, so we are living dangerously.
|
|
|
|
|
|
|
|
|
|
- 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.
|
|
|
|
|
|
|
|
|
|
(thanks to coq-club, Sep 2015).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Useful e.g. with submakefiles.
|
|
|
|
Prior to commit 964d1b70, the dependency files .mllib.d and .mlpack.d
were generated by a call to coqdep using the argument -c (for ocaml
code). While doing some finetuning of the generation of implicit rules,
this commit removed (I think by mistake) this "-c". And without this
-c argument coqdep output nothing on mllib files leading to incorrect
linking of mllibs.
|
|
|
|
|
|
|
|
|
|
|
|
Characters do not need to be escaped in character ranges. It just had the
effect of matching backslashes four times.
|
|
|
|
"This function is deprecated: the runtime system is now able to print
uncaught exceptions as precisely as Printexc.catch does. Moreover, calling
Printexc.catch makes it harder to track the location of the exception
using the debugger or the stack backtrace facility. So, do not use
Printexc.catch in new code."
|
|
|
