aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2020-04-01Merge PR #11873: python3 script does not need to import from the futureEmilio Jesus Gallego Arias
Reviewed-by: JasonGross
2020-04-01Merge PR #11971: [ci] Run bignums' testsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-31Merge PR #11818: [proof] Further consolidation of the regular declaration pathGaëtan Gilbert
Ack-by: Matafou Reviewed-by: SkySkimmer
2020-03-31Merge PR #11131: [ci] [gitlab] Add test-suite test for OCaml 4.10 and 4.11Théo Zimmermann
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2020-03-31[ci] Run bignums' testsPierre Roux
2020-03-30[ci] [overlays] Adapt to declare API changes.Emilio Jesus Gallego Arias
- problem with metacoq overlay ; it expects to send a non-ground constant to the kernel, now it fails at prepare. Record Sigma (A : Type) (B : A -> Type) : Type := { fst : A ; snd : B fst }. Arguments fst {A B}. Arguments snd {A B}. Quote Recursively Definition foo := (fst, snd). There is a hack on the overlay, we need to discuss it a bit more.
2020-03-30Fix commit hook when there are no changes (eg amend message)Gaëtan Gilbert
Fix #11967
2020-03-30Merge PR #11874: Auto-format micromega files in pre-commit hook.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-03-29[ci] [gitlab] Bump to edge to OCaml 4.10, add test-suite for OCaml 4.11Emilio Jesus Gallego Arias
2020-03-26[ci] Add bbvJason Gross
I believe a recent commit to master broke it, and now that it's no longer tested as part of fiat-crypto-legacy, I think it's time to add it.
2020-03-24Merge PR #11703: Making of NumTok an API for numeralPierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: proux01
2020-03-24Run ocamlformat on modified ml / mli files in pre-commit hook.Théo Zimmermann
Thanks to `.ocamlformat-ignore`, we can call ocamlformat blindly but only the non-ignored files will be affected. Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-23[ci] add metacoqMatthieu Sozeau
2020-03-22Overlay for QuickChickHugo Herbelin
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him.
2020-03-22Merge PR #11731: [proof] Miscellaneous refactoringsGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-03-20python3 script does not need to import from the futureRalf Treinen
2020-03-19[ocamformat] Update to 0.13.0Emilio Jesus Gallego Arias
We include the `version=0.13.0` field that should help users not to use the wrong version. `disable=true` still seems a noop with `dune`. There are some minor changes in the way comments are formatted; I'm unsure if this is due to the `wrap-comments` option; as always; tweaks to the config are most welcome.
2020-03-19[obligations] Step towards more structured handling of remaining obligations.Emilio Jesus Gallego Arias
There is a lot of check overhead in the code, we will try to provide a more convenient API for manipulation of remaining obligations.
2020-03-19[ci] Overlays for declare interface refactoring.Emilio Jesus Gallego Arias
2020-03-19[refman] Remove workaround for sphinx-doc/sphinx#4983Clément Pit-Claudel
2020-03-19Merge PR #11860: [ci] [docker] Update to 4.09.1Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
Ack-by: herbelin
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-03-18[ci] [docker] Update to 4.09.1Emilio Jesus Gallego Arias
That release includes non trivial changes related C compilers, in particular due to `-fno-common` support.
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
Reviewed-by: jfehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-18Adding overlays.Pierre-Marie Pédrot
2020-03-18Also show unchanged headers.Théo Zimmermann
2020-03-18Remove dates in headers.Théo Zimmermann
Cf. discussion at #11559 and decision of Coq Call 2020-02-26.
2020-03-16[ci] Cleanup old overlays.Emilio Jesus Gallego Arias
2020-03-16[ci] [docker] Update components in Docker imageEmilio Jesus Gallego Arias
We bump ounit, odoc, and lablgtk3 ; so far this is routine maintenance.
2020-03-13Update Azure MacOS version 10.13 -> 10.14Gaëtan Gilbert
10.13 is deprecated as an azure VM Close #11449
2020-03-13Merge PR #11804: [CI] test hierarchy builder as part of elpiGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-13Deprecation of catchable_exception, to be replaced by noncritical in try-with.Hugo Herbelin
2020-03-12[ci] [doc] Point to actual docker instructions.Emilio Jesus Gallego Arias
2020-03-12Print implicit arguments in types of referencesSimonBoulier
2020-03-11Update dev/ci/ci-basic-overlay.shEnrico Tassi
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-11[CI] test hierarchy builder as part of elpiEnrico Tassi
2020-03-10Merge PR #11732: Update the OCaml version in `default.nix` to 4.09.0Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-10Merge PR #11764: Simplify mutual template polymorphismGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-09Do not erase OCAMLPATH in CI targets with Dune-built CoqMaxime Dénès
2020-03-09Add CI overlays.Pierre-Marie Pédrot
2020-03-06Merge PR #11717: [dune] [ocamldebug] Improve ocamldebug rulesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-04Add overlay for equations.Hugo Herbelin
2020-03-03Update the OCaml version in `default.nix` to 4.09.0Maxime Dénès
It is more convenient to use recent versions of OCaml while developing (better backtraces, etc).
2020-03-02Merge PR #11728: [dune] [doc] Be more explicit about coqtop dependenciesThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-01[ci] [docker] overlay for elpi 1.10Enrico Tassi
2020-03-01[ci] [docker] bump elpi to 1.10.2Enrico Tassi
2020-03-01[ci] bump dune to 2.0.1 due to upstream problemsEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 00:00:04 +0000