| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
|
|
|
|
|
|
|
|
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
|
|
|
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
|
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
|
|
|
|
|
|
|
|
|
|
I used a low-level function, now changed to `msg_notice`.
|
|
|
|
Hence we reuse the ones in master.
|
|
|
|
|
|
This makes the treatment of universe constraints/normalization more
understandable in the Sync/Async case:
- if one has to keep the constraints of the body and the type of
a lemma separate, then equations coming from the body are kept
(see: 866c41 )
- if they can be merge then the equations (substituted on both the
body and type) can be removed (one of the sides occurs nowhere)
The result is that, semantically, the constraints of a lemma do not
depend on weather it was produced asynchronously (v->vio->vo, or in
a CoqIDE session) or synchronously (v->vo).
Still the internal representation of the constraints changes to
accommodate an optimization (to reduce the size of the constraint set):
- in the synchronous case (some) equations are substituted (in both the
type and body), hence they can be completely dropped from the constraint
set
- in the asynchronous case (some) equations are substituted in the body
only (the type is fixed once and for all before the equations are
discovered/generated), hence these equations are necessary to relate
the type and the (optimized) body and are hence kept in the constraint
set
|
|
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
|
Pretype_errors.PretypeError.
Instad of trying to print the exception, we raise it in the tactic monad.
|
|
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
|
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
|
|
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
|
|
allow reusability of the implementation throughout the Coq codebase.
We effectively feature a generalized version of the logical monad where the
input state, the output state and the inner exception can be arbitrarily chosen.
This will allow for more efficient implementations of close variants of the
monad.
|
|
|
|
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
|
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
|
We just inline the state in the iolist: less closures makes the GC happier.
|
|
|
|
|
|
|
|
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
|
|
|
|
together with the tactic monad.
The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.
|
|
progress.
Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far.
Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it).
Fixes bugs (one reported directly on coqdev, and #3412).
|
|
|
|
|
|
|
|
Ultimately setoid rewrite should be written in the monad to fix it properly.
|
|
actually calling the VM at Qed time.
|
|
|
|
|
|
Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
|
|
Updated doc, but not tests-suite yet.
|
|
After commit b46944e the system got way slower, hence the optimization
is relevant also for non polymorphic constants. Putting it back now,
but we shall find something in between: an optimization that does
not clash with async proofs but that gives some performance improvement
over no optimization at all.
|
|
As discussed on coqdev, clear is not perfect, Hints for trivial
using cleared section vars are still used.
But it is better than nothing I guess.
|
|
|
|
Given that the proof state contains a callback (a terminator)
that is not sent (dropped by the ephemeron mechanism at marshall
time) de-referencing the ephemeron during this function makes it
impossible to call it in a worker. Now the worker can call the
function and replace the terminator with a good one.
|
|
When one generates a .vi file only the type is stocked.
When one completes a .vi the proof term is stocked but the
corresponding type is not changed:
- if one minimizes the constraints of the body, the minimization
could find that 2 univs are equal and substitute one for the
other in the body, but it should also apply the subst to the type
orelse coqchk could fail
- also, a "retroactive" change of a type (making it stricter)
invalidates what was type checked afterwards, so this operation
clashes with the vi2vo compilation chain
Hence we enable this optimization only for universe polymorphic
constants that:
- are the ones that truly requires such optimization
- are never processed asynchronously, so the scenario above does
not apply
|
