| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-13 | [dune] [doc] Support for building the reference manual with Dune. | Emilio Jesus Gallego Arias | |
| This is a reduced version of #8503 as to provide a way to build the reference manual with Dune. Dune 1.6 supports (experimentally) directories as targets, thus we introduce a rule that will call `sphinx` to build the manual. This only provides build, however generation of `.install` rules is not done, it will be hopefully addressed in #8503. Note that we set `expire: 1 month` for all the artifacts we build with Dune. IMHO this makes most sense as not to abuse Gitlab's hosting, however of course we could consider a different deployment strategy if wanted. | |||
| 2018-12-13 | [ci] [appveyor] Temporally disable test suite on Appveyor. | Emilio Jesus Gallego Arias | |
| Hopefully we will re-enable it back soon, I am preparing a refactoring that should make it more robust w.r.t paths and changes on Windows which will enable to use a faster build system. But now it is timing out 100% of the times [due to #8655] so it is not useful. | |||
| 2018-12-12 | Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix ↵ | Maxime Dénès | |
| comments. | |||
| 2018-12-09 | fix copy-paste error in CI_ARCHIVEURL | Christian Doczkal | |
| 2018-12-09 | add relation-algebra to CI test suite | Christian Doczkal | |
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-12-05 | [ci] Add four color theorem proof to CI | Emilio Jesus Gallego Arias | |
| 2018-12-05 | Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Pierre-Marie Pédrot | |
| 2018-12-05 | Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks. | Pierre-Marie Pédrot | |
| 2018-12-04 | CI: track dev branch of coq-simple-io | Yishuai Li | |
| 2018-11-30 | [vernac] [hooks] Refactor towards optional hooks. | Emilio Jesus Gallego Arias | |
| We make `declaration_hook`s optional arguments everywhere, and thus we avoid some "fake" functions having to be passed. This identifies positively the code really using hooks [funind, rewrite, coercions, program, and canonicals] and helps moving toward some hope of reification. | |||
| 2018-11-30 | [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Emilio Jesus Gallego Arias | |
| The types are identical and we have no more reason for the split. Note the following TODOS: - discrepancy of `Ploc.after` with `CLexer.after` - discrepancy of `Ploc.comments` with `CLexer.comments` - `Ploc.dummy` vs `Loc.t option` | |||
| 2018-11-30 | Merge PR #9102: [ltac] Remove aliases already present in the lower layers. | Pierre-Marie Pédrot | |
| 2018-11-29 | Merge PR #9054: [ci] [appveyor] Move Appveyor to OPAM 2. | Maxime Dénès | |
| 2018-11-28 | [Windows CI] Do not build any addon if WINDOWS is not enabled_all_addons. | Théo Zimmermann | |
| Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com> | |||
| 2018-11-28 | [ltac] Remove aliases already present in the lower layers. | Emilio Jesus Gallego Arias | |
| We remove a few aliases present in the lower layers [`Genintern/Tactypes`] from `Tacexpr`. IMHO this enlarges the API for no good purpose, and difficults analysis. | |||
| 2018-11-27 | [ci] [appveyor] Move Appveyor to OPAM 2. | Emilio Jesus Gallego Arias | |
| We update the Appveyor configuration so it uses OPAM 2.0, and thus it can install newer packages. | |||
| 2018-11-27 | Merge PR #8850: Private universes for opaque polymorphic constants. | Matthieu Sozeau | |
| 2018-11-26 | [nix-ci] Add a README in dev/ci/nix | Vincent Laporte | |
| 2018-11-26 | [nix-ci] Use master version of Unicoq | Vincent Laporte | |
| 2018-11-24 | Merge PR #8933: Make initial evar map argument to check_evars_are_solved ↵ | Pierre-Marie Pédrot | |
| optional. | |||
| 2018-11-24 | Apply suggestions from code review | Théo Zimmermann | |
| Thanks to @Zimmi48 as always for the careful review. Co-Authored-By: ejgallego <e+git@x80.org> | |||
| 2018-11-24 | [ci] [doc] Note about `overlay-maintainers` team. | Emilio Jesus Gallego Arias | |
| 2018-11-24 | [ci] [doc] Note about `create-overlays.sh` | Emilio Jesus Gallego Arias | |
| 2018-11-24 | [ci] [doc] Split user/developer README, add info about Nix/Docker CI | Emilio Jesus Gallego Arias | |
| 2018-11-23 | Merge PR #9044: Remove pidetop from CI | Emilio Jesus Gallego Arias | |
| 2018-11-23 | Adding overlay. | Pierre-Marie Pédrot | |
| 2018-11-23 | Overlay for private polymorphic universes | Gaëtan Gilbert | |
| 2018-11-21 | Remove pidetop from CI | Maxime Dénès | |
| pidetop relies on some rather low level API from STM, which we'd like to change. It does not seem maintained much anymore, and still hasn't moved to github. | |||
| 2018-11-21 | [camlp5] Remove dependency on camlp5. | Emilio Jesus Gallego Arias | |
| 2018-11-21 | Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlib | Enrico Tassi | |
| 2018-11-21 | Add overlay for solve-remaining-evars-initial-arg | Gaëtan Gilbert | |
| 2018-11-21 | [legacy proof engine] Remove some cruft. | Emilio Jesus Gallego Arias | |
| We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps. | |||
| 2018-11-21 | [gramlib] [build] Switch make-based system to packed gramlib | Emilio Jesus Gallego Arias | |
| This makes the make-based build system stop linking to Camlp5's gramlib and instead links to our own gramlib. We use the style done in the packing of `Stdlib` in OCaml 4.07. As to introduce a minimal amount of noise in history we use an autogenerated `gramlib__pack` directory. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2018-11-20 | gitlab: Install stdlib doc in build:base | Gaëtan Gilbert | |
| Looks like we forgot to adapt this when we split off the sphinx job and stopped using -with-doc yes. | |||
| 2018-11-20 | Merge PR #7925: Clean transparent state | Maxime Dénès | |
| 2018-11-19 | Merge PR #9003: [vernacextend] Consolidate extension points API | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8902: [ltac] Use CAst nodes in the tactic AST. | Pierre-Marie Pédrot | |
| 2018-11-19 | Adding overlays. | Pierre-Marie Pédrot | |
| 2018-11-18 | Merge PR #9018: [devtools] Small script to setup overlays automatically | Gaëtan Gilbert | |
| 2018-11-17 | [devtools] Small script to setup overlays automatically | Emilio 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 API | Emilio 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-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-13 | Merge PR #8976: CoqHammer CI | Gaëtan Gilbert | |
| 2018-11-13 | Merge PR #8978: nix helpers for debugging external projects from CI | Emilio Jesus Gallego Arias | |
| 2018-11-12 | Skip submodules in HoTT CI script. | Gaëtan Gilbert | |
| Avoid downloading Coq. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |