aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2020-09-15[zarith] [micromega] Bump to 1.10 and remove some hacksEmilio Jesus Gallego Arias
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see https://github.com/ocaml/Zarith/issues/58
2020-09-14[nix] Update ref for ocamlformat 0.15Emilio Jesus Gallego Arias
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-09-14[ci] [docker] Up testing to OCaml 4.11.1Emilio Jesus Gallego Arias
- `odoc` must be bumped to support 4.11
2020-09-11[ci] [mathcomp] run the test suiteEnrico Tassi
2020-09-10Add simple-io to dev/ci/nix.Théo Zimmermann
2020-09-04Merge PR #12969: CI: build Iris examples instead of lambda-Rustcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-03[bench] Only upload some filesJason Gross
We will now also record a listing of all files that we could have uploaded, in case we want to know what's available to upload in the future.
2020-09-03[bench] Also upload the raw timing files, etcJason Gross
2020-09-03Merge PR #12968: Replace `frozen` by `allowed` evars in evarconv, and delay themPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-03Merge PR #12899: [bench] Update bench script with better urls and more infoPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-03Add Equations overlayMaxime Dénès
2020-09-02fix grepping for the Iris commitRalf Jung
2020-09-02CI: build Iris examples instead of lambda-RustRalf Jung
2020-09-01Merge PR #12892: Update update_global_env usagePierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
2020-08-31Add zarith to the include path for ocamldebug-coqJasper Hugunin
2020-08-31Merge PR #12958: Fix load_printers after zarithcoqbot-app[bot]
Reviewed-by: ejgallego
2020-08-31Update update_global_env usageGaëtan Gilbert
- take just a ugraph instead of the whole env - rename to update_sigma_univs - push global env lookup a bit further up - fix vernacinterp call to update all surrounding proofs, not just the top one - flip argument order for nicer partial applications
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-31Fix load_printers after zarithGaëtan Gilbert
2020-08-28Adding overlay for coq-elpi.Hugo Herbelin
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: silene
2020-08-26Use the lite variants of performance tests in the bench default packages.Pierre-Marie Pédrot
They are much faster and should be as informative as their heavy counterparts. I have been forgetting to do that for a long time already.
2020-08-26Merge PR #12904: Move bench job definition to its own filePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-25Move bench job definition to its own fileGaëtan Gilbert
This focuses review requests to bench-maintainers instead of sharing with ci-maintainers
2020-08-25Remove useless commit guessing logicJason Gross
On GitLab, we don't need to base the job info on the PR number, since it ought to be available from the git repo. Removing the logic will make the bench infrastructure more uniform.
2020-08-25[bench] Update bench script with better urls and more infoJason Gross
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
2020-08-25Merge PR #12882: Perform a few tweaks to make the bench script work properly.coqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: ppedrot
2020-08-25Merge PR #12798: Change OUnit package name to ounit2.coqbot-app[bot]
Reviewed-by: ejgallego
2020-08-24Fix Coqtail test directory.whonore
Tests moved in https://github.com/whonore/Coqtail/pull/134.
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
Added user overlay for bignums
2020-08-24Merge PR #12565: Dnets now consider axioms as being opaque for pattern ↵coqbot
recognition. Reviewed-by: mattam82
2020-08-24Perform a few tweaks to make the bench script work properly.Pierre-Marie Pédrot
2020-08-20Special commit to start benchmarking.Maxime Dénès
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
Reviewed-by: herbelin Reviewed-by: maximedenes
2020-08-20Adding overlays.Pierre-Marie Pédrot
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
Try just going with the user-given names, and not worrying about what happens with repeated names or anonymous implicits. (Support for anonymous implicits is due to herbelin in #11098.) This PR should not change behaviour in the absence of repeated names. Since repeated names are already a poorly handled corner case, I would recommend changing binder names to avoid overlap in the case of a change in behavior. Since anonymous implicits and implicits with repeated names can already happen, I think this is unlikely to cause too many new problems, though it might exacerbate existing ones. However, I already had to fix one newly possible anomaly, so I can't be too confident. The most common change in external developments was that an argument no longer gets `0` appended to it, causing the `Arguments` command to complain about renaming. To fix this and keep the old name, one can simply use the `rename` flag as suggested, or switch to the new, un-suffixed name. Closes #6785 Closes #12001 Another step towards checking the standard library with `-mangle-names`.
2020-08-19Add overlay.Pierre-Marie Pédrot
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-08-18Dockerfile: Update ounitGaëtan Gilbert
2020-08-13Merge PR #12720: Factor code related to class hint clenvHugo Herbelin
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2020-08-12Merge PR #12748: Windows CI: changed cygwin repo servercoqbot
Reviewed-by: Zimmi48
2020-08-12Add overlays.Pierre-Marie Pédrot
2020-08-12Windows CI: changed cygwin repo serverMichael Soegtrop
2020-08-11Merge PR #12717: More documentation on grammars and parsingPierre-Marie Pédrot
Reviewed-by: Zimmi48 Ack-by: herbelin Reviewed-by: ppedrot
2020-08-03More documentation on grammars and parsingJim Fehrle
2020-07-24CI metacoq: make .merlinGaëtan Gilbert
For convenience
2020-07-23Merge PR #12679: Remove redundant data from VM case switch.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: silene
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
No need to store the case_info, all the data is reconstructible from the context. Furthermore, this reconstruction is performed in a context where we already access the environment, so performance is not at stake. Hopefully this will also reduce the number of globally allocated VM values, since the switch representation now only depends on the shape of the inductive type.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:51:50 +0000