| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This reverts commit 587e556a909fcd2e1507a9230d9cdaffa3f9394e from PR #1024.
This commit did not solve any issue at the time it was merged but made the
macOS package we produce compatible only with macOS 10.12 and later.
|
|
Specifically since e88dfedd99a84e9e375f3583be6fd1de3de36c72.
There seem to have been no actual errors due to this, only ocaml
complaining about missing .cmi files.
|
|
This overlay is now useless (change pushed upstream in bignums) and
moreover does not contain my commit making bignums resilient to PR#768.
|
|
|
|
We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.
For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.
Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.
|
|
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.
|
|
We remove `init_library_roots` as there is no point in resetting this
internal variable. Its only user is `init_load_path` and this function
is not meant (and is not) idempotent now.
|
|
|
|
Compute plugin
|
|
"_something")
|
|
inductive definition)
|
|
|
|
BZ#4852)
|
|
|
|
|
|
|
|
|
|
|
|
This allows the timing aggregation scripts to handle logs from Travis,
which, for some reason, seems to insert trailing spaces.
|
|
|
|
|
|
Also simplifies the way it is presented (no need to be overly precise).
|
|
|
|
The manual has long stated that these forms are deprecated. We add a
warning for them, as indeed `Add Morphism` is an "proof evil" [*]
command, and we may want to remove it in the future.
We've also fixed the stdlib not to emit the warning.
[*] https://ncatlab.org/nlab/show/principle+of+equivalence
|
|
When a context variable x is of the form "x := body : Z",
romega is now made aware of this body. Technically, we reify an equation
x = body, and push a corresponding (eq_refl x) as argument of the
final do_omega.
See also the previous commit adding this same feature to omega
(fixing bug 142).
|
|
148)
For compatibility, this extra feature of omega could be disabled via
Unset Omega UseLocalDefs.
Caveat : for now, real let-ins inside goals or hyps aren't handled, use
some "cbv zeta" reduction if you want to get rid of them. And context
definitions whose types aren't Z or nat are ignored, some manual "unfold"
are still mandatory if expanding these definitions will help omega.
|
|
|
|
|
|
|
|
to escape non-UTF-8 file names)
|
|
|
|
|
|
|
|
|
|
BZ#5757)
|
|
cleared context.
|
|
coq_makefile are in sync (supersed #1039)…
|
|
|
|
BZ#4852)
This code simplification isn't that important, but it can trigger further
simplifications elsewhere, see for instance BZ#4852.
NB: normally, the extraction favors eta-expanded forms, since that's the usual
way to avoid issues about '_a type variables that cannot be generalized. But
the atomic eta-reductions done here shouldn't be problematic (no applications
put outside of functions).
|
|
.dir-locals.el can be useful for users of the tarballs as well,
and TODO doesn't exist anymore.
|
|
The typical Coq `Pp.t` document contains a lot of "gluing" which
produces efficient structures but it is quite painful in
serialization.
We optimize a common document building case so we don't create as much
glue nodes as with the "naive" strategy, and without incurring in the
large performance cost full flattening would produce.
This is a temporal fixup, see #505 for more context on the discussion
and medium-term plans.
|
|
This is inconvenient because it can only be tested on tags
and it didn't work for V8.7+beta1.
|
|
|
|
This includes _ and insecable space which can be used in idents and
this allows more precise heuristics.
|
|
|
|
|
|
This allows e.g. the following to work:
Reserved Notation "* a" (at level 70).
Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m).
We seize this opportunity to make main calls to Metasyntax to depend
on an arbitrary env rather than on Global.env.
Incidentally, this fixes a little coqdoc bug in classifying the
inductive type referred to in the "where" clause.
|
|
|
|
|
