aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
AgeCommit message (Collapse)Author
2018-11-20Merge PR #7925: Clean transparent stateMaxime Dénès
2018-11-19Merge PR #9003: [vernacextend] Consolidate extension points APIPierre-Marie Pédrot
2018-11-19Merge PR #8902: [ltac] Use CAst nodes in the tactic AST.Pierre-Marie Pédrot
2018-11-19Adding overlays.Pierre-Marie Pédrot
2018-11-18Merge PR #9018: [devtools] Small script to setup overlays automaticallyGaëtan Gilbert
2018-11-17[devtools] Small script to setup overlays automaticallyEmilio Jesus Gallego Arias
This is very preliminary but you should get the idea. The script tries to build contribs, then creates a branch and sets the remote properly as to submit a PR. Usage example: ``` ./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi ``` This only works for contributions hosted in github for now.
2018-11-17[vernacextend] Consolidate extension points APIEmilio Jesus Gallego Arias
We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`.
2018-11-17[ci] Uniformize casing of makefile targets and ci variables.Emilio Jesus Gallego Arias
This is convenient as to have better automation.
2018-11-17[ci] Cleanup of old overlays.Emilio Jesus Gallego Arias
2018-11-17[CoqProject] Abstract warning function for CoqProject readers.Emilio Jesus Gallego Arias
`CoqProject_file` uses the feedback system, however this is not very convenient in some scenarios such as `coqdep` that has to be run very early in the build process [and thus in "boot" mode]. We thus make the warning function a paramater. Should fix #8913.
2018-11-17[ltac] Use CAst nodes in the tactic AST.Emilio Jesus Gallego Arias
This provides several advantages to people serializing tactic scripts. Appearance of the involved constructors is common enough as to bother to submit this PR.
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-13Merge PR #8976: CoqHammer CIGaëtan Gilbert
2018-11-13Merge PR #8978: nix helpers for debugging external projects from CIEmilio Jesus Gallego Arias
2018-11-12Skip submodules in HoTT CI script.Gaëtan Gilbert
Avoid downloading Coq.
2018-11-12CoqHammer CILukasz Czajka
2018-11-12Helpers for debugging external projects from CIVincent Laporte
2018-11-10[ci] Add paramcoq to CI.Emilio Jesus Gallego Arias
2018-11-09Adding an overlay for #8601.Pierre-Marie Pédrot
2018-11-08Revert "Merge PR #8923: Bump camlp5 minimal version and use its safe API."Pierre-Marie Pédrot
This reverts commit c4880effb91fab55c250a799cbceac9b04681db0, reversing changes made to 65927c22bcad62e1bc9a28a57377d82eba215a2d.
2018-11-07Bump up the minimal camlp5 version to 7.06.Pierre-Marie Pédrot
This is the first release that contains the type-safe grammar API.
2018-11-07Merge PR #8868: [Docker] Update OCaml (4.07.1) and camlp5 (7.07-almost)Emilio Jesus Gallego Arias
2018-11-06[Docker] Update COMPILER_EDGE: 4.07.0 → 4.07.1Vincent Laporte
Also update CAMLP5_VER_EDGE: 7.06 → 7.06.10-g84ce6cc4 This is to avoid an OCaml bug that occurs when compiling the OCaml code extracted from part of a patched version of CompCert. ~~~ File "extraction/Parser.ml", line 12375, characters 19-29: Error: Constraints are not satisfied in this type. Type initstate' should be an instance of initstate' ~~~ This compiler issue only appears with OCaml 4.07.0 (neither with 4.06 nor with 4.07.1); hence this update.
2018-11-06Add overlay for EquationsMatthieu Sozeau
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-03Merge PR #8844: Move abstract out of tactics.mlPierre-Marie Pédrot
2018-11-02Add overlays (command driven attributes)Gaëtan Gilbert
2018-10-31Merge PR #8688: Generalizing the various evar_map printers in Termops over ↵Pierre-Marie Pédrot
an environment
2018-10-30Merge PR #8750: [ci] [doc] Notes about branch names.Gaëtan Gilbert
2018-10-30Overlays (#8844 split-tactics)Gaëtan Gilbert
2018-10-30Adding overlay for coq-elpiHugo Herbelin
2018-10-28Merge PR #8827: Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet ↵Emilio Jesus Gallego Arias
merged commit."
2018-10-26Fix overlay for this extension of the PR. To be removed.Matthieu Sozeau
2018-10-26PR 8671: Add overlay for plugin-tutorialMatthieu Sozeau
2018-10-26Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit."Gaëtan Gilbert
This reverts commit df69c44af03f2587b3f1706a805d0e2728c1f1dc. Should be merged before any PR with plugin tutorial overlays, or we can just merge the vendor PR instead.
2018-10-26Overlay for kernel entries changeMaxime Dénès
2018-10-23[dune] [opam] Move to OPAM 2.0Emilio Jesus Gallego Arias
We need to update in Docker: - dune to 1.4.0: as it honors `-p` on test stanzas - dune-release to 1.1.0: support for OPAM 2.0 + fixes This makes `dune-release distrib` / `dune-release opam pkg` work. TODO: we need to figure out what is going on with the versioning. Should we do `dune subst` on `pinned`?
2018-10-22[doc] [api] Update `odoc` to new release 1.3.0Emilio Jesus Gallego Arias
This includes many changes, please have a look at the newly generated docs.
2018-10-18Merge PR #8719: [ci] [appveyor] Disable validate target.Maxime Dénès
2018-10-18[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit.Théo Zimmermann
This fixes the CI until this commit is merged into master.
2018-10-17[ci] [doc] Notes about branch names.Emilio Jesus Gallego Arias
I'd like to add this convention as it is very convenient for the development of dev tools. Example, I can do `setup-coq-devs ltac equations` and then get a fully composed tree. Similarly for preparing overlays.
2018-10-15Merge PR #8704: [vernac] Remove unused abstraction from declaration_hook type.Hugo Herbelin
2018-10-14[ci] [sf] Remove sed hacks from the SF build.Emilio Jesus Gallego Arias
Fixes #8337
2018-10-12[ci] [appveyor] Disable validate target.Emilio Jesus Gallego Arias
Not a big point on running the checker on Appveyor I think, this will save a bunch of time and improve reliability.
2018-10-11[vernac] Remove unused abstraction from declaration_hook type.Emilio Jesus Gallego Arias
"Declaration" hooks can be polymorphic on their return type, however this facility doesn't seem used in the codebase. We thus remove the polymorphism with the hope to be able to reify the control later on.
2018-10-08[ci] Add aac-tactics.Théo Zimmermann
And fix a typo that was previously there.
2018-10-08Merge PR #8660: Issue 8659 not always build all addonsThéo Zimmermann
2018-10-08Merge PR #8554: Fixes #8553: regression of tactic "change" under binders.Pierre-Marie Pédrot
2018-10-06Merge PR #8555: Remove section paths from kernel namesPierre-Marie Pédrot
2018-10-05Merge PR #8645: Improve markdown in changes.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:44:18 +0000