| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-11 | Windows packaging build with Gitlab CI | Maxime Dénès | |
| We use a specific runner on Inria CloudStack. This allows us to have the same build infrastructure setup for signed and unsigned binary packages. The main Coq repository on Gitlab will produce unsigned binaries, using a runner without secret. On my repository, a one-click operation will sign the packages, making this part of the release process smoother. | |||
| 2018-05-10 | Merge PR #7437: [coqdep] Minor cleanups. | Pierre-Marie Pédrot | |
| 2018-05-10 | Merge PR #7473: [ci] Add mit-plv/cross-crypto | Emilio Jesus Gallego Arias | |
| 2018-05-10 | Merge PR #7471: [travis] Fix version of camlp5 for OCaml 4.06.1. | Emilio Jesus Gallego Arias | |
| 2018-05-09 | [ci] Add mit-plv/cross-crypto | Jason Gross | |
| I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything. | |||
| 2018-05-09 | [travis] Add explicit opam switch command to guarantee we're using the ↵ | Théo Zimmermann | |
| requested compiler. | |||
| 2018-05-09 | [travis] Fix version of camlp5 for OCaml 4.06.1. | Théo Zimmermann | |
| 2018-05-09 | Merge PR #7438: [gitlab] Do expensive builds with the flambda compiled Coq. | Gaëtan Gilbert | |
| 2018-05-09 | Merge PR #7435: [gitlab] Add bleeding-edge flambda build. | Gaëtan Gilbert | |
| 2018-05-08 | Merge PR #7459: Try to fix CODEOWNERS | Théo Zimmermann | |
| 2018-05-08 | Merge PR #7446: [lib] Re-add `set_timeout` to help users workaround #7408 | Pierre-Marie Pédrot | |
| 2018-05-08 | Try to fix CODEOWNERS | Maxime Dénès | |
| 2018-05-08 | [gitlab] Do expensive builds with a flambda-compiled Coq. | Emilio Jesus Gallego Arias | |
| Gains seem superior to 50%, but data is taken from Gitlab so no reliable at all. | |||
| 2018-05-08 | [CoqProject] Add some comments and remove unnecessary use of Pp. | Emilio Jesus Gallego Arias | |
| But indeed we need to split this file, as it is used now from CoqIDE is incorrect. | |||
| 2018-05-08 | [coqdep] Remove unnecessary dependency on Pp and CError. | Emilio Jesus Gallego Arias | |
| This allows for even earlier bootstrapping. | |||
| 2018-05-08 | [coqdep] Minor cleanups. | Emilio Jesus Gallego Arias | |
| - Remove inclusion of the `tactics` directory, this is coming from a time loadable modules were found there, now all are under `plugins`. - Remove 2 dependencies so we can bootstrap coqdep earlier. - Use `Format` instead of `Printf` for printing. | |||
| 2018-05-07 | [gitlab] Add bleeding-edge flambda build. | Emilio Jesus Gallego Arias | |
| We also introduce a bit more systematic job naming: `base/edge`. In order to make the flambda switch selectable we update the Docker image so all the dependencies are installed in that one. Note the extra quote rule for the flambda parameters, but unless we can assign arrays to Gitlab variables there is not a good way to do this I'm afraid. With this patch we are getting close to being able to remove most builds from Travis. | |||
| 2018-05-07 | [lib] Re-add `set_timeout` to help users workaround #7408 | Emilio Jesus Gallego Arias | |
| It seems like #7408 will need some potentially intrusive work, so let's add the low-level hook back so third party developments can work well with `8.8.1/master` for the moment. | |||
| 2018-05-07 | Merge PR #7347: Fix for #7081 (Windows lablgtk) and #7083 (Windows logging) | Maxime Dénès | |
| 2018-05-07 | Merge PR #7371: Propose some updates of the CODEOWNER file. | Maxime Dénès | |
| 2018-05-07 | Merge PR #7445: [ci] Add ounit to the base Docker package set. | Gaëtan Gilbert | |
| 2018-05-07 | Merge PR #7301: [sphinx] Backport forgotten updates during the migration & ↵ | Maxime Dénès | |
| other improvements | |||
| 2018-05-07 | Merge PR #7440: [ci] Add a default target to `Makefile.ci` | Gaëtan Gilbert | |
| 2018-05-07 | [ci] Add ounit to the base Docker package set. | Emilio Jesus Gallego Arias | |
| This should help #6808. | |||
| 2018-05-07 | Merge PR #7427: Fix #7413: coqdep warning on repeated files | Pierre-Marie Pédrot | |
| 2018-05-06 | Merge PR #7387: [gitlab] [circleci] Use a Docker base image for CI | Gaëtan Gilbert | |
| 2018-05-06 | Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow ↵ | Maxime Dénès | |
| kernel style. | |||
| 2018-05-06 | [ci] Add a default target to `Makefile.ci` | Emilio Jesus Gallego Arias | |
| So we avoid problems like the one in #7438. | |||
| 2018-05-05 | [gitlab] [circleci] Use a Custom Docker Image as base CI setup. | Emilio Jesus Gallego Arias | |
| We provide a custom `Dockerfile` for Coq's CI system, based on `ubuntu:bionic`. The image includes the required set of packages and OPAM switches. This greatly simplifies the Gitlab and Circle scripts, at the cost of having to push a Docker build for them to depend on. Travis is not included in this PR as it requires significant more refactoring due to lack of native Docker support. This is work in progress but ready, a build hook is used so the image is properly tagged in the Docker autobuilder. We need to improve the autobuilder setup but this last point requires some design on how to trigger it. Fixes #7383 | |||
| 2018-05-05 | [sphinx] Fixes around apply, including indentation and fixing a Coq warning. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Fixes around refine, including indentation and a hard-coded ref. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Improve typeclass chapter. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Add indices for only, all and par. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Improvements around injection tactic. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Improve part about Hints. | Théo Zimmermann | |
| Fix Hint (Transparent | Opaque) index. | |||
| 2018-05-05 | [sphinx] Re-indent to get much better rendering. | Théo Zimmermann | |
| Add some more cmd references. And use deprecated directives. | |||
| 2018-05-05 | Remove duplicate Introduction title. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Backport changes from #5979. | Théo Zimmermann | |
| 2018-05-05 | Two more uses of verbatim in doc. | Théo Zimmermann | |
| 2018-05-05 | Clean-up around cmd documentation. | Théo Zimmermann | |
| In particular, remove trailing dots. | |||
| 2018-05-05 | Remove duplicate Extraction commands documentation. | Théo Zimmermann | |
| 2018-05-05 | Add some refs in the Omega chapter. | Théo Zimmermann | |
| 2018-05-05 | More fixes in the Generalized Rewriting chapter. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Replace remaining `@natural` by `@num`. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] More use of cmd references in Extraction chapter. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Use references for command Info. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] More reference fixes. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Fix a porting mistake. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Use references for Print. | Théo Zimmermann | |
| 2018-05-05 | Fix error messages and make them consistent. | Théo Zimmermann | |
| All the error messages start with a capitalized letter and end with a dot. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |