| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
| |
with Enrico.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
in 8.4 with the schemes of the subcomponent of an inductive added to
the environment or discharged as let-ins over the main scheme.
As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).
|
| |
|
|
|
|
| |
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
|
| |
|
|
|
| |
Substitution on bound modules was incorrectly extended without sequential
composition.
|
| |
|
|
|
| |
This was because the traversal algorithm used canonical names instead of user
names, confusing which term was defined and which term was an axiom.
|
| |
|
|
|
| |
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
| | |
|
| |
|
|
| |
This commit is chiefly about moving code around to ease readability.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
in 8.4 with the schemes of the subcomponent of an inductive added to
the environment or discharged as let-ins over the main scheme.
As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).
|
| |
|
|
|
|
| |
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
|
| |
|
|
|
| |
command line. Documenting only the former for simplicity and
uniformity with predating option -with-geoproof.
|
| |
|
|
|
|
|
|
| |
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 should actually probably be an anomaly, but I'm unsure the code
for decidability schemes is robust enough to dare it.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
decidability scheme).
Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:
Set Decidable Equality Schemes.
Inductive a := A with b := B.
which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
|
| |
|
|
|
|
|
|
|
|
| |
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
|
| |
|
|
| |
verbose flag.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
|
| | |
|
| |
|
|
| |
This allows fatal_error to be used for printing anomalies at loading time.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
| |
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
|
| |
|
|
|
| |
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
|
| | |
|
| |
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
| |
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)
|
| |
|
|
|
|
| |
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
| | |
|
| | |
|
| |
|
|
|
| |
This disables colors in emacs compilation buffer, which does not
support ansi colors by default.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
For now, warnings are still ignored by default, but this may change. This
commit at least allows to print them whenever desired. The -w syntax is
also opened to future additions to further control the display of
warnings.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
|
| | |
|
| |
|
|
|
|
|
| |
In compiler mode, only vernac.ml knows the current file name.
Stm.process_error_hook moved from Vernacentries to Vernac to
be bale to properly enrich the exception with the current file
name (if any).
|
| | |
|
| |
|
|
|
|
|
| |
The command [Redirect "filename" (...)] redirects all the output of
[(...)] to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
|
| | |
|
Hugo Herbelin
Maxime Dénès
Pierre-Marie Pédrot
Matthieu Sozeau
mlasson
Guillaume Melquiond
Enrico Tassi
Matthieu Sozeau
Lionel Rieg
Thomas Sibut-Pinote
Gabriel Scherer
Alec Faithfull
Clément Pit--Claudel
Pierre Courtieu