aboutsummaryrefslogtreecommitdiff
path: root/.gitlab-ci.yml
AgeCommit message (Collapse)Author
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
2019-04-04remove support for Coq 8.6Enrico Tassi
2019-04-01Improve CI head trackingGeorges Gonthier
As per @ejgallego ’s suggestion.
2019-01-29Add more libraries to CI & Update local opam doc (#272)Erik Martin-Dorel
* Update INSTALL.md for installing mathcomp as local opam packages This patch documents the change 1046da99d22462d6aeb23dd12043c2537f47abf1 that was required by the GitLab CI setup to be able to rely on opam 2.0. Close #251 * Propose to bump the required version of coq in coq-mathcomp-ssreflect.opam so the CI could use the Docker image coqorg/coq:8.9 (which is already available albeit it currently is a synonymous of coqorg/coq:8.9-beta1 with the opam repos coq-released + coq-core-dev + coq-extra-dev) * [ci] Add math-comp/odd-order and coq-community/lemma-overloading jobs Related: math-comp/math-comp#245 and math-comp/math-comp#256
2018-12-21Add hidden job .make-build to also test the Makefile build infraErik Martin-Dorel
* This job is only instantiated with coqorg/coq:latest * Add the associated Dockerfile.make
2018-12-21chore: s/.build/.opam-build/Erik Martin-Dorel
2018-12-21Add Docker-based GitLab CI configurationErik Martin-Dorel
* Design: - build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.6 .) - choice of the OCaml compiler: var OPAM_SWITCH in {base, edge} (Dockerfile containing: "opam switch set $compiler && eval $(opam env)") - master (protected branch) => push on GitLab registry and Docker Hub - other branches (not tags) => push on GitLab registry - Todo: GitHub PRs => push on GitLab - test stage (image: mathcomp-dev:$IID_$SLUG_coq-8.6) - script template foreach project (custom CONTRIB_URL, script) - jobs foreach project and Coq version (custom COQ_VERSION, CONTRIB_VERSION) * Config for protected branches: - set vars HUB_REGISTRY, HUB_REGISTRY_USER, HUB_REGISTRY_IMAGE, HUB_TOKEN * Remark: - The name chosen for branches should ideally yield different values of CI_COMMIT_REF_SLUG. - But this is not mandatory as image tags start with "${CI_PIPELINE_IID}_". cf. doc: - CI_COMMIT_REF_NAME: The branch or tag name for which project is built. - CI_COMMIT_REF_SLUG: $CI_COMMIT_REF_NAME lowercased, shortened to 63 bytes, and with everything except 0-9 and a-z replaced with -. No leading / trailing -. Use in URLs, host names and domain names. - CI_PIPELINE_IID: The unique id of the current pipeline scoped to project.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 17:38:19 +0000