| Age | Commit message (Collapse) | Author |
|---|
|
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
|
|
It is more convenient to use recent versions of OCaml while developing
(better backtraces, etc).
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
Fixes #11726
|
|
We provide the closure of the dependencies manually.
This is still a hack, but not so bad given that the `source`'d files
still do contain that duplication too.
Dune should provide this functionality so we can replace both this
rule and the source files. Actually, that's not hard to implement,
`utop` already supports a printer attribute so these are loaded
automatically, so the ocamldebug mode could do the same.
Should fix #11716
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
|
|
New versions did remove the autogen.sh script in favor of plain
`autoreconf`
Note that the Coquelicot build documentation seems incorrect.
|
|
Raising inside exception printers is quite tricky as the order of
registration for printers will indeed depend on the linking order.
We thus forbid this, and make our API closer to the upstream
`Printexn` by having printers return an option type.
|
|
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Also renamed it to relative_entry_level.
Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused
Should not change global semantics (except error message in pr_arg).
|
|
|
|
notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
|
|
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: mattam82
|
|
Reviewed-by: ppedrot
|
|
packaging
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
|
|
beta versions.
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
No reason to have them in the same .sh
|
|
|
|
|
|
Motivations:
- We should have only maintained developments in our CI
- `make ci-fiat-crypto-legacy` takes about 15 mins before the first call
to `coqc`, making it unusable to work on overlays
- The coding style of this development is so fragile that adapting to
any change of behavior requires diffing gigabytes of Ltac traces.
@mattam82 and I have been blocked for 6 months this way, when working on
unifall.
I understand this development was meant to stress-test some components
like printing, but I think the trade-off is bad. We should rather come
up with specialized test suites for these components.
|
|
Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes
|
|
|
|
- Add a `--fuzz` option to `make-both-single-timing-files.py`
Passing `--fuzz=N` allows differences in character locations of up to
`N` characters when matching lines in per-line timing diffs.
The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`.
See also the discussion at
https://github.com/coq/coq/pull/11076#pullrequestreview-324791139
- Allow passing `--real` to per-file timing scripts and `--user` to
per-line timing script.
This allows easily comparing real times instead of user ones (or vice
versa).
- Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build
- We also now use argparse rather than a hand-rolled argument parser;
there were getting to be too many combinations of options.
- Fix the ordering of columns in Coq's build system; this is the
equivalent of #8167 for Coq's build system.
Fixes #11301
Supersedes / closes #11022
Supersedes / closes #11230
|
|
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
|
|
|
|
|
|
Fiat-Crypto does not guarantee compatibility with the tip of bedrock2,
only with the pinned version, and bedrock2 is still relatively unstable.
So we make the CI not have Fiat-Crypto depend on bedrock2, and instead
use the pinned submodule, by using `EXTERNAL_REWRITER=1
EXTERNAL_COQPRIME=1` rather than `EXTERNAL_DEPENDENCIES=1`.
|
|
It was virtually unused except in ssr, and there is no reason to clutter
the kernel with irrelevant code.
Fixes #9390: What is the purpose of the function "kind_of_type"?
|
|
Co-Authored-By: Jason Gross <jasongross9@gmail.com>
|
|
The computation of which files to build is now mostly cached rather than
computed, eliminting basically all of the wait-time from `make` to the
first invocation of `coqc`.
Note that we no longer need to invoke
`./etc/ci/remove_autogenerated.sh`, but it does not hurt, and it speeds
up `coqdep` somewhat significantly.
Fixes #9298
|
