aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2020-05-19Merge PR #12353: Update release-process.mdEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-18Bump minimal versions of refman dependencies.Théo Zimmermann
Fixes #11936. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-05-18[ci] Old overlay cleanup.Emilio Jesus Gallego Arias
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Update to 8.13.Théo Zimmermann
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
2020-05-18Direct URL for triggering a pipeline with SKIP_DOCKER=false.Théo Zimmermann
2020-05-16[ci] [azure] Rework windows Azure pipelineEmilio Jesus Gallego Arias
- use a different mirror for main cygwin archive - (always) publish build log as artifact - fix call to dune makefiles - we do just build Coq for now, as: + dune is rebuilding Coq to run the test-suite, this needs move investigation. + the test suite seems to take long and it times-out on Win.
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: kyoDralliam
2020-05-16Merge PR #12335: Clarify release-process.mdThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-16Merge PR #11566: [misc] Better preserve backtraces in several modulesPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-05-15Add overlays for coqhammer and coq-dpdgraph.Hugo Herbelin
2020-05-15Update dev/doc/release-process.mdEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-05-15Merge PR #11979: Add a rudimentary script to generate release changelog.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-05-15Clarify release-process.mdEnrico Tassi
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-15Merge PR #12032: [win] Elpi, Coq-Elpi and HBMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
Re-raising inside exception handlers must be done with care in order to preserve backtraces; even if newer OCaml versions do a better job in automatically spilling `%reraise` in places that matter, there is no guarantee for that to happen. I've done a best-effort pass of places that were re-raising incorrectly, hopefully I got the logic right. There is the special case of `Nametab.error_global_not_found` which is raised many times in response to a `Not_found` error; IMHO this error should be converted to something more specific, however the scope of that change would be huge as to do easily...
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: gares
2020-05-14[ci] [sf] Fix SF build.Emilio Jesus Gallego Arias
We move from the previous complex CI download setup to a much more straightforward public mirror repository. Thanks to Yishuai Li and Benjamin Pierce for the very quick response. Closes #12290
2020-05-13Overlay elpiHugo Herbelin
2020-05-10Add overlays.Pierre-Marie Pédrot
2020-05-10Merge PR #12286: [sphinx] Add links to other versions of the refmanThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-09[sphinx] Add links to other versions of the refmanClément Pit-Claudel
2020-05-09Add overlaysPierre Roux
2020-05-09Merge PR #12040: Document the signing procedure of released binary packages.Maxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2020-05-07[win] CI build addons Coq-Elpi Hierarchy-BuilderEnrico Tassi
2020-05-07[win] addon for Hierarchy BuilderEnrico Tassi
2020-05-07[win] addon for elpiEnrico Tassi
2020-05-07[win] rules to build ElpiEnrico Tassi
2020-05-07[win] bump camlp5 to 7.11 since OCaml 4.08 requires itEnrico Tassi
Also fix an installation issue
2020-05-07[win] since 4.07 the seq package is part of ocamlEnrico Tassi
2020-05-07[win] Coq trunk is now called masterEnrico Tassi
The old script was still working but downloading an old version, probably there is a git ref called trunk somewhere
2020-05-07[ci] overlay for coq-elpiEnrico Tassi
2020-05-06[ci] bump elpi to 1.11Enrico Tassi
2020-05-05Merge PR #12227: Spring cleaning of the tactic compatibility layerEnrico Tassi
Reviewed-by: gares
2020-05-04update documentation for overlay buildingOlivier Laurent
2020-05-03Add overlays.Pierre-Marie Pédrot
2020-05-01Merge PR #12217: Fix #12215: ci scripts naming inconsistenciesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-30renaming in Makefile.ci and ci scripts to avoid inconsistenciesOlivier Laurent
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-29Merge PR #12198: CI: change ext-lib url, it is at coq-community nowEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-04-29Merge PR #12174: [ci] Add coq-tools to the CIThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29correct script name create_overlays.shOlivier Laurent
2020-04-29CI: ext-lib is at coq-community nowAntonio Nikishaev
2020-04-27[ci] Add coq-tools to the CIJason Gross
After #12023 broke the bug minimizer, I'd like to add [coq-tools](https://github.com/JasonGross/coq-tools/) to the CI. It's relatively light-weight (under 5 minutes, I believe), and I'd like to know when it's going to break on master before it's broken, rather than after. It tests a relatively under-tested part of Coq, mostly (the display output of error message, by and large), and I'm happy to take responsibility for fixing it when some PR is going to break it (mainly I just want a sort-of early warning system, and I want PRs to not accidentally break it by changing things that they don't realize they're changing).
2020-04-26Document the signing procedure of released binary packages.Pierre-Marie Pédrot
2020-04-23Merge PR #12130: [declare] [tactics] Move declare to `vernac`Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-21Overlay for fiat-crypto, Mtac2, MetaCoq and UniMath.Hugo Herbelin
2020-04-21Adding a Declare ML Module in empty file Ltac.v.Hugo Herbelin
Indeed, it would be intuitive that `Require Import Ltac` is an equivalent for Ltac of `Require Import Ltac2.Ltac2`. Also declaring the classic proof mode.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 00:04:51 +0000