| Age | Commit message (Collapse) | Author |
|---|
|
When encountering
```Coq
Module M : T.
...
Lemma c :...
...
Qed.
...
End M.
```
every field `c` without body in `T` but with a body in `M` is
registered as opacified in a table along with all constants
`opacified(c)` without body in the environment at this point (i.e.,
all axioms potentially used by c).
Then, when printing axioms, if `c` appears in the final environment it
is replaced by `opacified(c)` in the resulting list of axioms.
|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
And enable related test.
|
|
Now all relevant typing_flags are taken in account by the checker.
The different forms of assumptions are now printed by the checker.
|
|
|
|
|
|
At the same time, we made the safe_env threading explicit.
|
|
For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.
With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.
We also rename some files from the checker so that they don't clash with
kernel files.
|
|
|
|
|
|
In 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct
access to the console, recommending instead to provide information to
the user by means of the `Feedback.msg_*` facilities.
However, we introduced a display bug in the checker printer as it is
special and doesn't use the Pp facilities (likely for trust reasons),
spotted by @herbelin
This patch fixes this bug and performs a couple more of fine tunings in
the input.
However, it could be desirable to port the `checker/printer.ml` to `Pp`
and use the feedback mechanism; this would allow IDEs to use the checker
in a more convenient way, at the cost of trusting `Pp` (which is already
a bit trusted currently)
A start of that idea can be found at:
https://github.com/ejgallego/coq/tree/fix_checker_printing
|
|
I had to remove code handling the -type-in-type option introduced by commit
9c732a5. We should fix it at some point, but I am not sure that using the
checker with a system known to be blatantly inconsistent makes much sense
anyway.
|
|
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.
|
|
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.
|
|
|
|
|
|
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The recent experiment with -dont-load-proofs in the stdlib showed that
this options isn't fully safe: some axioms were generated (Include ?
functor application ? This is still to be fully understood).
Instead, I've implemented an idea of Yann: only load opaque proofs when
we need them. This is almost as fast as -dont-load-proofs (on the stdlib,
we're now 15% faster than before instead of 20% faster with -dont-load-proofs),
but fully compatible with Coq standard behavior.
Technically, the const_body field of Declarations.constant_body now regroup
const_body + const_opaque + const_inline in a ternary type. It is now either:
- Undef : an axiom or parameter, with an inline info
- Def : a transparent definition, with a constr_substituted
- OpaqueDef : an opaque definition, with a lazy constr_substitued
Accessing the lazy constr of an OpaqueDef might trigger the read on disk of
the final section of a .vo, where opaque proofs are located.
Some functions (body_of_constant, is_opaque, constant_has_body) emulate
the behavior of the old fields. The rest of Coq (including the checker)
has been adapted accordingly, either via direct access to the new const_body
or via these new functions. Many places look nicer now (ok, subjective notion).
There are now three options: -lazy-load-proofs (default), -force-load-proofs
(earlier semantics), -dont-load-proofs. Note that -outputstate now implies
-force-load-proofs (otherwise the marshaling fails on some delayed lazy).
On the way, I fixed what looked like a bug : a module type
(T with Definition x := c) was accepted even when x in T was opaque.
I also tried to clarify Subtyping.check_constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
1- Management of the name-space in a modular development / sharing of non-logical objects.
2- Performance of atomic module operations (adding a module to the environment, subtyping ...).
1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P
Module M := P.
Module M.
Include P.
...
End M.
Declare Module K : S with Module M := P.
In this 3 cases we don't want to be bothered by the duplication of names.
Of course, M.foo delta reduce to P.foo but many non-logical features of coq
do not work modulo conversion (they use eq_constr or constr_pat object).
To engender a transparent name-space (ie using P.foo or M.foo is the same thing)
we quotient the name-space by the equivalence relation on names induced by the
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo).
So:
*************************************************************************************
* Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values *
*************************************************************************************
Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free
(also for a posteriori declaration of them, ex: a notation on M.foo will be
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.
2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate
several functors then we have bigger vo.
Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11954 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10826 85f007b7-540e-0410-9357-904b9bb8a0f7
|
