aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2019-01-29Merge PR #9417: Update update-compat.py scriptThéo Zimmermann
Reviewed-by: Zimmi48
2019-01-29Update update-compat.py scriptJason Gross
It now removes the outdated `CompatOldOldFlag.v` file on `--release`, and it now correctly updates `bug_9166.v` which seems to specifically be about the compat flag behavior. Additionally, it inserts an "autogenerated" notice at top of the two bug files, and makes them read-only.
2019-01-29Use \mathcal instead of \calGaëtan Gilbert
Apparently it's deprecated / doesn't always work, see https://tex.stackexchange.com/questions/84041/why-does-calm-n-give-m See #9429 (we also need to fix the distributed file on the server).
2019-01-29Merge PR #9383: Remove travisVincent Laporte
Reviewed-by: Zimmi48 Reviewed-by: vbgl
2019-01-27Merge PR #9263: [STM] explicit handling of parsing statesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares Ack-by: maximedenes
2019-01-24Update update-compat.py and release-process.mdJason Gross
In response to review comments by Zimmi48
2019-01-24Update update-compat.py scriptJason Gross
We now support --master and --release. On the master branch, we support four compatibility versions, while on releases and release branches, we support only three compatibility versions. We also support --git-add to automatically run `git add` with new and updated files, and to run `git rm` with deleted files.
2019-01-24Add OverlaysMaxime Dénès
2019-01-24[nix-CI] Split the build inputsVincent Laporte
Coq and the Coq libraries can now be excluded (by setting the NOCOQ environment variable).
2019-01-24[Nix-ci] Add QuickChickVincent Laporte
2019-01-24[Nix-ci] Fix UnicoqVincent Laporte
2019-01-24[Nix-ci] Add formal-topologyVincent Laporte
2019-01-23Merge PR #9043: [windows] Cleanup cruft from `dev/build/windows`Michael Soegtrop
Reviewed-by: MSoegtropIMC
2019-01-23Merge PR #9239: [ci] [appveyor] Pass -j2 to Appveyor's build and build test ↵Maxime Dénès
suite again
2019-01-22Remove travisGaëtan Gilbert
The azure OSX job replaces the first travis job, and the second always fails and so is useless.
2019-01-22Merge PR #9225: Fix issue: Windows CI: cygwin install cache is not reused #9212Maxime Dénès
Reviewed-by: maximedenes
2019-01-17Fix merge-pr.sh when multiple review commentsGaëtan Gilbert
It used to output duplicate trailers.
2019-01-17Merge PR #9345: [ci] Update fiat-crypto to the new pipelineGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-01-17Merge PR #9192: Issue #9175, #9190, #9191 (various minor Windows build issues)Maxime Dénès
Reviewed-by: Zimmi48
2019-01-17Merge PR #9242: merge-pr: add reviewer info to commit messageMaxime Dénès
Reviewed-by: maximedenes Ack-by: ejgallego
2019-01-16[ci] Update fiat-crypto to the new pipelineJason Gross
We're recently reorganized fiat-crypto. This should fix the OOM CI issues. Fixes #9338
2019-01-11Merge pull request #8778 from SkySkimmer/merge-plugin-tutoYves Bertot
Move plugin tutorial to Coq repo
2019-01-08[ci] Update fiat-crypto legacyJason Gross
Once https://github.com/mit-plv/fiat-crypto/pull/477 is merged, the master branch will no longer contain the files nor the targets for fiat-crypto legacy. (We should perhaps consider moving fiat-crypto legacy to coq-community as a source of vm and printing tests.)
2019-01-08Integrate plugin tutorial after code importGaëtan Gilbert
2019-01-08merge-pr: add reviewer info to commit messageGaëtan Gilbert
This produces a commit message like ~~~ Merge PR #9250: coqchk: fix check for kelim with functors Reviewed-by: ppedrot Ack-by: mattam92 ~~~
2019-01-07Merge PR #9309: [ci] Add Verdi Raft with dependencies to CIEmilio Jesus Gallego Arias
2019-01-05[ci] Add Verdi Raft with dependencies to CIKarl Palmskog
2019-01-04Remove formal-topology from CIMaxime Dénès
This was suggested by the author. See https://github.com/bmsherman/topology/issues/23
2018-12-27Merge PR #9224: Move lint job to gitlabEmilio Jesus Gallego Arias
2018-12-25[windows] Cleanup cruft from `dev/build/windows`Emilio Jesus Gallego Arias
The amount of cruft we are carrying there is high enough as to even difficult navigation. More cleanup should be performed, but this is a first step.
2018-12-25[ci] [appveyor] Pass -j2 to Appveyor's build.Emilio Jesus Gallego Arias
2018-12-21Move lint job to gitlabGaëtan Gilbert
This changes the semantics a bit since we don't have TRAVIS_COMMIT_RANGE anymore, instead we do per-commit linting for the commits since the last merge commit.
2018-12-20Fix line ending issuesGaëtan Gilbert
Try to mimick MSoegtropIMC (https://github.com/coq/coq/pull/9243#issuecomment-448968353 )
2018-12-18Merge PR #9215: Set up CI with Azure PipelinesEmilio Jesus Gallego Arias
2018-12-17Merge PR #9153: [api] Move reduction modules to `tactics`Pierre-Marie Pédrot
2018-12-17Set up CI with Azure PipelinesGaëtan Gilbert
2018-12-17Merge PR #8856: [gitlab] Test Ocaml trunk.Gaëtan Gilbert
2018-12-17Fix git line ending conversion in windowsGaëtan Gilbert
2018-12-17Merge PR #9220: Move shallow state logic to the function preparing state for ↵Enrico Tassi
workers
2018-12-16Merge PR #9172: [proof] Rework proof interface.Pierre-Marie Pédrot
2018-12-14Fix issue: Windows CI: cygwin install cache is not reused #9212Michael Soegtrop
2018-12-14[dune] [gitlab] Test OCaml trunk.Emilio Jesus Gallego Arias
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`] CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit` cannot be currently installed, thus we have to add a switch to the test suite to disable `unit-tests`. Many deprecation warnings happened in 4.08 so we use the `release` profile to make them not fatal. Using a 4.08 build profile would be an option too.
2018-12-14Merge PR #9147: [dune] [doc] Support for building the reference manual with ↵Théo Zimmermann
Dune.
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
- deprecate the old 5-tuple accessor in favor of a view record, - move `name` and `kind` proof data from `Proof_global` to `Proof`, this will prove useful in subsequent functionalizations of the interface, in particular this is what abstract, which lives in the monads, needs in order no to access global state. - Note that `Proof.t` and `Proof_global.t` are redundant anyways.
2018-12-13Add overlayMaxime Dénès
2018-12-13Merge PR #9210: Fix issue #9176 : Windows: change cygwin repoThéo Zimmermann
2018-12-13[dune] [doc] Support for building the reference manual with Dune.Emilio Jesus Gallego Arias
This is a reduced version of #8503 as to provide a way to build the reference manual with Dune. Dune 1.6 supports (experimentally) directories as targets, thus we introduce a rule that will call `sphinx` to build the manual. This only provides build, however generation of `.install` rules is not done, it will be hopefully addressed in #8503. Note that we set `expire: 1 month` for all the artifacts we build with Dune. IMHO this makes most sense as not to abuse Gitlab's hosting, however of course we could consider a different deployment strategy if wanted.
2018-12-13Merge PR #9217: [ci] [appveyor] Temporally disable test suite on Appveyor.Gaëtan Gilbert
2018-12-13[ci] [appveyor] Temporally disable test suite on Appveyor.Emilio Jesus Gallego Arias
Hopefully we will re-enable it back soon, I am preparing a refactoring that should make it more robust w.r.t paths and changes on Windows which will enable to use a faster build system. But now it is timing out 100% of the times [due to #8655] so it is not useful.
2018-12-12Higher-level libobject API for objects with fixed scopesMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-22 22:49:45 +0000