aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Expand)Author
2017-10-25Merge PR #6003: Point HoTT back at master, which now supports Coq masterMaxime Dénès
2017-10-23Point HoTT back at master, which now supports Coq masterJason Gross
2017-10-20Switch testing branch back to CompCert upstream.Théo Zimmermann
2017-10-19rename ci-iris-coq -> ci-iris-lambda-rustRalf Jung
2017-10-19CI: build lambdaRust (which depends on Iris) rather than just IrisRalf Jung
2017-10-10Merge PR #1067: Iris CI: use opam to install dependenciesMaxime Dénès
2017-10-09Merge PR #1117: [ci] Remove temporary bignums overlay.Maxime Dénès
2017-10-04[ci] Remove temporary bignums overlay.Théo Zimmermann
2017-10-03Fix GeoCoq build by using a shared CI configure.Théo Zimmermann
2017-10-03Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META fileMaxime Dénès
2017-09-29start counting at 0...Ralf Jung
2017-09-29Iris CI: use opam to determine std++ git commitRalf Jung
2017-09-20In gitlab set TRAVIS_BRANCH so user overlays will work as expected.Gaëtan Gilbert
2017-09-15Merge PR #979: Fix install-doc target and other gitlab failuresMaxime Dénès
2017-09-13Fix GitLab CIGaëtan Gilbert
2017-09-08Move README.ci and link to it from CONTRIBUTING.Théo Zimmermann
2017-09-07Merge PR #968: Better error messages on the CIMaxime Dénès
2017-09-07Merge PR #914: Making the detyper lazyMaxime Dénès
2017-09-07Trying to properly propagate errors in Windows CI script.Maxime Dénès
2017-09-05Make AppVeyor generate Windows package.Maxime Dénès
2017-09-05Fix Software Foundations build.Maxime Dénès
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-08-24Don't strip the newline, don't use \rJason Gross
2017-08-24Swap order of "aggregating..." message and travis_foldJason Gross
2017-08-24Only display travis_fold: on travisJason Gross
2017-08-15Move the rest of the ci target to a bash fileJason Gross
2017-08-15Better error messages on the CIJason Gross
2017-08-01Have coq-dpdgraph ci test print the differencesJason Gross
2017-07-31Merge PR #746: Timing on ci via coq_makefile for various projectsMaxime Dénès
2017-07-28Merge PR #782: Update API for fiatMaxime Dénès
2017-07-21Alternate way of doing timing on ciJason Gross
2017-07-21Separate make from python script for HoTTJason Gross
2017-07-21Display timing data travis for various projectsJason Gross
2017-07-18[ci] VST is now built with IGNORECOQVERSION=true.Théo Zimmermann
2017-07-11Merge PR #858: [travis] Remove CompCert version check hack.Maxime Dénès
2017-07-05[travis] Remove CompCert version check hack.Emilio Jesus Gallego Arias
2017-07-04Revert fiat-crypto overlayJason Gross
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-20Merge PR#779: Each user overlay goes into its own file.Maxime Dénès
2017-06-16Remove -j ${NJOBS} from make invocations in the ciJason Gross
2017-06-16Fix ci-fiat-crypto to have a proper lite targetJason Gross
2017-06-16Each user overlay goes into its own file.Théo Zimmermann
2017-06-15Merge PR#778: Revert "[travis] temporary UniMath overlay"Maxime Dénès
2017-06-15Update fiat-parsers overlayJason Gross
2017-06-15Remove bedrock from test suite.Maxime Dénès
2017-06-14Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58Maxime Dénès
2017-06-14Temporary overlays because fewer plugins are loaded at startup.Maxime Dénès
2017-06-14[travis] overlay for fiat-crypto (a Require Import FunInd)Pierre Letouzey
2017-06-14[travis] overlays for CompCert and VST (an extra Require Export FunInd)Pierre Letouzey
2017-06-14[travis] fix Software Foundation (one added Require Extraction)Pierre Letouzey