| Age | Commit message (Collapse) | Author |
|---|
|
We factorize code from declareInd.ml and inductiveops.ml which was
already existing in record.ml.
We keep expansion of local definitions in the type of fields of
primitive records while these are not expanded in the non-primitive
case. This is to be consistent with what Indtypes.compute_projections
is doing. See discussion at #11135.
We keep the unused code from inductiveops.ml for possible future use
though.
Include improvements contributed by Gaëtan Gilbert.
|
|
Ack-by: Zimmi48
Ack-by: cpitclaudel
|
|
|
|
to reflect lexer requirement for no space
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: MSoegtropIMC
Reviewed-by: ppedrot
Ack-by: tchajed
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
We inline the "with_evars := false" case.
|
|
The effects field of the UniqueProjection constructor was never accessed.
|
|
This makes some invariants explicit and is 1:1 equivalent.
|
|
|
|
Reviewed-by: ppedrot
|
|
definitions.
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
Cf. #12049.
|
|
Reviewed-by: JasonGross
|
|
As of today flambda is pretty stack-hungry for some developments, in
particular it doesn't work [`StackOverflow` in fiat-crypto extracted
code even with large stacks.
We are thus forced to revert fiat-crypto's compilation to the regular
OCaml compiler.
This is OCaml bug https://github.com/ocaml/ocaml/issues/7842
|
|
Reviewed-by: anton-trunov
|
|
|
|
This is useful as witnessed by #11829 , as some errors printers do
still fail, so it costs little to have both backtraces.
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
|
|
|
|
|
|
Let vs Definition / Example syntax was split in 7c28130 for parsing
reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could
be introduced. This split is probably the reason why Let was
overlooked when support for universe bindings and universe constraints
were added to Definition and variants.
|
|
|
|
|
|
Being able to inspect the generated OCaml code is a useful debug tool.
It seems this was disabled by mistake in #11081.
|
|
cleanall
Reviewed-by: gares
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: mattam82
|
|
Reviewed-by: ejgallego
|
|
The location was missing in the parser.
|
|
|
|
|
|
|
|
It seems that this PR is making the rewrite much, much faster.
|
|
A quick analysis showed that most of the calls to whd do not lead to a
term which further triggers reduction, so there is no point in refolding
a potentiall huge term for no reason.
|
|
There is no point in using the exaggerately inefficient Reductionops machine.
We need to be call-by-name to preserve the shape of the reduced terms, as
call-by-need would introduce sharing and thus at-distance effects in term
refolding. Yet, the Reductionops machine is worse than that, since it performs
substitutions eagerly, leading to a catastrophical performance profile.
Instead, we use the kernel reduction in by-name mode to replace the Reductionops
machine in whd_betaiota_deltazeta_for_iota_state with all flags on. Since the
kernel is using explicit substitutions, this is algorithmically more efficient.
Apart from minor differences, this should produce the same normal form.
As showed by the benchmarks, this is a critical change for the odd-order proofs.
Ideally, we should use delayed substitutions in the Reductionops machine as well
for great profit, but due to code entanglement this is a much less self-contained
change.
|
|
Reviewed-by: ejgallego
|
|
autogen.sh was removed in https://gitlab.inria.fr/flocq/flocq/-/commit/d679d3770aea2ff8608c77096158653837798124
|
|
parsing of coqtop arguments in coqide
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: jfehrle
|
|
This octopus merge is meant to preserve the commit history / blame of
all the parts.
|
