aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-02-20Inline proofs of exist_exp0 and exist_cos0.Guillaume Melquiond
2021-02-19Remove some trivial definition.Guillaume Melquiond
2021-02-19Abstract the non-computational part away.Guillaume Melquiond
2021-02-19Terminate intermediate lemmas with Qed.Guillaume Melquiond
2021-02-19Make intermediate lemmas more explicit, so that they can be terminated by Qed.Guillaume Melquiond
2021-02-19Make most of DRealAbstr opaque.Guillaume Melquiond
The function returned by DRealAbstr starts by a call to the axiom sig_forall_dec, so it is not computable anyway.
2021-02-19Terminate some lemmas with Qed.Guillaume Melquiond
Since the proofs start by applying or destructuring Qed-ed lemmas, they cannot be used in a computational setting, so no need for them to be Defined.
2021-02-19Merge PR #13865: [coqtop] be verbose only in interactive modecoqbot-app[bot]
Reviewed-by: silene Ack-by: SkySkimmer
2021-02-19Merge PR #13867: Fix missing arities of VM opcodes.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-02-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-02-17Add an entry to file critical-bugs.Guillaume Melquiond
2021-02-16Fix missing arities of VM opcodes.Guillaume Melquiond
Since the compiler initializes the arities to zero, coq_tcode_of_code wrongly believes that the word following a primitive operation contains an opcode, while it is the global index of the primitive operation. So, the function will try to translate it and thus corrupt it. But as long as the evaluated term fully reduces (which is always the case for CoqInterval), the corrupted word will never be read. At this point, it all depends on the arity of the global index (seen as an opcode). If it is zero, then coq_tcode_of_code will recover and correctly translate the following opcodes. If it is nonzero, then the function starts translating random words, possibly corrupting the memory past the end of the translation buffer. Independently of this memory corruption, coq_interprete will execute random code once it gets to the opcode following the primitive operation, since it has not been translated. The reason CoqInterval is not always crashing due to this bug is just plain luck. Indeed, the arity of the pseudo opcode only depends on the global index of the primitive operations. So, as long as this arity is zero, the memory corruption is fully contained. This happens in the vast majority of cases, since coq_tcode_of_code translates any unrecognized opcode to STOP, which has arity zero. This bug is exploitable.
2021-02-16Merge PR #13866: Only run windows job when WINDOWS=enabledcoqbot-app[bot]
Reviewed-by: Zimmi48
2021-02-16[coqtop] be verbose only in interactive modeEnrico Tassi
2021-02-16Only run windows job when WINDOWS=enabledGaëtan Gilbert
This seems to have been missed in https://github.com/coq/coq/pull/13598 (16cd0d5cfc0c4702b8220dad8e91f31a89d904ba)
2021-02-11Merge PR #13844: [vernac] pass the loc of the whole command to the interp ↵coqbot-app[bot]
function Reviewed-by: ejgallego
2021-02-11[ci] overlay for elpiEnrico Tassi
2021-02-11Merge PR #13640: Add ounit2 to with-test dependenciescoqbot-app[bot]
Reviewed-by: ejgallego
2021-02-11Merge PR #13642: Add build dependency of conf-python-3 to coq-doccoqbot-app[bot]
Reviewed-by: ejgallego
2021-02-11Merge PR #13823: Update release process following coq/ceps#52.coqbot-app[bot]
Reviewed-by: ejgallego Ack-by: gares
2021-02-11Merge PR #13831: Properly document the local and global locality attributes.coqbot-app[bot]
Reviewed-by: gares Reviewed-by: jfehrle Ack-by: SkySkimmer
2021-02-11[vernac] pass the loc of the whole command to the interp functionEnrico Tassi
2021-02-11Merge PR #13847: [ci] elpi 1.13.0coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-02-11overlay for coq-elpiEnrico Tassi
2021-02-11[ci] elpi 1.13.0Enrico Tassi
2021-02-11Merge PR #13826: [micromega] Fixes #13794Vincent Laporte
Reviewed-by: vbgl
2021-02-10Merge PR #13818: [bench] Re-enable coq-performance-testscoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-02-10Merge PR #13821: Properly handle ordering of -w and -native-compilercoqbot-app[bot]
Reviewed-by: gares
2021-02-10[micromega/nia] Improve sharing of proofsBESSON Frederic
Closes #13794
2021-02-09Merge PR #13822: Remove deprecated command line argumentscoqbot-app[bot]
Reviewed-by: gares
2021-02-09Merge PR #13810: ide: shift+enter to find backwardscoqbot-app[bot]
Reviewed-by: herbelin
2021-02-08Properly document the local and global locality attributes.Théo Zimmermann
2021-02-06Merge PR #13829: Fix hierarchy of sections in module chapter.coqbot-app[bot]
Reviewed-by: jfehrle
2021-02-05Fix hierarchy of sections in module chapter.Théo Zimmermann
2021-02-04Update release process following coq/ceps#52.Théo Zimmermann
2021-02-04Changelog for #13822Gaëtan Gilbert
2021-02-04Remove deprecated -inputstate command line argumentGaëtan Gilbert
Deprecated since 6dd9e003c289a79b0656e7c6f2cc59935997370c (2014)
2021-02-04Remove deprecated -sprop-cumulative command line argumentGaëtan Gilbert
Deprecated since #12034 (8.12)
2021-02-04Merge PR #13731: vernac/declaremods: make object collection tail-recursivecoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-02-04Properly handle ordering of -w and -native-compilerGaëtan Gilbert
Warnings are handled as injection commands, interleaved with options and requires. Native compiler impacts require, so we must convert "yes" to "no" before handling injections. As such the semantic handling of the native command line argument must be separated from the emission of the warning message, which this PR implements. Fix #13819 In principle the other 2 cwarning in coqargs (deprecated spropcumul and inputstate) should be moved to injections too, but since they're deprecated I can't be bothered.
2021-02-04Merge PR #13528: [RM] Script to list the contributors between two git revisionscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: gares
2021-02-04Use release branch instead of master.Théo Zimmermann
2021-02-03Merge PR #13817: CI: Switch coqhammer job to edge ocamlcoqbot-app[bot]
Reviewed-by: Zimmi48
2021-02-03Merge PR #13776: Fix #13739 - disable some warnings when calling Function.coqbot-app[bot]
Reviewed-by: gares Ack-by: Zimmi48 Ack-by: SkySkimmer
2021-02-03Fix #13739 - disable some warnings when calling Function.Pierre Courtieu
Also added a generic way of temporarily disabling a warning. Also added try_finalize un lib/utils.ml.
2021-02-03[bench] Re-enable coq-performance-testsJason Gross
Partial revert of 6f4c61d152ad801bd571088ab99eb276b0085a04. coq-performance-tests was fixed in https://github.com/coq-community/coq-performance-tests/commit/ae8385b9471409387d0f47f01e38b866ba70bda1. Note that the current state is not optimal, as the bench does not test the native compiler at all (see #13807).
2021-02-03CI: Switch coqhammer job to edge ocamlGaëtan Gilbert
This fixes CI from their using the Stdlib module.
2021-02-02Merge PR #13814: Add VST to the set of default bench packages.coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-02-02Add VST to the set of default bench packages.Pierre-Marie Pédrot
2021-02-02Merge PR #13805: Bench: remove broken packagesPierre-Marie Pédrot
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:02:18 +0000