| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-01-19 | Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵ | Pierre-Marie Pédrot | |
| pattern Reviewed-by: ppedrot | |||
| 2021-01-18 | Adding overlay for perennial. | Hugo Herbelin | |
| 2021-01-18 | Support locality attributes for Hint Rewrite (including export) | Gaëtan Gilbert | |
| We deprecate unspecified locality as was done for Hint. Close #13724 | |||
| 2021-01-13 | Merge PR #13740: [osx] macpack also coqidetop (for libgmp) | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC | |||
| 2021-01-13 | Merge PR #13598: [ci] window jobs based on the platform | Michael Soegtrop | |
| Ack-by: MSoegtropIMC Ack-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2021-01-12 | [osx] macpack all binaries, not just coqide | Enrico Tassi | |
| 2021-01-12 | Merge PR #13704: [ci] [coq-performance-tests] Errors at end of log | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Ack-by: gares | |||
| 2021-01-11 | [ci] [coq-performance-tests] Errors at end of log | Jason Gross | |
| By running `make -k; make` whenever `make` initially fails, we can get error messages to occur at the end of the log. This way they'll show up on the GitHub Actions preview/summary, rather than me having to go digging for them in the GitLab logs. | |||
| 2021-01-09 | Merge PR #13299: Remember universe instances of constants in notations | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: herbelin | |||
| 2021-01-07 | Merge PR #13718: Move printing and sorting out of AcyclicGraph | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-01-06 | Further pushing up the printing and sorting of universes. | Pierre-Marie Pédrot | |
| We expose the representation function in UGraph and change the printer signature to work over the representation instead of the abstract type. Similarly, the topological sorting algorithm is moved to Vernacentries. It is now even simpler. | |||
| 2021-01-05 | [ci] windows job based on the platform | Enrico Tassi | |
| 2021-01-04 | Remember universe instances of constants in notations | Jasper Hugunin | |
| 2021-01-04 | Document the change of case representation. | Pierre-Marie Pédrot | |
| 2021-01-04 | Add overlays. | Pierre-Marie Pédrot | |
| 2021-01-04 | Change the representation of kernel case. | Pierre-Marie Pédrot | |
| We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval. | |||
| 2021-01-04 | Merge PR #13685: Add a debug printer for fconstr substitutions. | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-01-04 | [win] remove old scripts, we now use the platform ones | Enrico Tassi | |
| 2021-01-01 | Merge PR #13693: [ci] Switch to testing the maintenance branch for Flocq 3. | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2020-12-30 | Merge PR #13692: Fix failing Windows CI builds. | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2020-12-30 | Merge PR #13321: Move evaluable_global_reference from Names to Tacred. | coqbot-app[bot] | |
| Reviewed-by: herbelin Ack-by: ejgallego | |||
| 2020-12-30 | Fix failing Windows CI builds. | Théo Zimmermann | |
| Following a recent change in Cygwin. Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com> | |||
| 2020-12-30 | [ci] Switch to testing the maintenance branch for Flocq 3. | Théo Zimmermann | |
| This is the version that CompCert will be compatible with for the time being. | |||
| 2020-12-28 | Register a printer for fconstr substitutions in the kernel. | Pierre-Marie Pédrot | |
| 2020-12-28 | Merge PR #13665: Set Python's default output encoding to utf-8 | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 Ack-by: palmskog | |||
| 2020-12-26 | Set the locale in Docker so Python's default output encoding is utf-8 | Jim Fehrle | |
| 2020-12-21 | Add overlays. | Pierre-Marie Pédrot | |
| 2020-12-18 | Do not load overlay data (workaround to fix CI). | Théo Zimmermann | |
| 2020-12-17 | [ci/gitlab/windows] Bump OCaml to 4.10.2 to fix Windows CI. | Théo Zimmermann | |
| 2020-12-16 | Merge PR #13644: Fix overlay system: projects need to be loaded before overlays. | coqbot-app[bot] | |
| Reviewed-by: gares | |||
| 2020-12-16 | Merge PR #13616: Bench: add .log extension to .stdout/stderr files | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-12-16 | Fix overlay system: projects need to be loaded before overlays. | Gaëtan Gilbert | |
| Also fixes is_in_projects | |||
| 2020-12-15 | Merge PR #13615: Document the manual tasks that I need to do at each release. | coqbot-app[bot] | |
| Reviewed-by: ejgallego | |||
| 2020-12-15 | Merge PR #13633: [ci] uniform name of projects w.r.t. opam packages | coqbot-app[bot] | |
| Reviewed-by: ejgallego | |||
| 2020-12-15 | Merge PR #13632: [ci] Update pin ci script | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2020-12-15 | [ci] uniform name of projects w.r.t. opam packages | Enrico Tassi | |
| This makes it easier to track projects across Coq's CI and the platform | |||
| 2020-12-14 | Update dev/tools/pin-ci.sh | Enrico Tassi | |
| Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2020-12-14 | [ci] simplify script to pin ci projects | Enrico Tassi | |
| 2020-12-14 | [ci] fix code to check if the overlay is valid | Enrico Tassi | |
| 2020-12-13 | Update dev/ci/user-overlays/README.md | Enrico Tassi | |
| Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> | |||
| 2020-12-12 | [ci] update doc for overlays | Enrico Tassi | |
| 2020-12-12 | Merge PR #13603: [ci] function to declare projects | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Ack-by: RalfJung Ack-by: Zimmi48 | |||
| 2020-12-11 | Removing non relevant argument binding_kind of GLocalDef. | Hugo Herbelin | |
| 2020-12-11 | Bench: add .log extension to .stdout/stderr files | Gaëtan Gilbert | |
| Hopefully this allows viewing online with a download dialog on gitlab. | |||
| 2020-12-11 | Document the manual tasks that I need to do at each release. | Théo Zimmermann | |
| 2020-12-10 | [ci] update url of autosubst | Enrico Tassi | |
| 2020-12-10 | [ci] remove old overlays so that people don't copy them | Enrico Tassi | |
| 2020-12-10 | [ci] simplify overlay scripts | Enrico Tassi | |
| 2020-12-10 | Move Azure jobs to GitHub Actions. | Théo Zimmermann | |
| 2020-12-09 | [ci] function to declare projects | Enrico Tassi | |
| incidentally the "projects" array can be queried to get the list of projects | |||
