aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2018-05-22Merge PR #7577: Fixing debugger after #6859 (loading dynlink.cma before ↵Emilio Jesus Gallego Arias
lib.cma).
2018-05-22Fixing debugger after #6859 (loading dynlink.cma before lib.cma).Hugo Herbelin
2018-05-22Merge PR #7384: Split UniversesPierre-Marie Pédrot
2018-05-22Merge PR #7324: Infrastructure for ocamldebug on the checkerHugo Herbelin
2018-05-22Merge PR #7526: [circle] Use Docker image from Gitlab registry.Gaëtan Gilbert
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
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.
2018-05-19Merge PR #7527: [windows] Don't build menhir and int anymore in the ↵Michael Soegtrop
packaging scripts.
2018-05-18Merge PR #7550: [CI] Fix the script used by math-classes.Emilio Jesus Gallego Arias
2018-05-18Merge PR #6965: [api] Move universe syntax to `Glob_term`Pierre-Marie Pédrot
2018-05-18Create a documentation for the release manager.Théo Zimmermann
This process is expected to evolve in the future as we automate it more and more. [ci skip]
2018-05-18[CI] Fix the script used by math-classes.Pierre-Marie Pédrot
We call configure to properly regenerate the Makefile and its dependencies.
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
This API is a bit strange, I expect it will change at some point.
2018-05-17[circle] Use Docker image from Gitlab registry.Emilio Jesus Gallego Arias
2018-05-17Merge PR #7525: [ci] Try to build more of fiat-crypto.Gaëtan Gilbert
2018-05-17Merge PR #6808: Add unit tests to test-suiteGaëtan Gilbert
2018-05-16[ci] Try to build more of fiat-crypto.Emilio Jesus Gallego Arias
2018-05-16Merge PR #7514: [ci] Don't build lite versions of CI developments.Gaëtan Gilbert
2018-05-16Merge PR #7391: Add a small documentation writer's guideMaxime Dénès
2018-05-16[windows] Don't make menhir and int anymore.Emilio Jesus Gallego Arias
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.
2018-05-16add unit tests to test suitePaul Steckler
2018-05-16Merge PR #7442: Gitlab: build docker image in pipeline and use through registry.Emilio Jesus Gallego Arias
2018-05-16[ci] Don't build lite versions of CI developments.Emilio Jesus Gallego Arias
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.
2018-05-16Merge PR #7505: Pick up user overlays when running GitLab CI on PRs.Emilio Jesus Gallego Arias
2018-05-15Merge PR #7519: git / gpg integration linkThéo Zimmermann
2018-05-15[doc] Add an ELisp snippet to insert Sphinx roles and quotesClément Pit-Claudel
2018-05-15Update MERGING.mdMatthieu Sozeau
Simpler
2018-05-15Update MERGING.mdMatthieu Sozeau
Actually there are more general instructions
2018-05-15git / gpg integration linkMatthieu Sozeau
2018-05-15Merge PR #7213: Do not compute constr matching context if not used.Matthieu Sozeau
2018-05-14Merge PR #7170: Script to identify the code owner for given filesMaxime Dénès
2018-05-14Update CI README with info about gitlab windows and docker jobs.Gaëtan Gilbert
2018-05-14Merge PR #7337: dir-locals: add bug-reference-mode variablesEmilio Jesus Gallego Arias
2018-05-14Merge PR #7482: Update CI documentation following recent evolutions.Emilio Jesus Gallego Arias
2018-05-14Merge PR #7344: Windows packaging build with Gitlab CIGaëtan Gilbert
2018-05-14Pick up user overlays when running GitLab CI on PRs.Théo Zimmermann
2018-05-14Update CI documentation following recent evolutions.Théo Zimmermann
2018-05-13Infrastructure for ocamldebug on the checkerGaëtan Gilbert
2018-05-11Merge PR #7470: use at least 6 Xs in mktemp filename templatesGaëtan Gilbert
2018-05-11coqdev.el: add bug-reference-mode variablesGaëtan Gilbert
2018-05-11Windows packaging build with Gitlab CIMaxime 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-09[ci] Add mit-plv/cross-cryptoJason Gross
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything.
2018-05-09use at least 6 Xs in mktemp filename templatesSven M. Hallberg
OpenBSD mktemp fails with an error otherwise.
2018-05-09Merge PR #7435: [gitlab] Add bleeding-edge flambda build.Gaëtan Gilbert
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
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.
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-07Merge PR #7347: Fix for #7081 (Windows lablgtk) and #7083 (Windows logging)Maxime Dénès
2018-05-07[ci] Add ounit to the base Docker package set.Emilio Jesus Gallego Arias
This should help #6808.
2018-05-06Merge PR #7387: [gitlab] [circleci] Use a Docker base image for CIGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 07:36:27 +0000