aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-13Remove floating-point comparison operators as they are no longer needed.Guillaume Melquiond
2020-11-13Turn coq_float64.h into a .c file as it is no longer needed by coq_interp.c.Guillaume Melquiond
2020-11-13Inline the functions from coq_float64.h.Guillaume Melquiond
Since the code is compiled in -fPIC mode, the compiler cannot inline the functions, due to the ABI mandating the ability to interpose visible symbols. Hiding the symbols of coq_float64.h would work, except that they float64.ml needs to reference them. (See #13124 for more details.) This commit improves performances by 7% on the following code. From Coq Require Import Int63 BinPos PrimFloat. Definition foo n := let two := of_int63 2 in Pos.iter (fun x => sub (mul x two) two) two n. Time Eval vm_compute in foo 100000000. If we consider only the floating-point operations (by ignoring the cost of the loop), the speedup is actually 30%.
2020-11-13Make callback opcodes more generic.Guillaume Melquiond
This does not make the code any slower, since Is_coq_array(accu) && Is_uint63(sp[0]) and !Is_accu(accu) && !Is_accu(sp[0]) take the exact same number of tests to pass in the concrete case. In the accumulator case, it takes one more test to fail, but we do not care about the performances then.
2020-11-13Optimize Is_accu a bit.Guillaume Melquiond
2020-11-13Improve documentation of closure representations.Guillaume Melquiond
2020-11-13Turn Ksequence into a unary opcode, as its binary structure was never used.Guillaume Melquiond
2020-11-13Remove unused if-then-else construct from VM.Guillaume Melquiond
2020-11-13Restore discard_dead_code and use it to simplify match-with constructs.Guillaume Melquiond
Otherwise, these constructs would be followed by a spurious Kreturn opcode, when in tail position.
2020-11-13Remove some unused opcodes from VM.Guillaume Melquiond
2020-11-13Remove unchecked arithmetic operations from VM, as they are not used.Guillaume Melquiond
2020-11-13Optimize handling of the VM stack with respect to the GC.Guillaume Melquiond
1. There is no point in marking plain integers as GC roots. 2. There is no need to restore the stack pointer, as the stack is not allocated on the OCaml heap (contrarily to coq_env).
2020-11-13Merge PR #12420: [stdlib] Decidable instance for negationcoqbot-app[bot]
Reviewed-by: Blaisorblade Ack-by: SkySkimmer
2020-11-12Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and popcoqbot-app[bot]
Reviewed-by: gares Ack-by: SkySkimmer Ack-by: ejgallego
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-11-12Merge PR #13318: Turn ssr proxy notation for supporting ↵coqbot-app[bot]
second-order/contextual pattern abbreviations to only parsing Reviewed-by: gares
2020-11-12Merge PR #13361: Move last changelog entry for 8.12.1.coqbot-app[bot]
Reviewed-by: ejgallego
2020-11-12Move last changelog entry for 8.12.1.Théo Zimmermann
2020-11-12Merge PR #13359: Print failed test suite logs in CIcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, ↵coqbot-app[bot]
not only on subidentifiers of an identifier Reviewed-by: Zimmi48
2020-11-12Merge PR #13355: Fix Iris CI scriptcoqbot-app[bot]
Reviewed-by: ejgallego Ack-by: RalfJung Ack-by: Zimmi48
2020-11-12Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: SkySkimmer Ack-by: gares Ack-by: jfehrle Ack-by: jashug Ack-by: ejgallego
2020-11-12Print failed test suite logs in CIGaëtan Gilbert
in addition to having them as artefacts
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ↵Pierre-Marie Pédrot
naming Ack-by: gares Reviewed-by: ppedrot
2020-11-12Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -Icoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: Zimmi48 Ack-by: ppedrot Ack-by: jfehrle
2020-11-12Add the test as a misc script.Pierre-Marie Pédrot
I left the other test as a v file since it might become relevant when the corresponding Qed bug is fixed.
2020-11-12Add documentation about the soundness bug.Pierre-Marie Pédrot
2020-11-12Fix #13330: Kernel messes with polymorphic side-effects.Pierre-Marie Pédrot
Polymorphic side-effects generated in monomorphic mode would be counted towards trusted subcomponents. This would allow to make ill-typed terms pass as legitimate by mimicking the shape of the inlining of monomorphic side-effects in such a proof.
2020-11-12Fix Iris CI scriptGaëtan Gilbert
Also add nice error message when the grep produces an empty result
2020-11-12Add changelog for #13345.Hugo Herbelin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-12Clarifying the role of Add ML Path vs -I (see #13344).Hugo Herbelin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
Reviewed-by: gares Ack-by: Zimmi48
2020-11-11Add changelog for #13351.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-10Merge PR #13335: Fix running unit tests with dune compiled coqcoqbot-app[bot]
Reviewed-by: ejgallego
2020-11-10Merge PR #13315: Convert logic chapter to prodncoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-10Fix running unit tests with dune compiled coqGaëtan Gilbert
(for runs outside dune, ie "make -C test-suite unit-tests" rather than "dune build @runtest") Fix #13333
2020-11-10Merge PR #13325: [compat] remove 8.10coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-10Merge PR #13322: [obligation] Properly handle no obligations on `Next ↵coqbot-app[bot]
Obligation` Reviewed-by: SkySkimmer
2020-11-10Merge PR #13297: Remove the native symbol registering from the safe environment.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-09Add additional escape sequences for notationsJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-11-09Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, ↵coqbot-app[bot]
OCaml and Gallina. Reviewed-by: jfehrle Reviewed-by: cpitclaudel
2020-11-09Merge PR #13327: Fix documentation of Ltac ::=coqbot-app[bot]
Reviewed-by: jfehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-09[obligation] Proper handle no obligations on `Next Obligation`Emilio Jesus Gallego Arias
Fixes #13320 . Trivial programming error, actually this is handled better in a further refactoring branch not submitted due to the long time the whole rework took.
2020-11-09Remove virtually unused replace rule.Théo Zimmermann
2020-11-09Fix #5226: Add index entry for ::=.Théo Zimmermann
2020-11-09Fix indentation of todo in Ltac chapter.Théo Zimmermann
Actual documentation was interpreted as a comment.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:02:55 +0000