aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
...
| | * | | Document Smart/Array changes in dev/doc/Changes.md.Gravatar Hugo Herbelin2018-05-23
| |/ / / |/| | |
| * | | [ci] Build fiat-crypto targets in sequenceGravatar Jason Gross2018-05-22
| | | | | | | | | | | | | | | | | | | | | | | | This should hopefully alleviate memory problems on gitlab, by first building the `lite` targets, and then building the remaining not-that-big targets.
* | | | Merge PR #7577: Fixing debugger after #6859 (loading dynlink.cma before ↵Gravatar Emilio Jesus Gallego Arias2018-05-22
|\ \ \ \ | |/ / / |/| | | | | | | lib.cma).
| * | | Fixing debugger after #6859 (loading dynlink.cma before lib.cma).Gravatar Hugo Herbelin2018-05-22
| | | |
* | | | Merge PR #7384: Split UniversesGravatar Pierre-Marie Pédrot2018-05-22
|\ \ \ \ | |/ / / |/| | |
* | | | Merge PR #7324: Infrastructure for ocamldebug on the checkerGravatar Hugo Herbelin2018-05-22
|\ \ \ \
* \ \ \ \ Merge PR #7526: [circle] Use Docker image from Gitlab registry.Gravatar Gaëtan Gilbert2018-05-22
|\ \ \ \ \
* | | | | | [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
* | | | | | Merge PR #7527: [windows] Don't build menhir and int anymore in the ↵Gravatar Michael Soegtrop2018-05-19
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | packaging scripts.
* \ \ \ \ \ \ Merge PR #7550: [CI] Fix the script used by math-classes.Gravatar Emilio Jesus Gallego Arias2018-05-18
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6965: [api] Move universe syntax to `Glob_term`Gravatar Pierre-Marie Pédrot2018-05-18
|\ \ \ \ \ \ \ \
| | | | | | | * | Create a documentation for the release manager.Gravatar Théo Zimmermann2018-05-18
| |_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This process is expected to evolve in the future as we automate it more and more. [ci skip]
| | * | | | | | [CI] Fix the script used by math-classes.Gravatar Pierre-Marie Pédrot2018-05-18
| |/ / / / / / |/| | | | | | | | | | | | | | | | | | | | We call configure to properly regenerate the Makefile and its dependencies.
| | | | | * | Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
| | | | | | |
| | | | | * | Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | This API is a bit strange, I expect it will change at some point.
| | | * | | [circle] Use Docker image from Gitlab registry.Gravatar Emilio Jesus Gallego Arias2018-05-17
| |_|/ / / |/| | | |
* | | | | Merge PR #7525: [ci] Try to build more of fiat-crypto.Gravatar Gaëtan Gilbert2018-05-17
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6808: Add unit tests to test-suiteGravatar Gaëtan Gilbert2018-05-17
|\ \ \ \ \ \
| | * | | | | [ci] Try to build more of fiat-crypto.Gravatar Emilio Jesus Gallego Arias2018-05-16
| |/ / / / / |/| | | | |
* | | | | | Merge PR #7514: [ci] Don't build lite versions of CI developments.Gravatar Gaëtan Gilbert2018-05-16
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7391: Add a small documentation writer's guideGravatar Maxime Dénès2018-05-16
|\ \ \ \ \ \ \
| | | | | * | | [windows] Don't make menhir and int anymore.Gravatar Emilio Jesus Gallego Arias2018-05-16
| |_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As pointed out by @MSoegtropIMC [here](https://github.com/coq/coq/pull/7522#issuecomment-389478963) there are not needed to build the packages, so not building them will save a couple of minutes.
| | | * | | | add unit tests to test suiteGravatar Paul Steckler2018-05-16
| |_|/ / / / |/| | | | |
* | | | | | Merge PR #7442: Gitlab: build docker image in pipeline and use through registry.Gravatar Emilio Jesus Gallego Arias2018-05-16
|\ \ \ \ \ \
| | | * | | | [ci] Don't build lite versions of CI developments.Gravatar Emilio Jesus Gallego Arias2018-05-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In the original Travis CI setup, the per-job time limit was an issue. However, Gitlab has much improved this problem due to a) Coq not being built for each contrib, b) user-configurable time limit. We thus disable the expensive builds from Travis: `fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`, `math-comp`, `unimath`, `vst` and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`] in full. We also update the `math-comp` script as the `odd-order` theorem lives in a separate repository and it is a key CI case.
* | | | | | | Merge PR #7505: Pick up user overlays when running GitLab CI on PRs.Gravatar Emilio Jesus Gallego Arias2018-05-16
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7519: git / gpg integration linkGravatar Théo Zimmermann2018-05-15
|\ \ \ \ \ \ \ \
| | | | * | | | | [doc] Add an ELisp snippet to insert Sphinx roles and quotesGravatar Clément Pit-Claudel2018-05-15
| |_|_|/ / / / / |/| | | | | | |
| * | | | | | | Update MERGING.mdGravatar Matthieu Sozeau2018-05-15
| | | | | | | | | | | | | | | | | | | | | | | | Simpler
| * | | | | | | Update MERGING.mdGravatar Matthieu Sozeau2018-05-15
| | | | | | | | | | | | | | | | | | | | | | | | Actually there are more general instructions
| * | | | | | | git / gpg integration linkGravatar Matthieu Sozeau2018-05-15
| | |_|/ / / / | |/| | | | |
* | | | | | | Merge PR #7213: Do not compute constr matching context if not used.Gravatar Matthieu Sozeau2018-05-15
|\ \ \ \ \ \ \ | |/ / / / / / |/| | | | | |
* | | | | | | Merge PR #7170: Script to identify the code owner for given filesGravatar Maxime Dénès2018-05-14
|\ \ \ \ \ \ \
| | | | * | | | Update CI README with info about gitlab windows and docker jobs.Gravatar Gaëtan Gilbert2018-05-14
| |_|_|/ / / / |/| | | | | |
* | | | | | | Merge PR #7337: dir-locals: add bug-reference-mode variablesGravatar Emilio Jesus Gallego Arias2018-05-14
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7482: Update CI documentation following recent evolutions.Gravatar Emilio Jesus Gallego Arias2018-05-14
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7344: Windows packaging build with Gitlab CIGravatar Gaëtan Gilbert2018-05-14
|\ \ \ \ \ \ \ \ \
| | | | | | * | | | Pick up user overlays when running GitLab CI on PRs.Gravatar Théo Zimmermann2018-05-14
| |_|_|_|_|/ / / / |/| | | | | | | |
| | * | | | | | | Update CI documentation following recent evolutions.Gravatar Théo Zimmermann2018-05-14
| | | | | | | | |
| | | | | | | * | Infrastructure for ocamldebug on the checkerGravatar Gaëtan Gilbert2018-05-13
| |_|_|_|_|_|/ / |/| | | | | | |
* | | | | | | | Merge PR #7470: use at least 6 Xs in mktemp filename templatesGravatar Gaëtan Gilbert2018-05-11
|\ \ \ \ \ \ \ \ | |_|/ / / / / / |/| | | | | | |
| | | * | | | | coqdev.el: add bug-reference-mode variablesGravatar Gaëtan Gilbert2018-05-11
| | | | | | | |
| | * | | | | | Windows packaging build with Gitlab CIGravatar Maxime Dénès2018-05-11
| |/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | [ci] Add mit-plv/cross-cryptoGravatar Jason Gross2018-05-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything.
| * | | | | | use at least 6 Xs in mktemp filename templatesGravatar Sven M. Hallberg2018-05-09
|/ / / / / / | | | | | | | | | | | | | | | | | | OpenBSD mktemp fails with an error otherwise.
* | | | | | Merge PR #7435: [gitlab] Add bleeding-edge flambda build.Gravatar Gaëtan Gilbert2018-05-09
|\ \ \ \ \ \
| | | | | * | [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We move syntax for universes from `Misctypes` to `Glob_term`. There is basically no reason that this type is there instead of the proper file, as witnessed by the diff. Unfortunately the change is not compatible due to moving a type to a higher level in the hierarchy, but we expect few problems. This change plus the related PR (#6515) moving universe declaration to their proper place make `Misctypes` into basically an empty file save for introduction patterns.
| * | | | | [gitlab] Add bleeding-edge flambda build.Gravatar Emilio Jesus Gallego Arias2018-05-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | Merge PR #7347: Fix for #7081 (Windows lablgtk) and #7083 (Windows logging)Gravatar Maxime Dénès2018-05-07
|\ \ \ \ \ \ | |/ / / / / |/| | | | |
* | | | | | [ci] Add ounit to the base Docker package set.Gravatar Emilio Jesus Gallego Arias2018-05-07
| | | | | | | | | | | | | | | | | | | | | | | | This should help #6808.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 01:16:38 +0000