aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
This has been in the TODO queue for a long time, and indeed I have recently seen some trouble with users passing two .v files to Coq, which it isn't a) tested, b) supported. Moreover, it doesn't even work correctly in 8.13 due to some other changes in the toplevel related to auxiliary files. (*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
2021-02-26Merge PR #13884: CI Windows: adjust branch name to Coq Platform branch renamingcoqbot-app[bot]
Reviewed-by: gares
2021-02-26Merge PR #13883: Expose Top_printers.econstr_displaycoqbot-app[bot]
Reviewed-by: ejgallego
2021-02-26CI Windows: adjust branch name to Coq Platform branch renamingMichael Soegtrop
2021-02-26Expose Top_printers.econstr_displayGaëtan Gilbert
2021-02-26Merge PR #13869: Use make_case_or_project in auto_ind_declPierre-Marie Pédrot
Reviewed-by: ppedrot
2021-02-26Merge PR #13676: Protect caml_process_pending_actions_exn with ↵Pierre-Marie Pédrot
caml_something_to_do. Reviewed-by: gasche Ack-by: ppedrot Reviewed-by: xavierleroy
2021-02-26Merge PR #13868: Make genOpcodeFiles.ml handle opcode arity.Pierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: gares Reviewed-by: ppedrot
2021-02-25Merge PR #13393: [proof using] Remove duplicate code, refactor.coqbot-app[bot]
Reviewed-by: gares Ack-by: SkySkimmer
2021-02-25[proof using] Remove duplicate code, refactor.Emilio Jesus Gallego Arias
PR #13183 introduced quite a bit of duplicate code, we refactor it and expose less internals on the way. That should make the API more robust.
2021-02-25Merge PR #13202: Infrastructure for fine-grained debug flagscoqbot-app[bot]
Reviewed-by: gares Ack-by: herbelin Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer Ack-by: ejgallego
2021-02-25Merge PR #13863: Get rid of the compilation date from the binaries to make ↵coqbot-app[bot]
them more stable. Reviewed-by: SkySkimmer Reviewed-by: gares
2021-02-25Merge PR #13080: Ascii: add leb and ltbcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-02-25Merge PR #13738: Make sure Ltac2 get cleaned too.coqbot-app[bot]
Reviewed-by: gares
2021-02-24Overlay for Set DebugGaëtan Gilbert
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-19Be less permissive with respect to nonsensical bytecode.Guillaume Melquiond
2021-02-19Make the generated file the official source of arity.Guillaume Melquiond
2021-02-19Add a file coq_arity.h generated by genOpcodeFiles.ml.Guillaume Melquiond
This avoids forgetting to add opcodes to coq_fix_code.c, and thus prevents arities being mistakenly set to zero.
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-17Use make_case_or_project in auto_ind_declGaëtan Gilbert
Towards #5154 (but insufficient)
2021-02-17Reduce imperative arrays in build_beq_scheme + reindentGaëtan Gilbert
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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 11:22:41 +0000