| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
coq-makefile's tests do depend on this
|
|
On NixOS in particular, /usr/bin/time doesn't exist.
|
|
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
|
|
|
|
|
|
It is empty and not used anymore.
|
|
|
|
|
|
|
|
This commit adds timing scripts from
https://github.com/JasonGross/coq-scripts/tree/master/timing into the
tools folder, and integrates them into coq_makefile and Coq's makefile.
The main added makefile targets are:
- the `TIMING` variable - when non-empty, this creates for each built
`.v` file a `.v.timing` variable (or `.v.before-timing` or
`.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively)
- `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of
sorted timings at the end, saving it to `time-of-build-pretty.log`
- `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after
TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file
`time-of-build-before.log` or `time-of-build-after.log`, respectively
- `print-pretty-timed-diff` - prints a table with the difference between
the logs recorded by `make-pretty-timed-before` and
`make-pretty-timed-after`, saving the table to
`time-of-build-both.log`
- `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a
table with the differences between two `.v.timing` files, and saves
the output to `time-of-build-pretty.log`
- `*.v.timing.diff` - this saves the result of
`print-pretty-single-time-diff` for each target to the
`.v.timing.diff` file
- `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's
own Makefile) - makes all `*.v.timing.diff` targets
N.B. We need to make `make pretty-timed` fail if `make` fails. To do
this, we need to get around the fact that pipes swallow exit codes.
There are a few solutions in
https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make;
we choose the temporary file rather than requiring the shell of the
makefile to be bash.
|
|
This closes [bug #5596](https://coq.inria.fr/bugs/show_bug.cgi?id=5596).
|
|
This should help preventing weird compilation failures due to leftover
object files after deleting or moving some source files
By the way:
- use plain $(filter-out ...) instead of a 'diff' macro (thanks Jason
for the suggestion)
- rename FIND_VCS_CLAUSE into FIND_SKIP_DIRS since it contains more
than version control stuff nowadays
|
|
This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619)
|
|
Due to the recent conversion of many .mli-only files into .ml files
(hugely debatable impact of the API introduction), parallel make may
fail badly again (always the same race between ocamlc and ocamlopt for .cmi).
Still working on a proper fix, but meanwhile let's reintroduce the
old hacks against these corruptions.
|
|
of this file
There is now a warning if the content of micromega.ml isn't what MExtraction.v would
produce.
|
|
|
|
|
|
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
|
|
generate them later.
|
|
|
|
|
|
"plugins/micromega/MExtraction.v"
|
|
|
|
|
|
"plugins/micromega/MExtraction.v"
|
|
|
|
This allows to grant a wish by Hugo: to build coqtop.byte and prelude
with it, you could do:
make -j BEST=byte states
|
|
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
|
|
The .mli only acknowledges the current API. I'm not guilty your honor!
|
|
This removes some remaining support for camlp4 in the infrastructure
and documents the change.
|
|
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
|
|
By default, we serialize messages to the "rich printing
representation" as it was done in 8.6, this ways clients don't have to
adapt unless they specifically request the new format using option
`--xml_format=Ppcmds`
|
|
|
|
Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.
This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.
Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.
However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.
The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.
We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.
`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.
Thus, the new panorama is:
- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
to coqtop.
_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.
_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.
A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.
The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.
|
|
For some reason "grammar/grammar.cma" was declares only an "order-only" dependency for "*.ml" files generated from "*.ml4".
I this that this is a problem because when we change "grammar/*.mlp" files, even tough "grammar/grammar.cma" is regenerated,
the actual "*.ml" files (defined by "*.ml4" as well as "grammar/grammar.cma") are not regenerated.
|
|
This file was only used during ocamldebug sessions (in the dev/db
script). It was containing a large subset of the core cma files,
up to the printing functions. There were a few notable exceptions,
for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
But printers.cma was troublesome to maintain : almost each time an ML file
was added/removed/renamed in the core of Coq, dev/printers.mllib
had to be edited, in addition to the directory-specific .mllib
(kernel/kernel.mllib and co). So I propose here to kill this file,
and put instead in dev/db several "load_printer" of the core cma files.
For that to work, we need to compile kernel/kernel.cma with the right
-dllib and -dllpath options, but that shouldn't hurt (on the contrary).
We also source now the camlpX cma in dev/db, via a new generated file
dev/camlp4.dbg containing a load_printer of either gramlib.cma or
camp4lib.cma.
If one doesn't want to perform the whole "source db" at the start
of an ocamldebug session, then the former "load_printer printers.cma"
could be replaced by:
source core.dbg
load_printer top_printers.cmo
See for instance the minimal dev/base_db.
|
|
|
|
- With the ?= construction, we avoid warnings about undefined variables,
while tolerating both 'make VERBOSE=1' and 'VERBOSE=1 make'
- Some extra documentation and cleanup
|
|
|
|
|
|
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.
|
|
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
|
|
This allows to grant a wish by Hugo: to build coqtop.byte and prelude
with it, you could do:
make -j BEST=byte states
|
|
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
|
|
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
|
|
|
|
