| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Instead of browsing the term as many times as there are abstracted constants,
we replace the constants in one pass. We have to be a bit careful to replace
the right variables though, in case there are chained abstracts. This is much
faster.
This solves the second part of bug #5382: Huge case analysis fails in coq8.5.x.
|
|
Was introduced by 4f041384cb27f0d2. Unsoundness seems miraculously
avoided by a safeguard I put in nativecode.ml. But other kernel changes
in this commit should probably be reviewed carefully.
|
|
|
|
We don't need to look for the size of the whole list to find whether we can
extract a suffix from it, as we can do it in one go instead. This slowness
was observable in abstract-heavy code.
|
|
This turned out to be costly in proofs with many abstracted lemmas, as an
important part of the time was passed in the computation of the size of the
opaquetab.
|
|
In one case, the hashconsed type of a judgement was not used anywhere else.
In another case, the Opaqueproof module was rehashconsing terms that had
already gone through a hashconsing phase. Indeed, most OpaqueDef constructor
applications actually called it beforehand, so that the one performed in
Opaqueproof was most often useless. The only case where this was not true
was at section closing time, so that we tweak the Cooking.cook_constant to
perform hashconsing for us.
|
|
|
|
|
|
|
|
We were doing fishy things in the Term_typing file, where side-effects were
not considered in the right uniquization order because of the uniq_seff_rev
function. It probably did not matter after a9b76df because effects were
(mostly) uniquize upfront, but this is not clear because of the use of the
transparente API in the module.
Now everything has to go through the opaque API, so that a proper dependence
order is ensured.
|
|
We move it from Entries to Term_typing and export the few functions needed
to manipulate it in this module.
|
|
|
|
|
|
|
|
|
|
I believe an unwanted shadowing was introduced by a4043608f704f0.
|
|
|
|
(ProcThreeStInl.v, when the final "Defined" runs). I've verified that the
change here fixes the stack overflow there with Coq 8.5pl2.
In this version, all the recursive calls are in tail position. Instead of
taking a single list of instructions, `emit' here takes a curent list and a remaining
list of lists of instructions. That means the two calls elsewhere in the file now
add an empty list argument. The algorithm works on the current list until it's empty,
then works on the remaining lists. The most complex case is for Ksequence, where
one of the pieces becomes the new current list, and the other pieces are consed onto
the remaining sub-lists.
|
|
The `a.[i] <- x` notation is deprecated and we were getting a couple
of warnings.
|
|
We now build Coq with `-safe-string`, which enforces functional use
of the `string` datatype. Coq was pretty safe in these regard so only
a few tweaks were needed.
- coq_makefile: build plugins with -safe-string too.
- `names.ml`: we remove `String.copy` uses, as they are not needed.
|
|
We add a more convenient API to create identifiers from mutable
strings. We cannot solve the `String.copy` deprecation problem until
we enable `-safe-string`.
|
|
The `emitcodes` string type was used in both a functional and an
imperative way, so we have to handle it with care in order to preserve
the previous optimizations and semantics.
|
|
Maxime points out that -notop cannot be used as the kernel requires
all constants to belong into a module. Indeed:
```
$ rlwrap ./bin/coqtop -notop
Coq < Definition foo := True.
Toplevel input, characters 0-23:
> Definition foo := True.
> ^^^^^^^^^^^^^^^^^^^^^^^
Error: No session module started (use -top dir)
Coq < Module M. Definition foo := True. End M.
Module M is defined
Coq < Locate foo.
Constant If you see this, it's a bug.M.foo
(shorter name to refer to it in current context is M.foo)
```
My rationale for the removal is that this kind of incomplete features
are often confusing to newcomers ─ it has happened to me many times ─
as it can be seen for example in #397 .
|
|
No functional change.
|
|
No functional change, we create the new string beforehand and
`id_of_string` will become a noop with `-safe-string`.
|
|
It was always set to `greedy:true`.
|
|
This performance bug was introduced 9 years ago in a8b0345, where the
responsibility of normalizing the term went from ccnv to eqappr in Reduction.
As a result, all recursive calls to eqappr that were preemptively reducing the
term ended up calling whd_stack twice, once by themselves, and once in the
subsequent call to eqappr.
This caused an important slowdown for conversion-intensive proofs, as the
whd_stack calls CClosure.zip to perfom in-place term sharing, leading to
useless huge re-allocations and repetitive write barriers.
Now that eqappr always head-normalizes the term beforehand, we simply don't
call whd_stack anymore when jumping to eqappr.
|
|
|
|
We unroll the map operation by hand in two performance-critical cases so as
not to call the generic array allocation function in OCaml, and allocate
directly on the minor heap instead. The generic array function is slow because
it needs to discriminate between float and non-float arrays. The unrolling
replaces this by a simple increment to the minor heap pointer and moves from
the stack.
The quantity of unrolling was determined by experimental measures on various Coq
developments. It looks like most of the maps are for small arrays of size lesser
or equal to 4, so this is what is implemented here. We could probably extend it
to an even bigger number, but that would result in ugly code. From what I've seen,
virtually all maps are of size less than 16, so that we could probably be almost
optimal by going up to 16 unrollings, but the code tradeoffs are not obvious. Maybe
when we have PPX?
|
|
|
|
This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.
|
|
|
|
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
|
|
|
|
|
|
|
|
|
|
The native compiler doesn't support `Require` inside `Module` sections
in some cases, we improve the error message. See:
https://coq.inria.fr/bugs/show_bug.cgi?id=4335
This patch improves the error message and gives the user some
feedback.
|
|
This was observable in long proofs, because side effects kept being
duplicated, leading to an additional cost linear in the size of the proof.
This commit touches kernel files, but the corresponding API is only used
in tactic-facing code so that the side_effects type remains opaque. Thus
it does not affect the kernel safety.
|
|
|
|
This was deactivated by 27c9346 and made an optimization moot in eauto. This
optimization was physically checking for equality, but as lists where rebuilt
by the mapping, this was never true. Some contribs were thus quite slower,
including persistent-union-find which was twice slower.
This 2-line patch fixes it by trying to preserve sharing as much as possible.
Note that we should still do something about eauto, because it does redo
useless work a lot whenever the environment only changes a bit, while we could
cache this computation.
|
|
cofixpoint (bug #5286).
|
|
cofixpoint (bug #5286).
|
|
This also fixes decide equality, discriminate, ... (see e.g. #5279).
|
|
This is really [mv fast_typeops.ml{,i} typeops.ml{,i}] plus trivial
changes in the other files, the real changes are in the parent commit.
|
|
This brings the fix in cad44fc for #2996 to the copy of
Fast_typeops.check_hyps_inclusion.
Fast_typeops.constant_type checks the universe constraints instead of
outputting them. Since everyone who used Typeops.constant_type just
discarded the constraints they've been switched to constant_type_in
which should be the same in Fast_typeops and Typeops.
There are some small differences in the interfaces:
- Typeops.type_of_projection <->
Fast_typeops.type_of_projection_constant to avoid collision with the
internally used type_of_projection (which gives the type of [Proj(p,c)]).
- check_hyps_inclusion takes [('a -> constr)] and ['a] instead of
[constr] for reporting errors.
|
|
|
|
This was yet another bug in the VM long multiplication, that
I unfortunately introduced in ebc509ed2. It was impacting only 32-bit
architectures.
In the future, I'll try to make sure that
1) we provide unit tests for integer arithmetic (my int63 branch ships
with such tests)
2) our continuous testing infrastructure runs the test suite on a 32-bit
architecture. I tried to set up such an instance, but failed. Waiting
for support reply.
|
|
Was PR#366: Univs: fix bug 5208
|
