| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-09 | fix copy-paste error in CI_ARCHIVEURL | Christian Doczkal | |
| 2018-12-09 | add relation-algebra to CI test suite | Christian Doczkal | |
| 2018-12-05 | [ci] Add four color theorem proof to CI | Emilio Jesus Gallego Arias | |
| 2018-12-04 | CI: track dev branch of coq-simple-io | Yishuai Li | |
| 2018-11-21 | Remove pidetop from CI | Maxime Dénès | |
| pidetop relies on some rather low level API from STM, which we'd like to change. It does not seem maintained much anymore, and still hasn't moved to github. | |||
| 2018-11-17 | [ci] Uniformize casing of makefile targets and ci variables. | Emilio Jesus Gallego Arias | |
| This is convenient as to have better automation. | |||
| 2018-11-13 | Merge PR #8976: CoqHammer CI | Gaëtan Gilbert | |
| 2018-11-12 | CoqHammer CI | Lukasz Czajka | |
| 2018-11-10 | [ci] Add paramcoq to CI. | Emilio Jesus Gallego Arias | |
| 2018-10-26 | Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit." | Gaëtan Gilbert | |
| This reverts commit df69c44af03f2587b3f1706a805d0e2728c1f1dc. Should be merged before any PR with plugin tutorial overlays, or we can just merge the vendor PR instead. | |||
| 2018-10-18 | [ci] Pin CI_REF to plugin_tutorial to use not yet merged commit. | Théo Zimmermann | |
| This fixes the CI until this commit is merged into master. | |||
| 2018-10-08 | [ci] Add aac-tactics. | Théo Zimmermann | |
| And fix a typo that was previously there. | |||
| 2018-10-05 | CI: fix Iris and stdpp ref selection | Gaëtan Gilbert | |
| This was broken due to a typo when introducing the archive download method. We also remove default [master] values from basic-overlay which hid this issue. | |||
| 2018-10-03 | Fix issue #8321 "Add more useful addons to the Windows Installer" | Michael Soegtrop | |
| Implemented by merging addon changes in V8.8.2 (keeping everything on master) | |||
| 2018-10-01 | [ci] Add plugin-tutorial to CI. | Emilio Jesus Gallego Arias | |
| This closes #7618. | |||
| 2018-08-31 | Download tarball instead of cloning external projects (when $CI is set). | Théo Zimmermann | |
| This allows to use fixed commits and not just branches or tags. We keep using git clone when $FORCE_GIT is set (for projects on gforge.inria.fr and projects pulling dependencies through git submodules). fiat-parsers also calls git submodule, but inside its own Makefile. | |||
| 2018-08-31 | [ci] Fix QuickChick by adding new simple-io dependency. | Théo Zimmermann | |
| 2018-06-27 | Add mit-plv/bedrock2-ci to CI | Andres Erbsen | |
| 2018-06-25 | Reuse CI info to know which version of plugins to build on Windows. | Théo Zimmermann | |
| 2018-06-21 | Update dpdgraph branch name | Gaëtan Gilbert | |
| See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context | |||
| 2018-06-02 | QuickChick CI | Leonidas Lampropoulos | |
| 2018-05-16 | [ci] Don't build lite versions of CI developments. | Emilio Jesus Gallego Arias | |
| In the original Travis CI setup, the per-job time limit was an issue. However, Gitlab has much improved this problem due to a) Coq not being built for each contrib, b) user-configurable time limit. We thus disable the expensive builds from Travis: `fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`, `math-comp`, `unimath`, `vst` and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`] in full. We also update the `math-comp` script as the `odd-order` theorem lives in a separate repository and it is a key CI case. | |||
| 2018-05-09 | [ci] Add mit-plv/cross-crypto | Jason Gross | |
| I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything. | |||
| 2018-05-02 | [ci]: add pidetop (fix #7336) | Enrico Tassi | |
| 2018-04-25 | updating CI for Mtac2 | Beta Ziliani | |
| 2018-04-20 | CI: add fcsl-pcm | Anton Trunov | |
| 2018-04-13 | Update the CI branch for Equations. | Théo Zimmermann | |
| 2018-02-19 | ci: add elpi | Enrico Tassi | |
| 2018-02-05 | Points to Flocq official repository. | Théo Zimmermann | |
| Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528. | |||
| 2018-01-16 | Source basic overlay before user overlays. | Gaëtan Gilbert | |
| 2017-12-07 | [ci] CoLoR has moved to github | Emilio Jesus Gallego Arias | |
| Closes #6194 . | |||
| 2017-11-20 | Add Equations to CI | Matthieu Sozeau | |
| 2017-11-13 | Merge PR #6071: [ci] Add Ltac2 | Maxime Dénès | |
| 2017-11-04 | [ci] Add Ltac2 | Jason Gross | |
| 2017-10-30 | [ci] Switch VST back to upstream. | Théo Zimmermann | |
| This finally closes #5994. | |||
| 2017-10-27 | [ci] Switch back to upstream version of Math-Classes and Corn. | Théo Zimmermann | |
| 2017-10-25 | Merge PR #6003: Point HoTT back at master, which now supports Coq master | Maxime Dénès | |
| 2017-10-23 | Point HoTT back at master, which now supports Coq master | Jason Gross | |
| 2017-10-20 | Switch testing branch back to CompCert upstream. | Théo Zimmermann | |
| This follows the merge of AbsInt/CompCert#191. | |||
| 2017-10-19 | CI: build lambdaRust (which depends on Iris) rather than just Iris | Ralf Jung | |
| 2017-10-04 | [ci] Remove temporary bignums overlay. | Théo Zimmermann | |
| 2017-09-07 | Merge PR #914: Making the detyper lazy | Maxime Dénès | |
| 2017-09-05 | Fix Software Foundations build. | Maxime Dénès | |
| The Software Foundations archive has been replaced by three volumes. | |||
| 2017-09-04 | Making detyping potentially lazy. | Pierre-Marie Pédrot | |
| The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. | |||
| 2017-07-28 | Merge PR #782: Update API for fiat | Maxime Dénès | |
| 2017-07-18 | [ci] VST is now built with IGNORECOQVERSION=true. | Théo Zimmermann | |
| 2017-07-04 | Revert fiat-crypto overlay | Jason Gross | |
| Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6. | |||
| 2017-06-15 | Merge PR#778: Revert "[travis] temporary UniMath overlay" | Maxime Dénès | |
| 2017-06-15 | Update fiat-parsers overlay | Jason Gross | |
| 2017-06-15 | Remove bedrock from test suite. | Maxime Dénès | |
| Bedrock relies on the 8.4 compat flag that we are removing, and we heard from MIT that they did not plan to port bedrock to more recent versions of Coq. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |