| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
One less global flag.
|
| |
|
|
|
| |
This brings us one step closer to actually moving all STM flags to
`stm`.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
On Win32, Sys.readdir translates the file names to the charset of the
local "code page", which may be not compatible with utf8.
Warnings referring to these names can be generated. These warnings may
be sent to CoqIDE. To ensure a utf8 compliant communication, we escape
non-utf8 file names under win32.
In the CoqIDE/Coq communication, Glib.IO.read_chars expects an
utf8-encoding and raises otherwise a Glib.Error "Invalid byte sequence in
conversion input".
This fixes bug #5715 (Hangul characters not recognized in file names)
but this does not solve the case of an operating system mounting a
file system with a different coding convention than the default one,
i.e. unicode using "Normalization Form Canonical Decomposition" in
UTF-8 for HFS+ on MacOS X, no encoding for ext3/ext4 on Linux,
(non-normalized?) UTF-16 for NTFS on Windows.
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
The same file name for .dot graphs could be used by concurrent processes.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).
|
| | |
| |
| |
| | |
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.
|
| |
|
|
|
|
| |
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
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
Coqdep_boot has almost no dependencies, and hence can be compiled
very early during the build, without relying on .ml.d files.
Some code of system.ml is now in a separate file minisys.ml,
which is also included in system.ml for compatibility.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
We protect Sys.readdir calls againts any nasty exception.
|
| |\| |
|
| | |
| |
| |
| | |
This fixes micromega in certain environments.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When coqtop is a long-lived process (e.g. coqide), the user might be
creating files on the fly. So we have to ask the operating system whether
a file exists beforehand, so that we know whether the content of the
directory cache is outdated.
In batch mode, we can assume that the cache is always up-to-date, so we
don't need to query the operating system before trusting the content of
the cache.
On a script doing "Require Import Reals", this brings down the number of
stat syscalls from 42k to 2k. The number of syscalls could be further
halved if all_subdirs was filling the directory cache.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
"open Unix" from lib/system.ml.
|
| | | |
|
| | |
| |
| |
| | |
This makes the function sightly more portable.
|
| |\| |
|
| | |
| |
| |
| |
| | |
second chance to dynamically regenerate the file system cache when a
file is not found (suggested by Guillaume M.).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
correct case on MacOS X whose file system is case-insensitive but
case-preserving (HFS+ configured in case-insensitive mode).
Generalized it to any case-preserving case-insensitive file system,
which makes it applicable to Windows with NTFS used in
case-insensitive mode but also to Linux when mounting a
case-insensitive file system.
Removed the blow-up of the patch, improved the core of the patch by
checking whether the case is correct only for the suffix part of the
file to be found (not for the part which corresponds to the path in
which where to look), and finally used a cache so that the effect of
the patch is not observable.
Note that the cache is implemented in a way not synchronous with
backtracking what implies e.g. that a file compiled in the middle of
an interactive session would not be found until Coq is restarted, even
by backtracking before the corresponding Require.
For history see commits
b712864e9cf499f1298c1aca1ad8a8b17e145079,
4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606
69941d4e195650bf59285b897c14d6287defea0f
e7043eec55085f4101bfb126d8829de6f6086c5a.
as well as
https://coq.inria.fr/bugs/show_bug.cgi?id=2554
discussion on coq-club "8.5 and MathClasses" (May 2015)
discussion on coqdev "Coq awfully slow on MacOS X" (Sep 2015)
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files"
and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X."
This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606
and 69941d4e195650bf59285b897c14d6287defea0f
and e7043eec55085f4101bfb126d8829de6f6086c5a.
Trying to emulate a case sensitive file system on top of a case aware one is
too costly: 3x slowdown when compiling the stdlib or CompCert.
|
| |\| |
|
| | |
| |
| |
| | |
Thanks to Vadim Zaliva for testing.
|
| | |
| |
| |
| |
| | |
found in the file system have the expected lowercase/uppercase
spelling)
|
| | |
| |
| |
| |
| | |
expected lowercase/uppercase spelling (based on a patch by Pierre B.).
This should fix #2554 (and see also discussion on coq-club, May 2015).
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error),
- uniformly expecting paths in Unix format and warning otherwise.
|
| | |
| |
| |
| |
| |
| | |
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
|
| |/
|
|
|
|
|
| |
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error).
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
Emilio Jesus Gallego Arias
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Pierre Letouzey
Tej Chajed
Guillaume Melquiond
Enrico Tassi