aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-12-14Circle CI: separate job to boot opam with all used packages.Gaëtan Gilbert
2017-12-14Circle CI: remove warning jobsGaëtan Gilbert
2017-12-14Circle CI: cat failed test suite logsGaëtan Gilbert
2017-12-13Circle CI: uses dependencies between external developments.Gaëtan Gilbert
2017-12-13Put bignums, math-classes and corn dependencies in MakefileGaëtan Gilbert
2017-12-13Circle CI: enable TIMED for external developmentsGaëtan Gilbert
2017-12-13Circle CI: use cache for opamGaëtan Gilbert
2017-12-13Circle CI: enable native compiler.Gaëtan Gilbert
2017-12-12Near-full implementation of Circle CI.Gaëtan Gilbert
VS gitlab: + fiat-crypto (Circle has 4GB RAM, gitlab 2GB) - caching opam (TODO) - publishing artefacts (TODO) * tests with -local, not installed VS travis: + reusing build products - flambda validate job (TODO?) - OSX jobs (TODO at least check if free OSX is possible) - linter (TODO?)
2017-12-11CI: poc Circleci configurationArnaud Spiwack
Revert "CI: poc Circleci configuration" Committed on master by mistake. Clearly I'm too clumsy to be trusted with push rights. This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34. CI: poc Circleci configuration Fixup Try minimising build for faster testing Various fixes Fixup: yaml identation Do not -j2: native compiler seems to take too much memory Revert "Do not -j2: native compiler seems to take too much memory" This reverts commit 4886151288a8d895c0fd23f9bded0970c59e1372. Deactivate native compiler Fixup (how did this happen?) Do not call time (not install on docker images, will fix later) Fixup Fixup
2017-12-11Merge PR #6368: [api] Remove yet another type alias.Maxime Dénès
2017-12-11Merge PR #6352: [makefile] Address #6291: install more development files.Maxime Dénès
2017-12-11Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Maxime Dénès
2017-12-11Merge PR #1150: [stm] Remove all but one use of VtUnknown.Maxime Dénès
2017-12-11Merge PR #6338: Remove up-to-conversion term matchingMaxime Dénès
2017-12-11Merge PR #6369: [api] Remove kernel dependency on intf (Decl_kind)Maxime Dénès
2017-12-11Merge PR #6363: [META] Some dependency fixes.Maxime Dénès
2017-12-11Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.Maxime Dénès
2017-12-11Merge PR #6351: Fix a copy-paste error in ci-ltac2.Maxime Dénès
2017-12-11Merge PR #6346: [ci] CoLoR has moved to githubMaxime Dénès
2017-12-11Merge PR #6340: [default.nix] Add ocpIndent and ocp-index.Maxime Dénès
2017-12-10Merge PR #6370: [ci] Temporal workaround for checker non-backwards ↵Maxime Dénès
compatible change.
2017-12-10[ci] Temporal workaround for checker non-backwards compatible change.Emilio Jesus Gallego Arias
2017-12-10[api] Remove kernel dependency on intf (Decl_kind)Emilio Jesus Gallego Arias
We more the `recursivity_kind` type to `Declarations`, this indeed makes sense, and now `Decl_kind` morally lives in `library` as it should.
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-09[META] Some dependency fixes.Emilio Jesus Gallego Arias
2017-12-09[stm] Remove all but one use of VtUnknown.Emilio Jesus Gallego Arias
Together with #1122, this makes `VernacInstance` the only command in the Coq codebase that cannot be statically determined to open a proof. The reasoning for the commands moved to `VtSideff` is that parser-altering commands should be always marked `VtNow`; the rest can be usually marked as `VtLater`.
2017-12-09Remove up-to-conversion matching functions.Pierre-Marie Pédrot
They were not used anymore since the previous patches.
2017-12-09[ci] Download ci-sf archives into the proper CI build dir.Emilio Jesus Gallego Arias
Currently, `make ci-sf` downloads and builds the files in the main root directory. we fix that.
2017-12-08Revert "CI: poc Circleci configuration"Arnaud Spiwack
Committed on master by mistake. Clearly I'm too clumsy to be trusted with push rights. This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34.
2017-12-08CI: poc Circleci configurationArnaud Spiwack
2017-12-08[makefile] Address #6291: install more development files.Emilio Jesus Gallego Arias
As noted in the bug #6291, `.cmx` files are not installed in the coqlib, which yields the warning: ``` Warning 58: no cmx file was found in path for module Sorts, and its interface was not compiled with -opaque ``` We thus install the `cmx` files to fix this problem, and also install the `.o` files for plugins' `.o` to support linking the plugins statically. This closes #5099 and #6291.
2017-12-08Fix a copy-paste error in ci-ltac2.Théo Zimmermann
2017-12-08Merge PR #6334: Remove dead code in ReductionopsMaxime Dénès
2017-12-08Merge PR #6158: Allows a level in the raw and glob printersMaxime Dénès
2017-12-08Merge PR #6224: Add alienclean target to remove compilation products with no ↵Maxime Dénès
source.
2017-12-07[ci] CoLoR has moved to githubEmilio Jesus Gallego Arias
Closes #6194 .
2017-12-07Merge PR #6267: Fix PR merge script.Maxime Dénès
2017-12-07[default.nix] Add ocpIndent and ocp-index.Maxime Dénès
2017-12-07Getting rid of pf_matches in Hipattern.Pierre-Marie Pédrot
Funnily enough, the old code is completely bogus. It succeeds in early files of the prelude just because the heterogeneous equality has not been required. This raises an exception which is not the same one as if we tried to rewrite with the identity type first. The only user, the inversion tactic, was actually only relying on Logic.eq and was furthermore not even using the convertibility algorithm. We just perform a syntactic match now.
2017-12-07Merge PR #6290: Rename update to set, Fixes #6196Maxime Dénès
2017-12-07Merge PR #873: New strategy based on open scopes for deciding which notation ↵Maxime Dénès
to use among several of them
2017-12-07Merge PR #6142: Single quotes break on WindowsMaxime Dénès
2017-12-07Merge PR #6277: Qualified import in coqchkMaxime Dénès
2017-12-07Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding)Maxime Dénès
2017-12-07Merge PR #6321: Use preference for ocamlfind in configureMaxime Dénès
2017-12-07Merge PR #6316: Correct typoMaxime Dénès
2017-12-07Merge PR #6309: [default.nix] needs ncurses for the test-suiteMaxime Dénès
2017-12-07Merge PR #6303: Remove redundant Zcase from the checker.Maxime Dénès
2017-12-06Getting rid of pf_is_matching in Funind.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:06:09 +0000