aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-23Print anomaly labels regardless of -debug, and never print user_err labelsGaëtan Gilbert
2021-02-23Merge PR #13880: Fix the release process checklist with respect to the ↵coqbot-app[bot]
refman update. Reviewed-by: ejgallego
2021-02-22Fix the release process checklist with respect to the refman update.Théo Zimmermann
2021-02-22Merge PR #13878: [RM] Changelog for 8.13.1coqbot-app[bot]
Reviewed-by: Zimmi48
2021-02-22Merge PR #13836: Make detyping more resistent in the debuggerPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-02-22Merge PR #13828: Fix doc comment in pp.mlicoqbot-app[bot]
Reviewed-by: ejgallego
2021-02-22mention --version to CoqIDEEnrico Tassi
2021-02-22Merge PR #13872: Make lemmas from Reals opaque whenever possible.coqbot-app[bot]
Reviewed-by: thery
2021-02-22Merge PR #13870: Add option --version to Coqide (fix #13752).coqbot-app[bot]
Reviewed-by: gares
2021-02-22changelog for 8.13.1Enrico Tassi
2021-02-20Merge PR #13874: add changelog for #13867 (Fix missing arities of VM opcodes)coqbot-app[bot]
Reviewed-by: jfehrle
2021-02-20Update doc/changelog/01-kernel/13867-changelog-for-13867.rstEnrico Tassi
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-02-20add changelog for 13867Enrico Tassi
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-17Add option --version to Coqide (fix #13752).Guillaume Melquiond
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-15Fix doc comment in pp.mliGaëtan Gilbert
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-08Make detyping more resistent in the debuggerGaëtan Gilbert
2021-02-06Merge PR #13829: Fix hierarchy of sections in module chapter.coqbot-app[bot]
Reviewed-by: jfehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:10:10 +0000