aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-12[dev] Autogenerate OCaml dev files.Emilio Jesus Gallego Arias
For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579
2018-07-12Merge PR #8051: Clean-up user-overlays folder.Emilio Jesus Gallego Arias
2018-07-12Clean-up user-overlays folder.Théo Zimmermann
2018-07-12[warnings] Disable warning 58 "no cmx file was found in path"Emilio Jesus Gallego Arias
See https://github.com/ocaml/num/issues/9
2018-07-12[warnings] Disable warning 59 [assignment to a non-mutable value] to make ↵Emilio Jesus Gallego Arias
flambda happy. See issue #8043. Using `[@@@ocaml.warning "-59"]` to disable this fails, it seems like an OCaml bug.
2018-07-12Fix #7854: Native compilation + flambda trigger SEGFAULT.Pierre-Marie Pédrot
We use a more abstract representation for accumulators in the native compilation scheme, that requires less fiddling with low-level implementation details. It might be slower though.
2018-07-12[ci] Remove warning jobs in favor of default `-warn-error yes`Emilio Jesus Gallego Arias
As discussed in #6930, we remove the warnings jobs and instead do require the developers to submit a clean build.
2018-07-12Cleanup reduction effects: they only work on constants.Gaëtan Gilbert
We only ever call `reduction_effect_hook` on constants, so there's no point allowing it to be declared with globrefs. There is also no point using a constr map instead of constant map. (Technically there was a call of the effect hook on projections, but that can never match a globref so it was useless)
2018-07-12Statically typecheck the VERNAC EXTEND wrapper.Pierre-Marie Pédrot
This moves the typing code from the macro expansion to the extension registering mechanism, bringing in more static safety. We also seize the opportunity to remove dead code in the macro.
2018-07-12Export a wrapper simplifying the registration of vernacular commands.Pierre-Marie Pédrot
2018-07-12Merge PR #7871: [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gaëtan Gilbert
2018-07-12Tactic deprecation machineryMaxime Dénès
We make it possible to deprecate tactics defined by `Ltac`, `Tactic Notation` or ML. For the first two variants, we anticipate the syntax of attributes: `#[deprecated(since = "XX", note = "YY")]` In ML, the syntax is: ``` let reflexivity_depr = let open CWarnings in { since = "8.5"; note = "Use admit instead." } TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END ``` A warning is shown at the point where the tactic is used (either a direct call or when defining another tactic): Tactic `foo` is deprecated since XX. YY YY is typically meant to be "Use bar instead.".
2018-07-11[ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Emilio Jesus Gallego Arias
- We update the OCaml version used in the base CI image. - Windows / OSX image building is also updated to use newer OCaml. - We also update Dune to 1.0.0.
2018-07-11Merge PR #7998: [coqpp] Move to its own directory.Pierre-Marie Pédrot
2018-07-11Merge PR #8035: Fix #8033: Tactic assert-suceeds has a typo in its name in ↵Théo Zimmermann
the manual
2018-07-11Merge PR #8021: Get rid of horrendous hack limiting the size of parsed integersPierre-Marie Pédrot
2018-07-11Merge PR #8002: make-both-single-timing-files: fix --sort-by=diffJason Gross
2018-07-11Merge PR #7898: Remove camlp4 remainsEmilio Jesus Gallego Arias
2018-07-11[coqpp] Move to its own directory.Emilio Jesus Gallego Arias
Coqpp has nothing to do with `grammar`, we thus place it in its own directory, which will prove convenient in more modular build systems. Note that we add `coqpp` to the list of global includes, we could have indeed added some extra rules, but IMHO not worth it as hopefully proper containment will be soon checked by Dune.
2018-07-11Merge PR #7984: Compile `coqpp` inside the `bin/` folder and make it ↵Emilio Jesus Gallego Arias
available after installation
2018-07-11Merge PR #8031: Remove auto-retry in GitLab CI now that @coqbot is handling it.Emilio Jesus Gallego Arias
2018-07-10Export a function to apply toplevel tactic values in Tacinterp.Pierre-Marie Pédrot
This is a function that keeps beeing asked or reimplemented. It doesn't hurt adding it to the Ltac API.
2018-07-10Compile coqpp inside the bin/ folder and make it available after installation.Pierre-Marie Pédrot
2018-07-10Merge PR #8036: [travis] Remove even more jobs.Emilio Jesus Gallego Arias
2018-07-10Merge PR #8034: [travis] Try to workaround the repeated APT failures by ↵Emilio Jesus Gallego Arias
using Jason Gross's suggestion.
2018-07-10[travis] Remove even more jobs.Théo Zimmermann
Users who want to test external projects should be encouraged to activate GitLab CI as is documented in dev/ci/README.md.
2018-07-10fixed typo for assert_suceedcharguer
2018-07-10[travis] Try to workaround the repeated APT failures by using Jason Gross's ↵Théo Zimmermann
suggestion.
2018-07-10Remove auto-retry in GitLab CI now that @coqbot is handling it.Théo Zimmermann
2018-07-10Merge PR #7899: My recent improvements to the backport script.Maxime Dénès
2018-07-10Merge PR #7983: Turn a dead branch into an assertion failure in VM reification.Maxime Dénès
2018-07-10Merge PR #8028: Fix a few typosThéo Zimmermann
2018-07-10Merge PR #8025: Fix rst syntax for `quote ident {ident}`Théo Zimmermann
2018-07-10Add new options --no-conflict and --no-signature-check to backport script.Théo Zimmermann
2018-07-10Fix typo in doc/proof-engine/tactics.rst.whitequark
2018-07-10Fix typo in Init.Logic.whitequark
2018-07-09Merge PR #7920: Generic syntax for attributesMaxime Dénès
2018-07-09Fix rst syntax for `quote ident {ident}`Joachim Breitner
2018-07-09Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Matthieu Sozeau
2018-07-09Introduce a team of code owners for the CI system.Théo Zimmermann
This means that all the members of the team will receive a review request for PRs on the CI, but only one of them will need to approve the PR, and this will remove the review request for the others. Currently the team contains Emilio and Gaetan, the two former code owners of these files. It makes sense to start experimenting on this component since they had already decided to make their role symmetric. Updating the list of maintainers can be done by updating the list members, and without changing the CODEOWNER file.
2018-07-08Merge PR #8015: Output UTF-8 explicitly in timing toolsJason Gross
2018-07-08Get rid of horrendous hack limiting the size of parsed integersMaxime Dénès
2018-07-08Merge PR #7985: Remove letouzey from CODEOWNERS since he left the Coq ↵Maxime Dénès
organization.
2018-07-08Merge PR #8020: Modify URLs in xml-protocol.mdThéo Zimmermann
2018-07-08Modify URLs in xml-protocol.mdRin Arakaki
2018-07-08Modify URLs in xml-protocol.mdRin Arakaki
2018-07-08Merge PR #7843: Remove Emacs modesMaxime Dénès
2018-07-08Mention the removal of Emacs modes in CHANGES.Théo Zimmermann
2018-07-08Remove Emacs modes.Théo Zimmermann
They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead.
2018-07-07make diff sort by difference, not absolute differenceRalf Jung
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-13 20:27:52 +0000