| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-13 | Merge PR #7489: gitlab CI: remove math-classes job | Emilio Jesus Gallego Arias | |
| 2018-05-11 | gitlab CI: remove math-classes job | Gaëtan Gilbert | |
| It's redundant as a dependency of formal-topology. | |||
| 2018-05-11 | Merge PR #7340: Remove DirClosedSection. | Enrico Tassi | |
| 2018-05-11 | Merge PR #7470: use at least 6 Xs in mktemp filename templates | Gaëtan Gilbert | |
| 2018-05-11 | Merge PR #6959: [build] Build checker generated files using a make rule. | Enrico Tassi | |
| 2018-05-11 | Merge PR #7466: Remove tutorials from the repo | Maxime Dénès | |
| 2018-05-11 | Merge PR #7461: [sphinx] Improve the proof handling chapter. | Maxime Dénès | |
| 2018-05-11 | Merge PR #7341: Don't recurse into closed modules/sections in split_lib. | Enrico Tassi | |
| 2018-05-11 | Merge PR #7363: [ci] Fix another issue with the timing tests | Gaëtan Gilbert | |
| 2018-05-11 | Merge PR #7456: [toplevel] Don't ignore output filename provided by user in -o | Théo Zimmermann | |
| 2018-05-10 | Merge PR #7437: [coqdep] Minor cleanups. | Pierre-Marie Pédrot | |
| 2018-05-10 | Suggest going to /documentation to see a list of tutorials. | Théo Zimmermann | |
| 2018-05-10 | One can build all the HTML doc using default.nix. | Théo Zimmermann | |
| 2018-05-10 | Clean-up in Makefile.doc and include Sphinx in doc-html target. | Théo Zimmermann | |
| 2018-05-10 | Remove tutorials. | Théo Zimmermann | |
| 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-10 | [build] Build checker generated files using a make rule. | Emilio Jesus Gallego Arias | |
| Currently, `configure.ml` does copy/link some files from `kernel` to `checker` in an ad-hoc way. Instead, it is preferable to add a copy rule to make and let it handle the dependencies properly. This also fixes a dependency bug in Windows, as files wouldn't be properly refreshed if `configure` was not run each time. | |||
| 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 | [sphinx] Improve proof handling chapter. | Théo Zimmermann | |
| 2018-05-09 | Clarify that the description of coqtop does not reflect all user interfaces. | Théo Zimmermann | |
| 2018-05-09 | [sphinx] Improvements around the Show commands, including missing indices ↵ | Théo Zimmermann | |
| and indentation. | |||
| 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 | use at least 6 Xs in mktemp filename templates | Sven M. Hallberg | |
| OpenBSD mktemp fails with an error otherwise. | |||
| 2018-05-09 | test for coqc -o | Enrico Tassi | |
| 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-08 | [toplevel] Don't ignore output filename provided by user in -o | Emilio Jesus Gallego Arias | |
| This was a silly bug introduced in 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 that forgot to properly forward the command line option. Thanks to @SkySkimmer for finding out the problem. closes #7447 | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |