aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-28CI script wrapper now requires PythonMaxime Dénès
2020-09-27Avoid lookup up too many characters.Guillaume Melquiond
This would cause issues in noninteractive mode. For example, when using Drop, the first character of the OCaml code would be read by Coq's REPL instead of OCaml's REPL. The peek_string function is quite inefficient, since the Stream module does not provide any good function to lookup arbitrary characters (or to push back characters).
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-09-27Recognize only ":{{" as a sentence-gobbling quotation.Guillaume Melquiond
2020-09-27Make "xxx:{{" always start a quotation, whether registered or not.Guillaume Melquiond
This commit also prevents quotations using "(" and "[" from gobbling sentences. As a consequence, dynamically-registered quotations can no longer modify where Coq sentences stop.
2020-09-25Merge PR #12999: More improvements in locating tactic errorscoqbot-app[bot]
Reviewed-by: ppedrot Reviewed-by: ejgallego
2020-09-24fix ide/.merlinEnrico Tassi
2020-09-24Merge PR #12894: Modify bytecode representation of closures to please OCamls ↵coqbot-app[bot]
GC (fix #12636). Reviewed-by: maximedenes Ack-by: bgregoir Ack-by: proux01
2020-09-24Merge PR #13077: Fix issue #13065 - Windows CI brokencoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-23Fix issue #13065 - Windows CI brokenMichael Soegtrop
2020-09-23Merge PR #12977: Statically ensure that only polymophic hint terms come with ↵coqbot-app[bot]
a context. Reviewed-by: mattam82
2020-09-23Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)coqbot-app[bot]
Reviewed-by: ejgallego
2020-09-23Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of ↵Pierre-Marie Pédrot
quotations at printing time Reviewed-by: ppedrot
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-22Merge PR #13061: fix build:quick and build:base+async artifactscoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-22Merge PR #13067: Setting default value for Display Parentheses off in CoqIDEcoqbot-app[bot]
Reviewed-by: ejgallego
2020-09-22Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested ↵coqbot-app[bot]
applications in notations Reviewed-by: ejgallego Ack-by: maximedenes
2020-09-22Adding change log for #12794 and #13067.Hugo Herbelin
2020-09-22Setting default value for Display Parentheses off in CoqIDE.Hugo Herbelin
2020-09-22Add overlay for Equations.Hugo Herbelin
2020-09-22Adding change log for #13028.Hugo Herbelin
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-22Use the closure tag for accumulators.Guillaume Melquiond
The first field of accumulators points out of the OCaml heap, so using closures instead of tag-0 objects is better for the GC. Accumulators are distinguished from closures because their code pointer necessarily is the "accumulate" address, which points to an ACCUMULATE instruction.
2020-09-22Use the same memory layout as closures for accumulators.Guillaume Melquiond
That way, accumulators again can be used directly as execution environments by the bytecode interpreter. This fixes the issue of the first argument of accumulators being dropped when strongly normalizing.
2020-09-22Modify bytecode representation of closures to please OCaml's GC (fix #12636).Guillaume Melquiond
The second field of a closure can no longer be the value of the first free variable (or another closure of a mutually recursive block) but must be an offset to the first free variable. This commit makes the bytecode compiler and interpreter agnostic to the actual representation of closures. To do so, the execution environment (variable coq_env) no longer points to the currently executed closure but to the last one. This has the following consequences: - OFFSETCLOSURE(n) now always loads the n-th closure of a recursive block (counted from last to first); - ENVACC(n) now always loads the value of the n-th free variable. These two changes make the bytecode compiler simpler, since it no longer has to track the relative position of closures and free variables. The last change makes the interpreter a bit slower, since it has to adjust coq_env when executing GRABREC. Hopefully, cache locality will make the overhead negligible.
2020-09-22Merge PR #13046: Small optimization of acyclic graph merge operationcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-22Merge PR #13050: [ci/gitlab/cachix] Avoid running in trouble when calling ↵coqbot-app[bot]
git fetch --unshallow Reviewed-by: SkySkimmer
2020-09-22Merge PR #13049: [configure] Fix version checks for lablgtk and zarithcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: vbgl Ack-by: Zimmi48 Ack-by: JasonGross
2020-09-22Merge PR #13063: Make print-pretty-timed robust against non-output-sync logscoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-21Merge PR #13057: Adding debugging printers for Intmapcoqbot-app[bot]
Reviewed-by: ppedrot
2020-09-21Make print-pretty-timed robust against non-output-sync logsJason Gross
Also pass `--output-sync` on the CI, as suggested in https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect against this failure mode. Fixes #13062
2020-09-21Bump nixpkgs to get zarith 1.10.Théo Zimmermann
2020-09-21Merge PR #12723: dune: pass -bin-annot to configurecoqbot-app[bot]
Reviewed-by: ejgallego
2020-09-21fix build:quick and build:base+async artifactsGaëtan Gilbert
We put dmesg.txt in the artifact path for all build-template users, but only these 2 jobs produce it to avoid uploading unused data (see discussion in #13043).
2020-09-19Merge PR #13052: Clean up Dnet implementationHugo Herbelin
Reviewed-by: herbelin
2020-09-18Merge PR #13055: Fix Removed in Sphinx 4 deprecations.coqbot-app[bot]
Reviewed-by: jfehrle
2020-09-18Merge PR #12963: Formally deprecate the double induction tactic.Hugo Herbelin
Reviewed-by: VincentSe Ack-by: herbelin Ack-by: olaure01
2020-09-18Adding debugging printers for Intmap.Hugo Herbelin
2020-09-18Merge PR #13051: Improve `simple apply` examplecoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-18Merge PR #13043: [ci] call dmesg after quick/async jobs to detect OOMcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-18Fix Removed in Sphinx 4 deprecations.Théo Zimmermann
2020-09-18Make `simple apply in ...` point to `simple apply`Maxime Dénès
Instead, the example was duplicated.
2020-09-18[lib] make canonical_path_name always absolute (fix #13031)Enrico Tassi
2020-09-18[ci] [dmesg] save as artifactEnrico Tassi
2020-09-18Improve `simple apply` exampleMaxime Dénès
The example showing the difference between `apply` and `simple apply` used to depend on the order and the heuristics used on unification problems. We make it independent for better clarity and stability. Fixes https://github.com/coq/coq/issues/13023
2020-09-18Merge PR #12610: [leminv] [declare] Use higher-level Declare API.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-18Remove unused API from Dn.Pierre-Marie Pédrot
2020-09-18Clean up a bit the implemenation of dnets.Pierre-Marie Pédrot
We use higher-level combinators instead of composition of low-level ones.
2020-09-18Remove dead code in dnets.Pierre-Marie Pédrot
The boolean assumedly used to cut recursion was always set to true, since its introduction in 64ac193.
2020-09-18Merge PR #13027: [vernac] Don't allow attributes on print / checkcoqbot-app[bot]
Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 17:07:03 +0000