aboutsummaryrefslogtreecommitdiff
path: root/.gitlab-ci.yml
AgeCommit message (Collapse)Author
2021-03-07mathcomp analysis does not compire with Coq dev for nowCyril Cohen
2021-01-16Drop support for Coq 8.10 and deprecate the `deprecate` notationKazuhiko Sakaguchi
- The `deprecate` notation and `iota_add` have been deprecated. All the uses of the `deprecate` notation have been replaced with the `deprecated` attribute. - Deprecation aliases in `ssrnat` and `ssrnum` introduced in MathComp 1.11+beta1 have been removed. - Remove `VDFILE` related hacks from `Makefile.common`.
2021-01-15[CI/CD] support Coq 8.13Kazuhiko Sakaguchi
2021-01-09[CI/CD] Adding real-closed, analysis and multinomials (#692)Cyril Cohen
* Adding real-closed, analysis and multinomials to the CI * removing analysis for 8.10
2020-12-05Remove ci-fcsl-pcm-8.10Kazuhiko Sakaguchi
2020-11-11Intro pattern extensions for dup, swap and applyCyril Cohen
2020-11-07fix: Deploy each image w.r.t. a separate GitLab CI environment nameErik Martin-Dorel
to fully benefit from the "forward_deployment_failure" feature cf. https://docs.gitlab.com/ee/ci/environments/deployment_safety.html#skip-outdated-deployment-jobs Remark on environment names: > Caution: Some characters are not allowed in environment names. Use > only letters, numbers, spaces, and '-', '_', '/', '{', '}', or '.'. > Also, it must not start nor end with '/'. cf. https://docs.gitlab.com/ee/ci/environments/index.html
2020-10-12feat: Update only/except rulesErik Martin-Dorel
* Use only:refs, except:refs (available since GitLab 10.0) * Add except:variables/($CRON_MODE == "nightly") so coqbot can trigger the jobs currently chosen for scheduled pipelines, with a regular pipeline on master with variable CRON_MODE := nightly * Overall aim: rebuild coqorg/coq:dev & mathcomp/mathcomp-dev:coq-dev on GitLab CI after each successful update of coq.dev, using coqbot.
2020-10-07Turn class_of records into primitive records and get rid of the xclass idiomKazuhiko Sakaguchi
2020-09-27Merge pull request #530 from CohenCyril/moreCICyril Cohen
More CI
2020-09-27Update .gitlab-ci.ymlKazuhiko Sakaguchi
2020-09-11avoid rebuildEnrico Tassi
2020-09-11coq 8.13 does not exists yetEnrico Tassi
2020-09-11rm docker runEnrico Tassi
2020-09-10fixEnrico Tassi
2020-09-10new attemptEnrico Tassi
2020-09-07[test suite] infrastructure to test how some statements are printedEnrico Tassi
2020-08-29chore: refactor GitLab CI config a bit to lighten nightly buildsErik Martin-Dorel
* more precisely: jobs {coq-8.12, mathcomp-dev:coq-8.12} are unneeded in the scheduled pipeline https://gitlab.com/math-comp/math-comp/-/pipelines/182928354 * Insert commented jobs for upcoming coq-8.13 as well.
2020-06-08More CICyril Cohen
- fourcolor 8.11 and 8.12 - odd-order 8.11 and 8.12 - bigenough 8.11 and 8.12 - finmap 8.11 and 8.12
2020-06-07[CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha)Erik Martin-Dorel
2020-04-09- switching long suffixes to short suffixesReynald Affeldt
+ `odd_add` -> `oddD` + `odd_sub` -> `oddB` + `take_addn` -> `takeD` + `rot_addn` -> `rotD` + `nseq_addn` -> `nseqD` fixes #359
2020-03-08[ci] Build mathcomp/mathcomp-dev:8.11Erik Martin-Dorel
and test coq-lemma-overloading accordingly.
2020-03-08Fix CI (coq-lemma-overloading dropped compatibility with Coq < 8.10)Erik Martin-Dorel
2020-03-08refactor: Simplify the DockerfilesErik Martin-Dorel
* the CLI option --build-arg=compiler="${OPAM_SWITCH}" is now useless (it had been introduced to be able to compile Coq versions < 8.7, while mathcomp-dev now requires Coq 8.7+) * the "coqorg/base:bare" image now contains the two environment vars COMPILER and COMPILER_EDGE => clear COMPILER="" in mathcomp-dev's Dockerfile multi-stage build.
2020-01-07Add FCSL-PCM library to CIAnton Trunov
FCSL-PCM is in Coq's CI, so this will prevent breaking Coq's CI, see https://github.com/imdea-software/fcsl-pcm/issues/17
2019-12-18Remove CI overlay for PR #270Kazuhiko Sakaguchi
2019-12-15fix: Add missing "except: schedules"Erik Martin-Dorel
It seems adding an "except:" rule in a job that "extends:" another one *overwrites* the except rule, so we were getting too many jobs in the mathcomp-dev scheduled pipeline. Once merged, this patch should fix this.
2019-12-11The compatibility module in ssrnum should now be for version 1.10Kazuhiko Sakaguchi
2019-12-11remove ProdNormedZmodule (#419)affeldt-aist
* remove ProdNormedZmodule from ssrnum.v, it made its way to mathcomp-analysis in a generalized form (branch analysis_270) at the time of this writing * update gitlab-ci
2019-12-11renaming NormedZmoduleType and NormedZmoduleMixin (#416)affeldt-aist
* renaming NormedZmoduleType -> NormedZmodType NormedZmoduleMixin -> NormedZmodMixin that looks more homogeneous with regard to naming conventions used so far * update .gitlab-ci.yml * typo
2019-12-11Rename: (l|L)attice -> (d|D)istrLatticeKazuhiko Sakaguchi
2019-12-11editing documentation in order.v and ssrnum.vReynald Affeldt
2019-12-11Redefine `normedDomainType` (now `normedZmodType`) (#392)Kazuhiko Sakaguchi
* Redefine `normedDomainType` (now `normedZmodType`) - Redefine `normedDomainType` to drop ring and integral domain axioms. - Add canonical instance of `normedZmodType` for `prod`.
2019-12-11Rename `totalLatticeMixin` to `totalPOrderMixin` and several refactorKazuhiko Sakaguchi
- Rename `totalLatticeMixin` to `totalPOrderMixin`. - Refactor num mixins. - Use `Num.min` and `Num.max` rather than lattice notations if applicable.
2019-12-11Add (meet|join)_(l|r), some renamings, and small cleanupsKazuhiko Sakaguchi
New lemmas: - meet_l, meet_r, join_l, join_r. Renamings: - Order.BLatticeTheory.lexUl -> disjoint_lexUl, - Order.BLatticeTheory.lexUr -> disjoint_lexUr, - Order.TBLatticeTheory.lexIl -> cover_leIxl, - Order.TBLatticeTheory.lexIr -> cover_leIxr. Use `Order.TTheory` instead of `Order.Theory` if applicable
2019-10-18Add build for mathcomp/mathcomp-dev:coq-8.10 (#391)Erik Martin-Dorel
* feat: Add build for mathcomp/mathcomp-dev:coq-8.10 * fix(coq-mathcomp-ssreflect.opam): Bump coq upper bound * fix(*.opam): Remove "remove" directive href: coq/opam-coq-archive#703
2019-08-10fix(.gitlab-ci.yml): duplicated "variables:" entryErik Martin-Dorel
This could explain why the change in b8eadb8603b83c053a313b39c2a8f268385d8942 was not taken into account.
2019-07-30[ci] Adapt the GitLab CI config to allow scheduled builds for coq-devErik Martin-Dorel
* Normal builds (branches & GitHub PRs) are not impacted * Triggering a scheduled pipeline will only run {coq-dev, mathcomp-dev:coq-dev} to build and deploy the corresponding image to mathcomp/mathcomp-dev:coq-dev. * href: https://docs.gitlab.com/ce/user/project/pipelines/schedules.html
2019-07-30[ci] Add jobs {ci-fourcolor-8.9, ci-odd-order-8.9}Erik Martin-Dorel
* Add {fourcolor, odd-order} test builds with latest Coq release (8.9) * As a result, the math-comp CI config w.r.t. {fourcolor, odd-order} will be similar to that of the upstream repos: - https://github.com/math-comp/fourcolor/blob/master/.travis.yml - https://github.com/math-comp/odd-order/pull/16
2019-07-30refactor: deploy jobs need not clone the repoErik Martin-Dorel
* Set "GIT_STRATEGY: none" accordingly
2019-07-29style: fix indentation detailErik Martin-Dorel
2019-05-06add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma namesGeorges Gonthier
- add notation support for lemma renaming PRs, helping clients adjust to the name change by emitting warning or raising errors when the old name is used. The default is to emit warnings, but clients can change this to silence (if electing to delay migration) or errors (to help with actual migration). Usage: Notation old_id := (deprecate old_id new_id) (only parsing). —> Caveat 1: only prenex maximal implicit of `new_id` are preserved, so, as `Notation` does not support on-demand implicits, the latter should be added explicitly as in `(deprecate old new _ _)`. —> Caveat 2: the warnings are emitted by a tactic-in-term, which is interpreted during type elaboration. As the SSReflect elaborator may re-infer type in arguments multiple times (notably, views and arguments to `apply` and `rewrite`), clients may see duplicate warnings. - use the `deprecate` facility to introduce the first part of the refactoring of `seq` permutation lemmas : only lemmas concerning `perm_eq` should have `perm` as a component of their name. - document local additions in `ssreflect.v` and `ssrbool.v` - add 8.8 `odd-order` regression - the explicit beta-redex idiom use in the `perm_uniq` and `leq_min_perm` aliases avoids a strange name-sensitive bug of view interpretation in Coq 8.7.
2019-04-30Restore CI with `finmap master`Georges Gonthier
Following merge of math-comp/finmap#36
2019-04-30Fix compatibility for #237Georges Gonthier
- reprove rather than specialize `Some_inj` to allow for redefinition of `nonPropType` in `mathcomp.ssreflect.ssreflect` - retarget finmap CI to coq-9995-compatibility
2019-04-16[ci] Add tests with more librariesErik Martin-Dorel
- coq-mathcomp-odd-order.dev + coq.dev - coq-mathcomp-bigenough.dev, coq-{8.7, 8.8, 8.9, dev} - coq-mathcomp-finmap.dev, coq-{8.7, 8.8, 8.9, dev} The configs below are commented-out as the upstream repos' opam is not yet marked as compatible with mathcomp.dev (and Travis CI doesn't test it with mathcomp-dev images) # - coq-mathcomp-real-closed.dev, coq-{8.7, 8.8, 8.9, dev} # - coq-mathcomp-analysis.dev, coq-{8.8, 8.9, dev} Close math-comp/math-comp#245
2019-04-16Detail: Print a more legible description for the cloned external librariesErik Martin-Dorel
2019-04-16Swap the deploy and test stagesErik Martin-Dorel
so the images: - mathcomp/mathcomp-dev:coq-8.7 - mathcomp/mathcomp-dev:coq-8.8 - mathcomp/mathcomp-dev:coq-8.9 - mathcomp/mathcomp-dev:coq-dev will be pushed to Docker Hub even if a third-party library CI fails.
2019-04-16Print more debug informationErik Martin-Dorel
2019-04-16Refactor jobs: Split .opam-build & Create .docker-deployErik Martin-Dorel
* The latter template job is trusted and only runs: - in branch master, - if all build *and* test jobs were successful (major change in the deployment's condition) * The other jobs are not tagged with "environment: name: deployment", so they won't be able to read scoped protected variables. * href: https://gitlab.com/help/ci/variables/README.md#limiting-environment-scopes-of-variables-premium
2019-04-16Add commentary sections & Swap order of .make-build, .opam-buildErik Martin-Dorel
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:20:18 +0000