| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
With par: the scenario is this one:
coqide --- master ---- proof worker 1 (has no par: steps)
---- proof worker 2 (has a par: step)
---- tac worker 2.1
---- tac worker 2.2
---- tac worker 2.3
Actor 2 installs a remote counter for universe levels, that are
requested to master. Multiple threads dealing with actors 2.x
may need to get values from that counter at the same time.
Long story short, in this complex scenario a mutex was missing
and the control threads for 2.x were accessing the counter (hence
reading/writing to the single socket connecting 2 with master at the
same time, "corrupting" the data flow).
A better solution would be to have a way to generate unique fresh universe
levels locally to a worker.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A non-ASCII char is now converted to _UUxxxx_ with xxxx being its unicode index
in hexa. And any preexisting _UU substring in the ident is converted to _UUU.
The switch from __Uxxxx_ to _UUxxxx_ is cosmetic, it just helps the extraction
(less __ in names). But the other part of the patch (detection of preexisting
_UU substrings) is critical to make ascii_of_ident truly injective and avoid
the following kind of proof of False via native_compute :
Definition α := 1.
Definition __U03b1_ := 2.
Lemma oups : False.
Proof.
assert (α = __U03b1_). { native_compute. reflexivity. }
discriminate.
Qed.
Conflicts:
lib/unicode.mli
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
hash-consing, so as to avoid having too many kinds of equalities with
same name.
|
| |
|
|
| |
We protect Sys.readdir calls againts any nasty exception.
|
| |
|
|
| |
This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b
|
| |
|
|
| |
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
| |
|
|
|
|
|
| |
Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying
improperly. We now check that all strings outputed by Coq are proper UTF-8.
This is not perfect, as CoqIDE will sometimes truncate strings which contains
the null character, but at least it should not crash.
|
| |
|
|
| |
This fixes micromega in certain environments.
|
| |
|
|
|
|
|
| |
(e.g. with deprecated options such as -byte, etc.) since I guess this
is what we expect.
Was probably lost in 81eb133d64ac81cb.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
The Map interface of upcoming OCaml 4.03 includes a new union operator. In
order to make our homemade implementation of Maps compatible with OCaml
versions from 3.12 to 4.03, we define our own signatures for Maps.
|
| |
|
|
|
|
|
|
| |
CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
|
| |
|
|
|
|
|
|
| |
In the original version, ocamldoc markup wasn't used properly thus
ocamldoc output did not in all places make sense.
This commit makes sure that the documentation of the Predicate module
is as clear as the documentation of the Set module (in the standard library).
|
| |
|
|
|
|
|
|
|
|
| |
This patch also causes the code to finish a bit faster in the NoGlob case
by not preparing a string for dump_string. It also optimizes
Dumpglob.is_ghost by only checking whether the end position is zero.
Note that no ghost locations were part of the glob files of the standard
library before the patch. Note also that the html documentation of the
standard library is bitwise identical before and after the patch.
|
| |
|
|
|
|
| |
The interesting manifestation of the bug was Unix.select
returning no error but the empty list of descriptors, as if
a timeout did happen.
|
| |
|
|
| |
"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)
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
According to http://caml.inria.fr/mantis/view.php?id=5325
you can't use the same socket for both writing and reading.
The result is lockups (may be fixed in 4.03).
|
| | |
|
| |
|
|
| |
So that they display in response buffer.
|
| |
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
| |
Correcting the code w.r.t. to the API was not the right solution. Instead,
the API comment had to be corrected.
|
| |
|
|
|
|
| |
We ensure statically by typing that the tags used by the rich printer
are integers. Furthermore, we also expose through typing that tags are
irrelevants in the returned XML.
|
| | |
|
| | |
|
| |
|
|
|
| |
Contrarily to what was described in the API, nodes without annotations
were not ignored by the printer but left there instead.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| |
|
|
|
| |
hash-consing, so as to avoid having too many kinds of equalities with
same name.
|
| | |
|
| |
|
|
|
|
|
|
| |
File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.
There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
|
| |
|
|
| |
This allows fatal_error to be used for printing anomalies at loading time.
|
| |
|
|
|
| |
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
|
| |
|
|
|
|
|
| |
Of course there is an exception to the previous commit.
Fail used to print even if silenced but loading a vernac file.
This behavior is useful only in tests, hence this flag.
|
Enrico Tassi
Pierre Letouzey
Pierre-Marie Pédrot
Tej Chajed
Hugo Herbelin
Maxime Dénès
Emilio Jesus Gallego Arias
Matej Kosik
Guillaume Melquiond
Pierre Courtieu
Thomas Sibut-Pinote