aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: gares Ack-by: herbelin Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
Ack-by: ejgallego Ack-by: maximedenes Reviewed-by: ppedrot
2019-05-14Overlay for value-returning run_tacticGaëtan Gilbert
2019-05-13Adding overlay for Equations.Hugo Herbelin
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to ↵Enrico Tassi
prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl
2019-05-13Add overlay for UnicoqMaxime Dénès
2019-05-11Merge PR #10052: Cleanup the hypothesis conversion functionHugo Herbelin
Reviewed-by: herbelin
2019-05-10Add overlay for elpiVincent Laporte
2019-05-10Merge PR #9854: Improve field_simplify on fractions with constant denominatorMichael Soegtrop
Reviewed-by: MSoegtropIMC Ack-by: Zimmi48 Reviewed-by: amahboubi Reviewed-by: vbgl
2019-05-10Add overlays for coq/coq#10052.Pierre-Marie Pédrot
2019-05-10Merge PR #10120: Clean-up: remove dead appveyor.sh file.Emilio Jesus Gallego Arias
2019-05-09Merge PR #10081: Remove ppedrot/ltac2 from CI after integration in main repoMichael Soegtrop
Reviewed-by: MSoegtropIMC
2019-05-09Switched Coquelicot CI URLs from INRIA gforge to INRIA gitlabMichael Soegtrop
2019-05-08Remove ltac2 add-on from Windows installer now that it is in the main Coq ↵Théo Zimmermann
package.
2019-05-08Clean-up: remove dead appveyor.sh file.Théo Zimmermann
2019-05-07Remove overlays for CompCert and VSTVincent Laporte
2019-05-07[nix-ci] Add coquelicot, improve flocqVincent Laporte
2019-05-07Add overlays for CompCert, VST, and coquelicotVincent Laporte
2019-05-07Remove ppedrot/ltac2 from CI after integration in main repoGaëtan Gilbert
2019-05-07Add overlays.Pierre-Marie Pédrot
2019-04-24[coq_makefile] Enforce warn_error for plugins.Emilio Jesus Gallego Arias
The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974
2019-04-20overlay for elpiEnrico Tassi
2019-04-20update elpi to version 1.2Enrico Tassi
2019-04-16[ci] Overlays for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-10Overlays for Global removal in pretyperMaxime Dénès
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin Ack-by: ppedrot Ack-by: proux01
2019-04-04[CI] Fix build of math-comp dependenciesMaxime Dénès
We were incorrectly calling the global `install` target even when building only subcomponents of the library.
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ppedrot
2019-04-02Add overlaysPierre Roux
2019-04-01[CI] Disable Coquelicot on WindowsVincent Laporte
2019-04-01[CI] Coquelicot: use “master” development versionVincent Laporte
2019-04-01Merge PR #9870: Minor refactoring in canonical structuresEnrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2019-04-01Merge PR #9815: Multiple payload types in tokensPierre-Marie Pédrot
Reviewed-by: ppedrot Ack-by: proux01
2019-04-01Merge PR #9871: CI: add mit-pdos/argosyEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-01Merge PR #9872: Fix timing diff script to support non-utf8Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: jashug
2019-03-31Add overlayPierre Roux
2019-03-31Merge PR #9733: [lexer] keyword protected quotation token for arbitrary textPierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-03-31Revert "iconv bedrock2 CI output to UTF-8"Jason Gross
This reverts commit 1eb8b9dc3ff0e464c9cd6c7f12a1c9db4fa57423. This commit is no longer necessary
2019-03-31CI: add mit-pdos/argosyTej Chajed
2019-03-31overlay for ltac2Enrico Tassi
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
(warn if bar is a nonprimitive projection)
2019-03-30Overlay for ElpiVincent Laporte
2019-03-28Use only lowercase for unimath in CI scriptsGaëtan Gilbert
Fix #9845
2019-03-27[proof_global] [ci] Overlays for removal of imperative state.Emilio Jesus Gallego Arias
2019-03-26Overlays for HoTT, Ltac2, and UniMathVincent Laporte
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ↵Maxime Dénès
proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-03-20Add overlays for printer API changesMaxime Dénès
2019-03-19Merge PR #9647: [default.nix] Enable parallel buildThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-03-19[coqide] [ci] Update GTK toolchain to lablgtk3Emilio Jesus Gallego Arias
- Update Docker images to install compatible version of lablgtk3 - We remove unnecesary variables from configure. - We fix path detection of GTK libs in makefile