| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
|
| |
The first part only contains the summary of the library, while the second
one contains the effective content of it.
|
| |
|
|
| |
Wrong handling of algebraic universes that have upper bounds.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
| |
libraries at once (see #4193).
|
| |
|
|
| |
has a strict upper bound.
|
| |
|
|
|
| |
Without this commit, passing "-R theories Coq" to "coqtop -nois" has no
effect since "-Q theories Coq" has already been done implicitly.
|
| | |
|
| |
|
|
|
| |
Also removed the require function it was using, as it is absent from the
remaining of the code.
|
| | |
|
| |
|
|
|
|
|
|
| |
The new behaviour is simple: either a path is in the loadpaths or it is not.
No more wild expansions of paths!
This should not affect -R and -Q, but it does change the semantics of -I -as.
Still, there are no more users of it and it only does so in a subtle way.
|
| | |
|
| | |
|
| |
|
|
| |
It is still present in the libstack, though.
|
| |
|
|
|
| |
We explicit the fact that we only need the name of the library in most of the
summaries.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
| |
|
|
|
| |
Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.
|
| |
|
|
| |
[compare_head_gen] defined in terms of [compare_head_gen_leq]. Remove an unused argument from [compare_head_gen_leq].
|
| | |
|
| |
|
|
| |
(thanks to Enrico for noticing a bug).
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
Instead of registering all the transitive dependencies of a term in one go,
we rather recursively build the graph of direct dependencies of this term.
This is finer-grained and offers a better API.
The traversal now uses the standard term fold operation, and also registers
inductives and constructors encountered in the traversal.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Of course such proofs cannot be processed asynchronously
|
| | |
|
| |
|
|
|
|
|
|
| |
This is done by adding a fourth type of loadpath, the ones that are
neither implicit nor root, for the subdirectories of a -Q root.
Note: this means that scanning for available directories is no longer done
on the fly for -Q, but once and for all, as with -R.
|
| |
|
|
|
|
| |
optimized. Now "Import Arith ZArith" imports only once the libraries
reexported by both Arith and ZArith. (No side effect can be inserted
here, so that this looks compatible).
|
| | |
|
| |
|
|
| |
Follow-up on Matthieu's d030ce0721.
|
| |
|
|
| |
printing functions touched in the kernel).
|
| |
|
|
|
|
|
|
| |
This reverts commit 6d5b56d971506dfadcfc824bfbb09dc21718e42b but does not put
back in place the Requires inside modules that were found in the std lib.
Conflicts:
kernel/safe_typing.ml
|
| | |
|
| |
|
|
| |
This is a follow-up on Pierre's 5d80a385.
|
| |
|
|
|
|
| |
into monomorphic constants, which was still using the de Bruijn encoding
Bug revealed by discharging of hidden internal monomorphic definition in
otherwise polymorphic developments. Makes coqchk work on Hurkens again.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After this commit, module_type_body is a particular case of module_type.
For a [module_type_body], the implementation field [mod_expr] is
supposed to be always [Abstract]. This is verified by coqchk, even
if this isn't so crucial, since [mod_expr] is never read in the case
of a module type.
Concretely, this amounts to the following rewrite on field names
for module_type_body:
- typ_expr --> mod_type
- typ_expr_alg --> mod_type_alg
- typ_* --> mod_*
and adding two new fields to mtb:
- mod_expr (always containing Abstract)
- mod_retroknowledge (always containing [])
This refactoring should be completely transparent for the user.
Pros: code sharing, for instance subst_modtype = subst_module.
Cons: a runtime invariant (mod_expr = Abstract) which isn't
enforced by typing. I tried a polymorphic typing of mod_expr,
to share field names while not having mtb = mb, but the OCaml
typechecker isn't clever enough with polymorphic mutual fixpoints,
and reject code sharing (e.g. between subst_modtype and subst_module).
In the future (with ocaml>=4), some GADT could maybe help here,
but for now the current solution seems good enough.
|
| |
|
|
|
|
| |
Removing unused argument and fixing bug #3899, now warning when a record
cannot be made primitive in Set Primitive Projections mode because it
has no projection or at least one undefinable projection.
|
| |
|
|
|
|
|
| |
Fixes #3379 and part of #3363. Also avoids fragile code propagating required
libraries when closing an interactive module.
Had to fix a few occurrences in std lib.
|
| |
|
|
|
| |
API to let one forge a frozen state out of another frozen state
plus some frozen bits
|
| |
|
|
|
|
| |
In this way one can make surgery on the system states, like
checking if two frozen states have the same environment (i.e.
no running "abstract" in between)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
| |
|
|
|
| |
Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra
care with cmd.exe vs sh is no longer required.
|
| | |
|
Pierre-Marie Pédrot
Matthieu Sozeau
Guillaume Melquiond
Arnaud Spiwack
Hugo Herbelin
Matthieu Sozeau
Enrico Tassi
Maxime Dénès
Pierre Letouzey