aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2020-12-16Fix overlay system: projects need to be loaded before overlays.Gaëtan Gilbert
Also fixes is_in_projects
2020-12-15Merge PR #13632: [ci] Update pin ci scriptcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-12-14Update dev/tools/pin-ci.shEnrico Tassi
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-12-14[ci] simplify script to pin ci projectsEnrico Tassi
2020-12-14[ci] fix code to check if the overlay is validEnrico Tassi
2020-12-13Update dev/ci/user-overlays/README.mdEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-12[ci] update doc for overlaysEnrico Tassi
2020-12-12Merge PR #13603: [ci] function to declare projectscoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: RalfJung Ack-by: Zimmi48
2020-12-11Removing non relevant argument binding_kind of GLocalDef.Hugo Herbelin
2020-12-10[ci] update url of autosubstEnrico Tassi
2020-12-10[ci] remove old overlays so that people don't copy themEnrico Tassi
2020-12-10[ci] simplify overlay scriptsEnrico Tassi
2020-12-10Move Azure jobs to GitHub Actions.Théo Zimmermann
2020-12-09[ci] function to declare projectsEnrico Tassi
incidentally the "projects" array can be queried to get the list of projects
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 15:27:32 +0000