| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
We now print the file responsible for the incompatibility in require error
messages.
|
| | |
| |
| |
| | |
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 some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
| |
|
|
|
|
| |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
| |\
| |
| |
| | |
Add -o option to coqc
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The -o option lets one put .vo or .vio files in a directory of choice,
i.e. decouple the location of the sources and the compiled files.
This ease the integration of Coq in already existing IDEs that handle
the build process automatically (eg Eclipse) and also enables one to
compile/run at the same time 2 versions of Coq on the same sources.
Example: b.v depending on a.v
coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo
coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo
coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo
coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
For instance, calling only Id.print is faster than calling both str and
Id.to_string, since the latter performs a copy. It also makes the code a
bit simpler to read.
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
| |
For a script that does just "Require Reals", this avoids 40k queries.
Note that this changes the signature of the FileDependency feedback.
Indeed, it no longer provides the physical path to the dependency but
only its logical path (since the physical path is no longer available).
The physical path could still have been recovered thanks to the
libraries_filename_table list. But due to the existence of the
overwrite_library_filenames function, its content cannot be trusted. So
anyone interested in the actual physical path should now also rely on the
FileLoaded feedback.
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
| |
in the loadpath.
This patch causes a bit of code duplication (because of the .coq suffix
added to state files) but it makes it clear which part of the code is
looking up files in the loadpath and for what purpose. Also it makes the
interface of System.extern_intern and System.raw_extern_intern much saner.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The single remaining use is in library/states.ml. This use should be
reviewed, as it is most certainly broken.
The other uses of Loadpath.get_paths did not disappear by miracle though.
They were replaced by a new function Loadpath.locate_file which factors
all the uses of the function. This function should not be used as it is as
broken as Loadpath.get_paths, by definition.
Vernac.load_vernac now takes a complete path rather than looking up for
the file. That is the way it was used most of the time, so the lookup was
unnecessary. For instance, Vernac.compile was calling Library.start_library
which already expected a complete path.
Another consequence is that System.find_file_in_path is almost no longer
used (except for Loadpath.locate_file, obviously). The two remaining uses
are System.intern_state (used by States.intern_state, cf above) and
Mltop.dir_ml_load for dynamically loading compiled .ml files.
|
| |
|
|
|
|
|
|
|
|
| |
This command-line option was behaving like the old -require, except that
it did not do Import. In other words, it was loading files without
respecting the loadpath. Now it behaves exactly like Require, while
-require now behaves like Require Import.
This patch also removes Library.require_library_from_file and all its
dependencies, since they are no longer used inside Coq.
|
| | |
|
| | |
|
| |
|
|
|
| |
I do not think that this information is worth displaying without
the verbose flag.
|
| |
|
|
|
|
|
|
|
|
| |
Since Guillaume's, launching coqtop without -native-compiler and call
native_compute would mean recompiling silently all dependencies, even if they
had been precompiled (e.g. the stdlib).
The new semantics is that -native-compiler disables separate compilation of the
current library, but still tries to load precompiled dependencies. If loading
fails when the flag is on, coqtop stays silent.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
libraries at once (see #4193).
|
| | |
|
| |
|
|
|
| |
Also removed the require function it was using, as it is absent from the
remaining of the code.
|
| | |
|
| |
|
|
| |
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
|
| |
|
|
| |
(thanks to Enrico for noticing a bug).
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
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
|
Pierre-Marie Pédrot
Maxime Dénès
Emilio Jesus Gallego Arias
Pierre Letouzey
Enrico Tassi
Guillaume Melquiond
mlasson
Hugo Herbelin