aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2020-12-11Bench: add .log extension to .stdout/stderr filesGaëtan Gilbert
Hopefully this allows viewing online with a download dialog on gitlab.
2020-12-10Move Azure jobs to GitHub Actions.Théo Zimmermann
2020-12-09Adding overlays.Pierre-Marie Pédrot
2020-12-09[rm] announcements to discourseEnrico Tassi
2020-12-08Update dev/doc/release-process.mdEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-07[rm] manual is uploaded by CIEnrico Tassi
2020-12-07[rm] update instructions for windows signingEnrico Tassi
2020-12-04Merge PR #13497: [rm] update release notescoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-04[rm] clarify process for is_a_released_version = trueEnrico Tassi
2020-12-04[rm] update git commands to push tagsEnrico Tassi
2020-12-02Merge PR #13472: [ci] Add job for gappacoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: ejgallego
2020-11-30[ci] add job for gappaEnrico Tassi
2020-11-30[docker] install boost, mpfr, flex, bison, autoconf-archiveEnrico Tassi
2020-11-30dune: Don't echo "$(pwd)" when creating the shimsGaëtan Gilbert
AFAICT `echo "$(pwd)"` is unsound for the dune cache when called from different paths (typically different git worktrees).
2020-11-28Merge PR #13487: CI: Use hash of dockerfile in CACHEKEYcoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: gares
2020-11-27[RM] script to notify "platform" projects to tagEnrico Tassi
2020-11-26CI: Use hash of dockerfile in CACHEKEYGaëtan Gilbert
Checked by the linter so we don't forget to update it. Also checked by before_script so we don't run jobs for nothing.
2020-11-26Merge PR #13467: [ci] add job for intervalcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: silene
2020-11-26[ci] interval, disable native-computeEnrico Tassi
2020-11-26[ci] coquelicot, depend on ssr properEnrico Tassi
2020-11-26[ci] avoid always rebuilding jobs that use remakeEnrico Tassi
2020-11-26[ci] separate oddorder and fourcolor from mathcompEnrico Tassi
In this way interval does not have to wait too much
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
Reviewed-by: mattam82
2020-11-26[ci] bump elpi to 1.12.0Enrico Tassi
2020-11-26[ci] add job for intervalEnrico Tassi
2020-11-26[ci] coquelicot, run make installEnrico Tassi
2020-11-26Merge PR #13464: [CI] Compcert uses system libscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-11-25[docker] don't install ocamlformatEnrico Tassi
2020-11-25[ci] make compcert use flocq and menhirEnrico Tassi
2020-11-25[ci] job for menhirEnrico Tassi
2020-11-25Overlays for #13415Gaëtan Gilbert
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
This allows proper treatment in notations, ie fixes #13303 The "glob" representation of universes (what pretyping sees) contains only fully interpreted (kernel) universes and unbound universe ids (for non Strict Universe Declaration). This means universes need to be understood at intern time, so intern now has a new "universe binders" argument. We cannot avoid this due to the following example: ~~~coq Module Import M. Universe i. End M. Definition foo@{i} := Type@{i}. ~~~ When interning `Type@{i}` we need to know that `i` is locally bound to avoid interning it as `M.i`. Extern has a symmetrical problem: ~~~coq Module Import M. Universe i. End M. Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}. Print foo. (* must not print Type@{i} -> Type@{i} *) ~~~ (Polymorphic as otherwise the local `i` will be called `foo.i`) Therefore extern also takes a universe binders argument. Note that the current implementation actually replaces local universes with names at detype type. (Asymmetrical to pretyping which only gets names in glob terms for dynamically declared univs, although it's capable of understanding bound univs too) As such extern only really needs the domain of the universe binders (ie the set of bound universe ids), we just arbitrarily pass the whole universe binders to avoid putting `Id.Map.domain` at every entry point. Note that if we want to change so that detyping does not name locally bound univs we would need to pass the reverse universe binders (map from levels to ids, contained in the ustate ie in the evar map) to extern.
2020-11-24[ci] variable CI_INSTALL_DIR to use with --prefixEnrico Tassi
2020-11-24Merge PR #13466: Fix linter: incorrect commit was picked in CIcoqbot-app[bot]
Reviewed-by: ejgallego
2020-11-24Merge PR #13420: Modular printing algorithm for bench/render_results.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-24Fix linter: incorrect commit was picked in CIGaëtan Gilbert
The bot merge was changed some time ago.
2020-11-22Adding debugging printer for stacks of EConstr.Hugo Herbelin
2020-11-21Merge PR #13431: Make sure accumulators do not exceed the minor heap (partly ↵coqbot-app[bot]
fix #11170). Reviewed-by: gares Reviewed-by: xavierleroy Ack-by: ppedrot
2020-11-20Merge PR #13352: Configure default value of -native-compilercoqbot-app[bot]
Reviewed-by: erikmd Reviewed-by: silene Ack-by: mattam82 Ack-by: Blaisorblade Ack-by: gares Ack-by: Zimmi48 Ack-by: SkySkimmer Ack-by: ejgallego
2020-11-20Merge PR #13233: add perennial to benchmark suitePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-20[CI] Deactivate native-compiler in some jobsPierre Roux
A few libraries in the CI don't compile with it (out of memory).
2020-11-20Make sure accumulators do not exceed the minor heap (partly fix #11170).Guillaume Melquiond
Accumulators can grow arbitrarily large, even when well-typed. So, this commit makes sure they are allocated on the major heap when they are too large. If so, fields need to be filled with caml_initialize, in case they point to the minor heap.
2020-11-20add perennial to benchmark suiteRalf Jung
2020-11-19Add overlays for elpi and unicoq.Hugo Herbelin
2020-11-19Modular printing algorithm for bench/render_results.Pierre-Marie Pédrot
The old code was a mess of handwritten ad-hoc code to print the result table in a fancy way. Instead of hardcoding everything this patch introduces a generic function to print a table of data. This will allow extension of the profiling information displayed to the user in an easy way.
2020-11-18Merge PR #13312: [attributes] Allow boolean, single-value attributes.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: SkySkimmer Ack-by: gares
2020-11-18Merge PR #13389: [ci/gitlab/windows] Do not load user overlays.Michael Soegtrop
Reviewed-by: MSoegtropIMC
2020-11-18[attributes] Add overlays for #13312Emilio Jesus Gallego Arias
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot
2020-11-17[ci] Use lite target for PerennialTej Chajed
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 14:18:47 +0000