aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-01-16Merge PR #11400: Use the GTK completion widget in CoqIDEEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-01-16Adding a changelog.Pierre-Marie Pédrot
2020-01-16Adding an option to change the autocompletion delay.Pierre-Marie Pédrot
2020-01-16Better handling of asynchronous completion.Pierre-Marie Pédrot
2020-01-16Hacking a completion widget based on the default GtkSourceView one.Pierre-Marie Pédrot
2020-01-16Move the per-architecture check of marshalled Uint63s to Values.Pierre-Marie Pédrot
2020-01-16Checker validation acts on object representations rather than objects.Pierre-Marie Pédrot
2020-01-16Code factorization in checker validation.Pierre-Marie Pédrot
2020-01-16[mltop] Remove error handling hacks in favor of default methods.Emilio Jesus Gallego Arias
We don't need to handle `Dynlink` errors specially anymore.
2020-01-16[mltop] Store digest of modules used to compile files.Emilio Jesus Gallego Arias
This should allow digest-based builds to work correctly. Fixes #10874 For now, we store the digest of the module selected, this means that vo files loading modules will have different digests depending on whether the `native` or `byte` version was used. If that is a problem we can improve this tho; for example we could disable the digest in those cases. The code could be better, and indeed `Mltop` could enjoy a nice cleanup, I will likely do some when I add support for `Fl_dynload`.
2020-01-15Merge PR #11373: Close #11168Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-15Merge PR #11374: Close #11133Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-15[ocaml] Remove Custom Backtrace module in favor of OCaml'sEmilio Jesus Gallego Arias
As suggested by Pierre-Marie Pédrot, this is a more conservative version of #8771 . In this commit, we replace Coq's custom backtrace type with OCaml `Printexc.raw_backtrace`; this seems to already give some improvements in terms of backtraces [see below] and removes quite a bit of code. Main difference in terms of API is that backtraces become now first-class in `Exninfo`, and we seek to consolidate thus the exception-related APIs in that module. We also fix a bug in `vernac.ml` where the backtrace captured was the one of `edit_at`. Closes #6446 Example with backtrace from https://github.com/coq/coq/issues/11366 Old: ``` raise @ file "stdlib.ml", line 33, characters 17-33 frame @ file "pretyping/coercion.ml", line 406, characters 24-68 frame @ file "list.ml", line 117, characters 24-34 frame @ file "pretyping/coercion.ml", line 393, characters 4-1004 frame @ file "pretyping/coercion.ml", line 450, characters 12-40 raise @ unknown frame @ file "pretyping/coercion.ml", line 464, characters 6-46 raise @ unknown frame @ file "pretyping/pretyping.ml", line 839, characters 33-95 frame @ file "pretyping/pretyping.ml", line 875, characters 50-94 frame @ file "pretyping/pretyping.ml", line 1280, characters 2-81 frame @ file "pretyping/pretyping.ml", line 1342, characters 20-71 frame @ file "vernac/vernacentries.ml", line 1579, characters 17-48 frame @ file "vernac/vernacentries.ml", line 2215, characters 8-49 frame @ file "vernac/vernacinterp.ml", line 45, characters 4-13 ... ``` New: ``` Raised at file "stdlib.ml", line 33, characters 17-33 Called from file "pretyping/coercion.ml", line 406, characters 24-68 Called from file "list.ml", line 117, characters 24-34 Called from file "pretyping/coercion.ml", line 393, characters 4-1004 Called from file "pretyping/coercion.ml", line 450, characters 12-40 Called from file "pretyping/coercion.ml", line 464, characters 6-46 Called from file "pretyping/pretyping.ml", line 839, characters 33-95 Called from file "pretyping/pretyping.ml", line 875, characters 50-94 Called from file "pretyping/pretyping.ml" (inlined), line 1280, characters 2-81 Called from file "pretyping/pretyping.ml", line 1294, characters 21-94 Called from file "pretyping/pretyping.ml", line 1342, characters 20-71 Called from file "vernac/vernacentries.ml", line 1579, characters 17-48 Called from file "vernac/vernacentries.ml", line 2215, characters 8-49 Called from file "vernac/vernacinterp.ml", line 45, characters 4-13 ... ```
2020-01-15Discharge inductive types without rechecking themGaëtan Gilbert
2020-01-15generate variance data for section universes (not yet used)Gaëtan Gilbert
preparation for direct discharge
2020-01-15Merge PR #11401: [nix] Dune-2 and other improvementsThéo Zimmermann
2020-01-15[Nix] Fix setup hook when COQPATH is not boundVincent Laporte
2020-01-15[Nix] Update reference to nixpkgsVincent Laporte
This brings dune at version 2.1.2
2020-01-15[Nix/CI] Add verdi-raftVincent Laporte
2020-01-15[Nix/CI] Update fiat_cryptoVincent Laporte
2020-01-14Merge PR #11370: [zify] elim let in MLPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-14Merge PR #11249: [stdlib] Additional statements in List.vHugo Herbelin
Reviewed-by: anton-trunov Reviewed-by: herbelin
2020-01-14Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with ↵Hugo Herbelin
decorations Ack-by: Zimmi48 Reviewed-by: herbelin
2020-01-14[zify] elim let in MLFrédéric Besson
2020-01-14infercumulativity: take less argumentsGaëtan Gilbert
2020-01-14Merge PR #11392: Document the Set Default Proof Mode command.Théo Zimmermann
Reviewed-by: Zimmi48
2020-01-14[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorationsKarl Palmskog
2020-01-14Document the Set Default Proof Mode command.Pierre-Marie Pédrot
Fixes #10909: Set Default Proof Mode is not documented.
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to ↵Kazuhiko Sakaguchi
OCaml's string type Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: herbelin Ack-by: maximedenes Reviewed-by: pi8027
2020-01-13Merge PR #11081: Native compute: cleanup temporary files on program exitPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
We make a temporary directory for these files and cleanup at process exit. The temporary directory means we don't have to guess what extensions ocaml will produce, we can just delete everything there. We use Lazy to avoid spamming unused directories when ahead-of-time compiling without actually using native casts / nativenorm (typically stdlib files). Sadly ocaml has "create temp file" but not "create temp dir", so we have to copy the name generation code. Fix #10495
2020-01-13Merge PR #11285: fix #11279. Specialize h no longer expands letins in the ↵Pierre-Marie Pédrot
type of h. Reviewed-by: ppedrot
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio ↵Pierre-Marie Pédrot
(and not just… Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
The type of h is reconstructed to look as much as the initial type of h as possible.
2020-01-11Merge PR #11367: Minor cleanup of indtypes/indtypingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-11Merge PR #11349: [refman] [changelog] Announce omega replacement.Pierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: maximedenes
2020-01-10Merge PR #11387: [refman] missing space in "Controlling the locality of ↵Théo Zimmermann
commands" Reviewed-by: Zimmi48
2020-01-10Merge PR #11385: Add badges for Docker Hub and coqorg/coq:latest versionThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-10missing spaceOlivier Laurent
2020-01-10Merge PR #11384: Fix build after merge of #11164Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-09Merge PR #11371: [merge script] Never bypass outdated branch sanity check.Jason Gross
Reviewed-by: JasonGross
2020-01-09Add badges for Docker Hub and coqorg/coq:latest versionErik Martin-Dorel
2020-01-09Fix build after merge of #11164Gaëtan Gilbert
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: ppedrot
2020-01-08Merge PR #11375: Add note about default goal selector next to bullet docsThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-08Merge PR #11378: let CI test bedrock2's 'tested' branch instead of 'master'Théo Zimmermann
Reviewed-by: Zimmi48
2020-01-08Add Set NativeCompute TimingJason Gross
The command `Set NativeCompute Timing` causes calls to `native_compute` (as well as kernel calls to the native compiler) to emit separate timing information about compilation, execution, and reification. This allows more fine-grained timing of the native compiler without needing to set the `-debug` flag.
2020-01-08let CI test bedrock2's 'tested' branch instead of 'master'Samuel Gruetter
2020-01-08Add note about default goal selector next to bullet docsGaëtan Gilbert
Close #11036
2020-01-08Add changelog entry for native string extractionMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-04 22:54:10 +0000