| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
The old code was generating different patterns, depending on whether
a projection with parameters was expanded or not. In the first case,
parameters were present, whereas in the latter they were not.
We fix this by adding dummy parameter arguments on sight.
Fixes #14009: TC search failure with primitive projections.
|
|
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
|
|
Previously, `Array.init` was computing the first element of the array
twice, resulting in exponential overhead in the number of recursive
nestings of `Array.init`. Notably, since `Array.map` is implemented in
terms of `Array.init`, this exponential blowup shows up in any term
traversal based on `Array.map` over the arguments of application nodes.
Fixes #14011
|
|
Bytecode execution of persistent arrays can modify structured values meant
to be marshalled in vo files. Some VM values are not marshallable, leading
to this anomaly.
There are further issues with the use of a hash table to store structured
values, since they rely on structural equality and hashing functions.
Persistent arrays are not safe in this context.
Fixes #14006: Coqc cannot save .vo files containing primitive arrays.
|
|
Reviewed-by: gares
|
|
to check for conversion
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Fixes #14003: Ltac2 redefinition check is broken.
|
|
Reviewed-by: ppedrot
|
|
notation declarations
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
Reviewed-by: MSoegtropIMC
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
Fixes #13963
|
|
transitively closed
Reviewed-by: ppedrot
|
|
Fixes #13960: Ltac2 Eval does not work with Set Default Goal Selector "!".
|
|
|
|
|
|
The table of coercion classes (`class_tab`) has been extended with information
about reachability. The conversion checking of a pair of multiple inheritance
paths (of coercions) will be skipped if these paths can be reduced to smaller
adjoining pairs of multiple inheritance paths, and this reduction will be
determined based on that reachability information.
|
|
Instead of recomputing the n-th lifts of terms for every subterm under a context,
we introduce a table storing the value of this lift across contexts. While not
the most efficient algorithmically, it is still much more efficient in practice and
does not exhibit the exponential behaviour of replacing under different subcontexts.
In an ideal world we would have an equality function on terms that allows to compute
equality up to lifts, which would prevent having to even compute the lift at all, but
the current fix has the advantage to be self-contained and not require dangerous
tweaking of an equality function which is already complex enough as it is.
Fixes #13896: cbn very slow.
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Ack-by: ejgallego
|
|
Fix #13903
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
|
|
|
|
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: JasonGross
Reviewed-by: MSoegtropIMC
|
|
|
|
|
|
|
|
ssreflect asks setoid rewrite to rewrite in goal
"forall_special_name_ : T, _other_name_"
Since this is a non dependent product, setoid rewrite converts that to
"impl T _other_name_" and must be taught to restore the special name
when unfolding impl.
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
Reviewed-by: silene
Reviewed-by: gares
|
|
This has been in the TODO queue for a long time, and indeed
I have recently seen some trouble with users passing two .v files to
Coq, which it isn't a) tested, b) supported.
Moreover, it doesn't even work correctly in 8.13 due to some other
changes in the toplevel related to auxiliary files.
(*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
|
|
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
|
|
|
|
|
|
Otherwise, the interpreter sees already unified evars as accumulators
rather than actual constants, thus preventing the computations from
progressing.
This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed
evar normalization. The effect went unnoticed because the computed term is
still convertible to the reduced term, except that it is the lazy
machinery that ends up reducing it, rather than the bytecode one.
So, performances became abysmal, seemingly at random.
|
|
Reviewed-by: silene
Ack-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: vbgl
|
|
Closes #13794
|
|
Warnings are handled as injection commands, interleaved with options
and requires. Native compiler impacts require, so we must convert
"yes" to "no" before handling injections. As such the semantic
handling of the native command line argument must be separated from
the emission of the warning message, which this PR implements.
Fix #13819
In principle the other 2 cwarning in coqargs
(deprecated spropcumul and inputstate) should be moved to injections
too, but since they're deprecated I can't be bothered.
|
