| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| |
|
|
| |
This allows fatal_error to be used for printing anomalies at loading time.
|
| |
|
|
| |
May still be wrong on Windows, though.
|
| | |
|
| |
|
|
|
| |
We lambda-lift by hand the graph traversal functions in Univ to allocate
less closures.
|
| |
|
|
|
| |
Fixes bug 3936
This closes #73
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This interface is promoted by the operf-macro tool
https://github.com/OCamlPro/operf-macro
which allows to run benchmarks of time and memory usage
of various OCaml programs.
Coq already has two ways to get Gc infos:
- the -m|--memory command-line flag prints the total heap words allocated
- the "Print Debug Gc" command prints much more information,
but in a Coq-implementation-defined format that is not suitable
for across-programs comparison
(also an environment variable allows to profile Coq runs on any .v,
in an non-intrusive way)
Note to the Github Robot:
This closes #75
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
| |
A worker should never have to access the still-to-be-proved
obligations. If that happens, raise an informative anomaly.
|
| |
|
|
|
| |
This type contains a few unmarshallable fields, which can cause STM
workers to break in unpleasant ways when running queries
|
| |
|
|
|
|
|
|
|
|
|
| |
maybe ca71714).
Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.
was working in 8.4 but was failing in 8.5beta2.
Note: Changes in tacintern.ml are otherwise purely cosmetic.
|
| | |
|
| |
|
|
|
| |
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
|
| |
|
|
| |
I used a low-level function, now changed to `msg_notice`.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Message to the github robot:
This closes #63
|
| | |
|
| |
|
|
|
|
|
| |
Fix for [Anomaly: Uncaught exception Failure("hd")] after running [Show
Intros] at the end of a proof:
Goal True. trivial. Show Intros.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This mirrors the existing extraction libraries for OCaml.
One wart: the extraction for [string] requires that the Haskell code
imports Data.Bits and Data.Char. Coq has no way to add extra import
statements to the extracted code. So we have to rely on the user to
somehow import these libraries (e.g., using the -pgmF ghc option).
See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189
Message to github robot: this commit closes #65
|
| | |
|
| |
|
|
|
| |
Ideally, the code should be shared between the various toplevels, but this
is a lot more work than just fixing a few strings.
|
| | |
|
| | |
|
| |
|
|
| |
"Conjecture" (see #4252).
|
| |
|
|
|
| |
Was making the study of bugs like #4139 painful.
Now printing a better error message when a compiled file is missing.
|
| | |
|
| | |
|
| |
|
|
| |
Wrong handling of algebraic universes that have upper bounds.
|
| |
|
|
| |
Hence we reuse the ones in master.
|
| | |
|
| | |
|
| |
|
|
| |
with other reduction machines.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Patch provided by Çagdas Bozman.
|
| | |
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Trying to untangle the flags:
coqc -verbose coqtop -compile-verbose are used just to print the commands run;
-quiet, -silent, Set Silent, Unset Silent control Flags.verbose flag.
Flags.verbose controls many prints that are expected to be made in
interactive mode. E.g. "Proof" or "tac" prints goals if such flag is
true. To flip it, one can "Set/Unset Silent" in both coqtop and coqc
mode.
It is still messy, but the confusion between -verbose and Flags.verbose
has gone (I must have identified the two things with my initial STM
patch)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This makes the treatment of universe constraints/normalization more
understandable in the Sync/Async case:
- if one has to keep the constraints of the body and the type of
a lemma separate, then equations coming from the body are kept
(see: 866c41 )
- if they can be merge then the equations (substituted on both the
body and type) can be removed (one of the sides occurs nowhere)
The result is that, semantically, the constraints of a lemma do not
depend on weather it was produced asynchronously (v->vio->vo, or in
a CoqIDE session) or synchronously (v->vo).
Still the internal representation of the constraints changes to
accommodate an optimization (to reduce the size of the constraint set):
- in the synchronous case (some) equations are substituted (in both the
type and body), hence they can be completely dropped from the constraint
set
- in the asynchronous case (some) equations are substituted in the body
only (the type is fixed once and for all before the equations are
discovered/generated), hence these equations are necessary to relate
the type and the (optimized) body and are hence kept in the constraint
set
|
| | |
|
| | |
|
Thomas Sibut-Pinote
Maxime Dénès
Pierre-Marie Pédrot
Gregory Malecha
Gabriel Scherer
Enrico Tassi
Alec Faithfull
Hugo Herbelin
Arnaud Spiwack
Theo Zimmermann
Clément Pit--Claudel
Nickolai Zeldovich
Guillaume Melquiond
Cyprien Mangin
Matthieu Sozeau