| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: SkySkimmer
|
|
This job is currently broken because of Dune 2.5 not being available
yet on the mingw-opam-repository.
Before this, it was already red most of the time because of two
issues:
- Cygwin cannot be downloaded
- "Error on dynamically loaded library:
.\kernel/byterun\dllbyterun_stubs.dll: The specified module could not
be found" bug."
We don't know exactly when the latter appeared. It was missed because
of the former.
The goal is to reenable Windows testing based on standard opam with no
cygwin. Hopefully, this is achievable in the next few weeks.
|
|
Reviewed-by: Zimmi48
|
|
These targets are redundant with the shims.
We also improve the documentation quite a bit.
|
|
This completes a pure Dune bootstrap of Coq.
There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.
TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.
Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?
|
|
It is unfortunate that we cannot install coqide and Dune 2.5.0 in < 4.07.0
|
|
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.
|
