aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2019-02-05[Nix-CI] Add IrisVincent Laporte
2019-02-05[Nix-CI] Fix UnicoqVincent Laporte
2019-02-05OverlaysMaxime Dénès
2019-02-04Merge PR #9470: the default branch of Mtac2 changed to masterEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-02-04the default branch of Mtac2 changed to masterbeta
2019-02-04Remove AppVeyor: superseded by Azure.Théo Zimmermann
2019-02-04Overlays.Maxime Dénès
2019-02-04Dockerfile: update menhir from 20180530 to 20181113Vincent Laporte
2019-01-29Merge PR #9383: Remove travisVincent Laporte
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2019-01-24Add OverlaysMaxime Dénès
2019-01-24[nix-CI] Split the build inputsVincent Laporte
Coq and the Coq libraries can now be excluded (by setting the NOCOQ environment variable).
2019-01-24[Nix-ci] Add QuickChickVincent Laporte
2019-01-24[Nix-ci] Fix UnicoqVincent Laporte
2019-01-24[Nix-ci] Add formal-topologyVincent Laporte
2019-01-23Merge PR #9239: [ci] [appveyor] Pass -j2 to Appveyor's build and build test ↵Maxime Dénès
suite again
2019-01-22Remove travisGaëtan Gilbert
The azure OSX job replaces the first travis job, and the second always fails and so is useless.
2019-01-22Merge PR #9225: Fix issue: Windows CI: cygwin install cache is not reused #9212Maxime Dénès
Reviewed-by: maximedenes
2019-01-17Merge PR #9345: [ci] Update fiat-crypto to the new pipelineGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-01-17Merge PR #9192: Issue #9175, #9190, #9191 (various minor Windows build issues)Maxime Dénès
Reviewed-by: Zimmi48
2019-01-16[ci] Update fiat-crypto to the new pipelineJason Gross
We're recently reorganized fiat-crypto. This should fix the OOM CI issues. Fixes #9338
2019-01-11Merge pull request #8778 from SkySkimmer/merge-plugin-tutoYves Bertot
Move plugin tutorial to Coq repo
2019-01-08[ci] Update fiat-crypto legacyJason Gross
Once https://github.com/mit-plv/fiat-crypto/pull/477 is merged, the master branch will no longer contain the files nor the targets for fiat-crypto legacy. (We should perhaps consider moving fiat-crypto legacy to coq-community as a source of vm and printing tests.)
2019-01-08Integrate plugin tutorial after code importGaëtan Gilbert
2019-01-07Merge PR #9309: [ci] Add Verdi Raft with dependencies to CIEmilio Jesus Gallego Arias
2019-01-05[ci] Add Verdi Raft with dependencies to CIKarl Palmskog
2019-01-04Remove formal-topology from CIMaxime Dénès
This was suggested by the author. See https://github.com/bmsherman/topology/issues/23
2018-12-27Merge PR #9224: Move lint job to gitlabEmilio Jesus Gallego Arias
2018-12-25[ci] [appveyor] Pass -j2 to Appveyor's build.Emilio Jesus Gallego Arias
2018-12-21Move lint job to gitlabGaëtan Gilbert
This changes the semantics a bit since we don't have TRAVIS_COMMIT_RANGE anymore, instead we do per-commit linting for the commits since the last merge commit.
2018-12-20Fix line ending issuesGaëtan Gilbert
Try to mimick MSoegtropIMC (https://github.com/coq/coq/pull/9243#issuecomment-448968353 )
2018-12-18Merge PR #9215: Set up CI with Azure PipelinesEmilio Jesus Gallego Arias
2018-12-17Merge PR #9153: [api] Move reduction modules to `tactics`Pierre-Marie Pédrot
2018-12-17Set up CI with Azure PipelinesGaëtan Gilbert
2018-12-17Merge PR #8856: [gitlab] Test Ocaml trunk.Gaëtan Gilbert
2018-12-17Merge PR #9220: Move shallow state logic to the function preparing state for ↵Enrico Tassi
workers
2018-12-16Merge PR #9172: [proof] Rework proof interface.Pierre-Marie Pédrot
2018-12-14Fix issue: Windows CI: cygwin install cache is not reused #9212Michael Soegtrop
2018-12-14[dune] [gitlab] Test OCaml trunk.Emilio Jesus Gallego Arias
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`] CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit` cannot be currently installed, thus we have to add a switch to the test suite to disable `unit-tests`. Many deprecation warnings happened in 4.08 so we use the `release` profile to make them not fatal. Using a 4.08 build profile would be an option too.
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
- deprecate the old 5-tuple accessor in favor of a view record, - move `name` and `kind` proof data from `Proof_global` to `Proof`, this will prove useful in subsequent functionalizations of the interface, in particular this is what abstract, which lives in the monads, needs in order no to access global state. - Note that `Proof.t` and `Proof_global.t` are redundant anyways.
2018-12-13Add overlayMaxime Dénès
2018-12-13[dune] [doc] Support for building the reference manual with Dune.Emilio Jesus Gallego Arias
This is a reduced version of #8503 as to provide a way to build the reference manual with Dune. Dune 1.6 supports (experimentally) directories as targets, thus we introduce a rule that will call `sphinx` to build the manual. This only provides build, however generation of `.install` rules is not done, it will be hopefully addressed in #8503. Note that we set `expire: 1 month` for all the artifacts we build with Dune. IMHO this makes most sense as not to abuse Gitlab's hosting, however of course we could consider a different deployment strategy if wanted.
2018-12-13[ci] [appveyor] Temporally disable test suite on Appveyor.Emilio Jesus Gallego Arias
Hopefully we will re-enable it back soon, I am preparing a refactoring that should make it more robust w.r.t paths and changes on Windows which will enable to use a faster build system. But now it is timing out 100% of the times [due to #8655] so it is not useful.
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix ↵Maxime Dénès
comments.
2018-12-12Fix issue #9188 : Enable VST and aactactics in masterMichael Soegtrop
2018-12-11[ci] Clean overlay folder.Emilio Jesus Gallego Arias
2018-12-09fix copy-paste error in CI_ARCHIVEURLChristian Doczkal
2018-12-09add relation-algebra to CI test suiteChristian Doczkal
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :)
2018-12-05[ci] Add four color theorem proof to CIEmilio Jesus Gallego Arias
2018-12-05Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t`Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 02:26:41 +0000