| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
So that a module can add his own and look at the traffic
|
|
composition operator.
Short story:
This pull-request:
(1) removes the definition of the "right-to-left" function composition operator
(2) adds the definition of the "left-to-right" function composition operator
(3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead.
Long story:
In mathematics, function composition is traditionally denoted with ∘ operator.
Ocaml standard library does not provide analogous operator under any name.
Batteries Included provides provides two alternatives:
_ % _
and
_ %> _
The first operator one corresponds to the classical ∘ operator routinely used in mathematics.
I.e.:
(f4 % f3 % f2 % f1) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x
We can call it "right-to-left" composition because:
- the function we write as first (f4) will be called as last
- and the function write as last (f1) will be called as first.
The meaning of the second operator is this:
(f1 %> f2 %> f3 %> f4) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x
We can call it "left-to-right" composition because:
- the function we write as first (f1) will be called first
- and the function we write as last (f4) will be called last
That is, the functions are written in the same order in which we write and read them.
I think that it makes sense to prefer the "left-to-right" variant because
it enables us to write functions in the same order in which they will be actually called
and it thus better fits our culture
(we read/write from left to right).
|
|
We consider an approximation of the size of sets before choosing the most
appropriate algorithm. This drastically affects some universe-polymorphic
code which was doing a lot of set operations on disimilar sizes.
|
|
Suggested by @ppedrot
|
|
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
|
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
|
While the performance gain should go unnoticed in most cases, in some
degenerate situations, e.g. the evar-stressing test-case of bug #4964,
this commit speeds up coq by 10% since most of the time is spent scanning
long lists with most of the elements filtered out.
Note that this commit also changes the scanning order to front-to-back,
which is a bit less surprising (though no code should ever depend on the
scanning order).
|
|
|
|
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
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
|
|
Was PR#223: Allow feedback messages to carry a location.
|
|
we already have
val remove_first : ('a -> bool) -> 'a list -> 'a list
(** Remove the first element satisfying a predicate, or raise [Not_found] *)
now we also have the more general
val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
(** Remove and return the first element satisfying a predicate,
or raise [Not_found] *)
The implementation is tail-recursive. The code I'm hoping to factorize
reimplements extract_first in a tail-recursive way, so it seemed good
to preserve this. On the other hand remove_first is not tail-recursive
itself, and that gives better constant factors in real-life
cases. It's unclear what is the best choice.
|
|
The ErrorMsg datatype was introduced to allow locations in messages,
however, it was redundant with error and used only in one place.
We remove it in favor of a more uniform treatment of messages with
location. This patch also removes the use of `Loc.ghost` in one place.
Lightly tested.
|
|
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.
|
|
This is a first step to relay location info in an uniform way, as needed
by warnings and other mechanisms.
The location info remains unused for now, but coqtop printing could take
advantage of it if so wished.
|
|
IMO level indicators are not the proper place to store this information.
|
|
Coq locations already had support for this, but were containing dummy
information. We now don't need anymore to reconstruct this information by
browsing the file when printing an error message or enriching exceptions on the
fly.
It also became easier to interface with Coq since locations emitted by the
lexer now always contain full information.
On the API side, Loc.represent disappeared and Loc.t is now exposed as record.
It is less error-prone than manipulating a tuple of 5 integers. Also,
Loc.create takes 5 arguments instead of 3 and a pair.
|
|
With par: the scenario is this one:
coqide --- master ---- proof worker 1 (has no par: steps)
---- proof worker 2 (has a par: step)
---- tac worker 2.1
---- tac worker 2.2
---- tac worker 2.3
Actor 2 installs a remote counter for universe levels, that are
requested to master. Multiple threads dealing with actors 2.x
may need to get values from that counter at the same time.
Long story short, in this complex scenario a mutex was missing
and the control threads for 2.x were accessing the counter (hence
reading/writing to the single socket connecting 2 with master at the
same time, "corrupting" the data flow).
A better solution would be to have a way to generate unique fresh universe
levels locally to a worker.
|
|
|
|
In pre 8.6, `Pp` provided its own reimplementation of
`Pervasives.flush_all`, with different semantics.
Unfortunately, with the removal of `Pp.flush_all` in #179, a couple of
points were silently switched to the `Pervasives` version, which may
lead to some subtle printing differences.
As a preventive measure, we restore the same semantics for these parts
of the codebase.
Note that we don't re-introduce Coq's `flush_all` for several reasons:
- Consumers of the logging API should not mess with flushing and
Formatters as this is backend dependent (i.e: when in IDEs).
Use of `Format` should be fully encapsulated if we want some hope of
IDEs taking full control.
- As used, the old semantics of `flush_all` were fragile.
|
|
Add -o option to coqc
|
|
Documentation also updated.
|
|
|
|
This is the "error resiliency" mode for STM
|
|
|
|
|
|
|
|
|
|
This reverts commit 45748e4efae8630cc13b0199dfcc9803341e8cd8.
|
|
|
|
|
|
By default we enable only {} and par: that are detectable in
a complete way.
|
|
|
|
Dag extended to support arbitrary clusters, renamed to Property.
Vcs generalized to not impose the data hold by a Property.
Stm(VCS) names a property "a box" and imposes a topological invariant (no
overlap). It defines 2 kind of boxes: ProofTasks (the old cluster
notion) and ErrorBound (meant to confine errors to sub-proofs).
In the meanwhile more equations added to Make(..) functors in order to
have just one Stateid.Set module around.
|
|
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.
|
|
|
|
|
|
This breaks compilation via ocamlbuild, and also leads to awkward
commands via make
|
|
Thanks to HH for pointing it out.
|
|
This makes the core free from particular protocol choices.
It should help with the ppx serialization project and shrinks clib.cma a
bit.
|
|
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.
|
|
|
|
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.
|
|
The command line option is named:
- async-proofs-delegation-threshold
Values are of type float, default 1.0 (seconds).
Proofs taking less that the threshold are not delegated to
a worker.
|
|
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.
|
|
A non-ASCII char is now converted to _UUxxxx_ with xxxx being its unicode index
in hexa. And any preexisting _UU substring in the ident is converted to _UUU.
The switch from __Uxxxx_ to _UUxxxx_ is cosmetic, it just helps the extraction
(less __ in names). But the other part of the patch (detection of preexisting
_UU substrings) is critical to make ascii_of_ident truly injective and avoid
the following kind of proof of False via native_compute :
Definition α := 1.
Definition __U03b1_ := 2.
Lemma oups : False.
Proof.
assert (α = __U03b1_). { native_compute. reflexivity. }
discriminate.
Qed.
|
