| Age | Commit message (Collapse) | Author |
|---|
|
This was virtually dead code. The only place really accessing this data was the
user pretty-printer, but actually the tables were not installed for vanilla vo
files.
In practice, that meant that the only case where an access to this table could
have been triggered would have been to print a term coming from a vio file,
or a vo file generated via vio2vo. In all other cases, the printer would not
have displayed the internal universes. While the latter might be considered
a bug, I am instead convinced that this notion of user-facing internal universes
needs to be handled by another mechanism, the current one making little sense.
The fact it was broken all along without anybody noticing proves my point.
|
|
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
|
|
Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.
This also enhances debug printing, as the latter is unable to properly
print futures.
|
|
on test-suite/arithmetic/mod: 2.6s to 0.45s
|
|
About 20% better perf on test-suite/arithmetic/mod (3.4s to 2.6s)
|
|
For instance this halves the time it takes to check
the test-suite/arithmetic/ files.
on mod: 7.5s to 3.4s
|
|
|
|
Now that we link lib we can do this.
|
|
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.
|
|
|
|
|
|
|
|
Before this patch, passing a mere identifier (without dots) to the checker
would make it consider it as implicitly referring to a relative name. For
instance, if passed "foo", it would have looked for "Bar.foo.vo" and
"Qux.foo.vo" if those files were in the loadpath.
This was quite ad-hoc. We remove this "feature" and require the user to
always give either a filename or a fully qualified logical name.
|
|
|
|
|
|
Instead of relying on the OCaml demarshaller, which is not resilient against
ill-formed data, we reuse the safe demarshaller from votour. This ensures that
garbage files do not trigger memory violations.
|
|
|
|
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
|
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|
|
|
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 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
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
|
|
Since d09def34, only the summary of libraries was included in the checksum, not
the actual content of the library. This quick fix performs the checking of the
checksum immediately, even if the loading is delayed.
|
|
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.
|
|
|
|
proofs.
|
|
There is no reason (any longer?) to create simultaneous closures for
interning and externing files. This patch makes the code more readable
by separating both functions and their signatures.
|
|
Marshalled libraries are only loaded when needed and dropped thereafter.
This might be costly for Require inside modules, but such a practice is
discouraged anyway.
|
|
The first part only contains the summary of the library, while the second
one contains the effective content of it.
|
|
|
|
|
|
|
|
|
|
Universes that are computed in the vi2vo step are not part of the
outermost module stocked in the vo file. They are part of the
Library.seg_univ segment and are hence added to the safe env when
the vo file is loaded.
The seg_univ has been augmented. It is now:
- an array of universe constraints, one for each constant whose opaque
body was computed in the vi2vo phase. This is useful only to print
the constants (and its associated constraints).
- a union of all the constraints that come from proofs generated in the
vi2vo phase. This is morally the missing bits in the toplevel module
body stocked in the vo file, and is there to ease the loading of
a .vo file (obtained from a .vi file).
- a boolean, false if the file is incomplete (.vi) and true if it is
complete (.vo obtained via vi2vo).
|
|
|
|
File format:
The .vo file format changed:
- after the magic number there are 3 segments. A segment is made of 3
components: bynary int, an ocaml value, a digest. The binary int
is the position of the digest, so that one can skip the value without
unmarshalling it
- the first segment is the library, as before
- the second segment is the STM task list
- the third segment is the opaque table, as before
A .vo file has a complete opaque table (all proof terms are there).
A .vi file follows the same format of a .vo file, but some entries
in the opaque table are missing. A proof task is stocked instead.
Utilities:
coqc: option -quick generates a .vi insted of a .vo
coq_makefile: target quick to generate all .vi
coqdep: generate deps for .vi files too
votour: can browse .vi files too, the first question is which segment
should be read
coqchk: rejects .vi files
|
|
To reduce the amount of syntactic noise, we now provide
a few inner modules Int.List, Id.List, String.List, Sorts.List
which contain some monomorphic (or semi-monomorphic) functions
such as mem, assoc, ...
NB: for Int.List.mem and co we reuse List.memq and so on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Since digests are strings (of size 16), we just dump them
now in vo files (cf. Digest.output) instead of using Marshal
on them : this is cleaner and saves a few bytes.
Increased VOMAGIC to clearly identify this change in the format.
Please rerun ./configure after this commit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
it into the standard logger instead.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16402 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16399 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Get rid of the LightenLibrary hack : no more last-minute
collect of opaque terms and Obj.magic tricks. Instead, we
make coqc accumulate the opaque terms as soon as constant_bodies
are created outside sections. In these cases, the opaque
terms are placed in a special table, and some (DirPath.t * int)
are used as indexes in constant_body. In an interactive session,
the local opaque terms stay directly stored in the constant_body.
The structure of .vo file stays similar : magic number, regular
library structure, digest of the first part, array of opaque terms.
In addition, we now have a final checksum for checking the
integrity of the whole .vo file. The other difference is that
lazy_constr aren't changed into int indexes in .vo files, but are
now coded as (substitution list * DirPath.t * int). In particular
this approach allows to refer to opaque terms from another
library. This (and accumulating substitutions in lazy_constr)
seems to greatly help decreasing the size of opaque tables :
-20% of vo size on the standard library :-). The compilation times
are slightly better, but that can be statistic noise.
The -force-load-proofs isn't active anymore : it behaves now
just like -lazy-load-proofs. The -dont-load-proofs mode has
slightly changed : opaque terms aren't seen as axioms anymore,
but accessing their bodies will raise an error.
Btw, API change : Declareops.body_of_constant now produces directly
a constr option instead of a constr_substituted option
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Very little space saved this way, but it would hurt either...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16375 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Why? : avoid catching (and probably ignoring) exceptions
such as Sys.Break, anomalies, assertions, leading to undetected
bugs and ignored Ctrl-C.
How? : when the precise exception(s) concerned by the try is
known, use them explicitely in the "with". Otherwise, let's use
the pattern "with e when Errors.noncritical e -> "
Particular case : when an exception is catched and reraised
immediately after some adjustments, we leave it untouched.
Simply, for easily identifying these situations later, the name
of the exception variable is changed to "reraise".
Please also adopt this coding style. Automatic checks based
on the "mascot" tool of X. Clerc will be runned regularly.
If you want to avoid to check a particular try...with, use
the variable name "any" after the "with".
All these changes have been tested using the standard library
and the test-suite, but unfortunately this is far from ensuring
that coqtop behaves as before. We'll see after the nightly bench...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16276 85f007b7-540e-0410-9357-904b9bb8a0f7
|
