aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2018-05-26Merge PR #7603: Use -j 1 for high memory fiat crypto targetsEmilio Jesus Gallego Arias
2018-05-26Merge PR #6057: Start a release process documentation.Maxime Dénès
2018-05-25Use -j 1 for high memory fiat crypto targetsGaëtan Gilbert
2018-05-24[tactics] Remove anonymous fix/cofix form.Emilio Jesus Gallego Arias
We remove the `fix N / cofix N` forms from the tactic language. This way, these tactics don't depend anymore on the proof context, in particular on the proof name, which seems like a fragile practice. Apart from the concerns wrt maintenability of proof scripts, this also helps making the "proof state" functional; as we don't have to propagate the proof name to the tactic layer.
2018-05-24Merge PR #7574: Improve merging and overlay documentations.Emilio Jesus Gallego Arias
2018-05-24Complete rewrite of the documentation of overlays after Jim's additional ↵Théo Zimmermann
comments. [ci skip]
2018-05-24Relax advice on the name of user-overlays following Gaëtan's suggestion.Théo Zimmermann
[ci skip]
2018-05-24Improve merging and overlay documentations.Théo Zimmermann
Clarification prompted by Jim Fehrle. [ci skip]
2018-05-24Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵Pierre-Marie Pédrot
in CArray
2018-05-24Merge PR #7582: [ci] Build fiat-crypto targets in sequenceEmilio Jesus Gallego Arias
2018-05-23Document Smart/Array changes in dev/doc/Changes.md.Hugo Herbelin
2018-05-22[ci] Build fiat-crypto targets in sequenceJason Gross
This should hopefully alleviate memory problems on gitlab, by first building the `lite` targets, and then building the remaining not-that-big targets.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 22:09:41 +0000