| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
| |
This one is a bit weird.
Unused since 4d95eb4e878f375a69f1b48d8833801bf555fdd0 (kept semantics,
the m is the same one outside and inside the call)
|
| |
|
|
|
|
|
|
| |
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The patch has three parts:
- Introduction of a configure flag `-bytecode-compiler (yes|no)`
(due to static initialization this is a configure-time option)
- Installing the hooks that register the VM with the pretyper and the
kernel conditionally on the flag.
- Replacing the normalization function in `Redexpr` by compute if the
VM is disabled.
We also rename `Coq_config.no_native_compiler` to `native_compiler`
and `Flags.native_compiler` to `output_native_objects` [see #4607].
|
| |
|
|
|
|
| |
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
|
| | |
|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.
Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.
In particular:
== Added flags ==
- `Safe_typing.allow_delayed_constants`
Allow delayed constants in the kernel.
- `Flags.record_aux_file`
Output `Proof using` information from the kernel.
- `System.trust_file_cache`
Assume that the file system won't change during our run.
== Deleted flags ==
- `Flags.compilation_mode`
- `Flags.batch_mode`
Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.
The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.
|
| |
|
|
|
|
| |
The fix is not anymore needed after Id.of_string was made strict
(5b218f87). This allows to support the whole official syntax of
identifiers and not just the alpha-numerical ones (without quote).
|
| |
|
|
|
|
|
|
| |
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
|
| | |
|
| |
|
|
|
|
| |
AFAICS this function predates modern state-handling; nowadays
summaries are stored by the STM and nobody were using this
information.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| |\ |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
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.
|
Gaëtan Gilbert
Maxime Dénès
Emilio Jesus Gallego Arias
Théo Zimmermann
Hugo Herbelin
Pierre-Marie Pédrot
Pierre Letouzey
Enrico Tassi
Guillaume Melquiond
mlasson