aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2018-07-03Add overlay for equations.Gaëtan Gilbert
2018-07-02[ci] [docker] Make sure we don't install optional packages with apt.Emilio Jesus Gallego Arias
This should help towards ensuring that the system only has the packages we specify in the Dockerfile. We were missing: - `git`: used in the CI system itself! - `rsync`: used in the test-suite - `python3-setuptools`, `python3-wheel`: necessary to use pip3 properly to install the missing python package. - `autoconf`, `automake`: a few CI contribs depend on them.
2018-07-02Add Equations overlayMatthieu Sozeau
2018-07-02Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Emilio Jesus Gallego Arias
points of Camlp5
2018-06-29Adding an overlay for the PR.Pierre-Marie Pédrot
2018-06-29Document that GITURL variables shouldn't have a trailing .git anymore.Théo Zimmermann
This allows to append /archive at the end.
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Maxime Dénès
constr in Constr
2018-06-27Add mit-plv/bedrock2-ci to CIAndres Erbsen
2018-06-27Adding overlay.Hugo Herbelin
2018-06-27Merge PR #7863: Remove Sorts.contentsPierre-Marie Pédrot
2018-06-26Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵Pierre-Marie Pédrot
constants
2018-06-26Add overlay for elpiGaëtan Gilbert
2018-06-26Add overlay for Equations, ElpiGaëtan Gilbert
2018-06-25Activate the build of Ltac2 and Equations in the Windows installer.Théo Zimmermann
2018-06-25Reuse CI info to know which version of plugins to build on Windows.Théo Zimmermann
2018-06-24Merge PR #7895: Revert "Add a note about [ci skip] in CI README."Emilio Jesus Gallego Arias
2018-06-22Revert "Add a note about [ci skip] in CI README."Théo Zimmermann
This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
2018-06-21Update dpdgraph branch nameGaëtan Gilbert
See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
2018-06-19Merge PR #7797: Remove reference name type.Enrico Tassi
2018-06-18Overlay for reference removalMaxime Dénès
2018-06-18Update section on adding your project to CI and link to example PR.Théo Zimmermann
2018-06-14Merge PR #7793: [ci] update docker image to include elpi 1.0.4Emilio Jesus Gallego Arias
2018-06-14Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵Matthieu Sozeau
to anomaly)
2018-06-13[ci] update docker image to include elpi 1.0.4Enrico Tassi
2018-06-13Markdown docs: switch from absolute to relative links.Théo Zimmermann
We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip]
2018-06-12[api] Add compatiblity Misctypes module.Emilio Jesus Gallego Arias
To be removed in 8.10.
2018-06-11[ci] GeoCoq now depends on math-comp's ssralg.Emilio Jesus Gallego Arias
2018-06-08Merge PR #7687: [ci] [docker] Pin specific versions of OPAM CI dependencies.Gaëtan Gilbert
2018-06-06[ci] [docker] Pin specific versions of OPAM CI dependencies.Emilio Jesus Gallego Arias
Packages such as `menhir` or `elpi` are fragile w.r.t. updates, so allowing a non-deterministic install in the Dockefile seems risky. We have found trouble with Menhir in the past. We thus specify a concrete version for all `CI_OPAM` packages. cc: https://github.com/AbsInt/CompCert/issues/234 We also add remove `hevea` from `apt` dependencies as it hasn't been needed since #7466 and add `texlive-science` which is needed to build the `source-doc` target due to the `textgreek` package being used.
2018-06-06Add a note about [ci skip] in CI README.Théo Zimmermann
2018-06-06Merge PR #7717: [ci] Temporal fix for CompCertGaëtan Gilbert
2018-06-06[ci] Temporal fix for CompCertEmilio Jesus Gallego Arias
https://github.com/AbsInt/CompCert/issues/234
2018-06-05Merge PR #7099: Stronger invariants in unification signature.Matthieu Sozeau
2018-06-05Merge PR #7495: Fix restrict_universe_contextMatthieu Sozeau
2018-06-04Merge PR #7596: [ci] [windows] Use newer OCaml version.Michael Soegtrop
2018-06-04Adding an overlay for the Equations plugin.Pierre-Marie Pédrot
2018-06-02QuickChick CILeonidas Lampropoulos
2018-06-02[ci] Expose updated `OCAMLPATH` for CI users.Emilio Jesus Gallego Arias
This is needed for CI packages that use `META.coq` such as in https://github.com/coq/coq/pull/7656 .
2018-06-02[appveyor] Use OCaml version 4.06.1 in the Windows build.Emilio Jesus Gallego Arias
We bump Windows builds to 4.06.1, IMHO it makes sense to use the latest OCaml version to build on that platform due to the support status and number of fixes.
2018-05-30overlay triggering bug #7472 (that #7495) is supposed to fixEnrico Tassi
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
We make the vernacular implementation self-contained in the `vernac/` directory. To this extent we relocate the parser, printer, and AST to the `vernac/` directory, and move a couple of hint-related types to `Hints`, where they do indeed belong. IMO this makes the code easier to understand, and provides a better modularity of the codebase as now all things under `tactics` have 0 knowledge about vernaculars. The vernacular extension machinery has also been moved to `vernac/`, this will help when #6171 [proof state cleanup] is completed along with a stronger typing for vernacular interpretation that can distinguish different types of effects vernacular commands can perform. This PR introduces some very minor source-level incompatibilities due to a different module layering [thus deprecating is not possible]. Impact should be relatively minor.
2018-05-26Merge PR #7543: [ide] Move common protocol library to its own folder/object.Pierre-Marie Pédrot
2018-05-25Use -j 1 for high memory fiat crypto targetsGaëtan Gilbert
2018-05-24[tactics] Remove anonymous fix/cofix form.Emilio Jesus Gallego Arias
We remove the `fix N / cofix N` forms from the tactic language. This way, these tactics don't depend anymore on the proof context, in particular on the proof name, which seems like a fragile practice. Apart from the concerns wrt maintenability of proof scripts, this also helps making the "proof state" functional; as we don't have to propagate the proof name to the tactic layer.
2018-05-24Complete rewrite of the documentation of overlays after Jim's additional ↵Théo Zimmermann
comments. [ci skip]
2018-05-24Relax advice on the name of user-overlays following Gaëtan's suggestion.Théo Zimmermann
[ci skip]
2018-05-24Improve merging and overlay documentations.Théo Zimmermann
Clarification prompted by Jim Fehrle. [ci skip]
2018-05-24[ide] Move common protocol library to its own folder/object.Emilio Jesus Gallego Arias
The `ide` folder contains two different binaries, the language server `coqidetop` and `coqide` itself. Even if these binaries are in the same folder, the only thing they have in common is that they link to the protocol files. In the OCaml world, having "doubly" linked files in the same project is considered a bit of an ugly practice, and some build tools such as Dune disallow it.q Thus, to clean up the build, we move the common protocol files to its own library `ideprotocol`. This helps towards Dune integration and towards having an IDE standalone target, such as the one that was implemented here: https://github.com/ejgallego/coqide-exp
2018-05-22[ci] Build fiat-crypto targets in sequenceJason Gross
This should hopefully alleviate memory problems on gitlab, by first building the `lite` targets, and then building the remaining not-that-big targets.
2018-05-22Merge PR #7526: [circle] Use Docker image from Gitlab registry.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 16:19:06 +0000