| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-10-22 | Micro-optimization in Control.check_for_interrupt. | Pierre-Marie Pédrot | |
| We do not have to increase the step counter when out of the threaded mode since this counter is only relevant when in that mode. | |||
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann | |
| Add headers to a few files which were missing them. | |||
| 2020-03-08 | [exn] [nit] Remove not very useful re-raises. | Emilio Jesus Gallego Arias | |
| Cleanup: IMHO most of the re-raises here are not worth it. | |||
| 2020-01-15 | [ocaml] Remove Custom Backtrace module in favor of OCaml's | Emilio 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 ... ``` | |||
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann | |
| 2019-04-03 | Protect some I/O routines from SIGALRM | Maxime Dénès | |
| This is necessary to prevent Coq from sending ill-formed output in some scenarios involving `Timeout`. Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr> | |||
| 2019-01-22 | [thread] protect threads against sigalrm | Enrico Tassi | |
| This makes the implementation of Timeout on unix more reliable since only the main thread will receive the signal for timeout. | |||
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-05-07 | [lib] Re-add `set_timeout` to help users workaround #7408 | Emilio Jesus Gallego Arias | |
| It seems like #7408 will need some potentially intrusive work, so let's add the low-level hook back so third party developments can work well with `8.8.1/master` for the moment. | |||
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2017-12-11 | [flags] [stm] Reorganize flags. | Emilio Jesus Gallego Arias | |
| We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag. | |||
| 2017-11-24 | [lib] Generalize Control.timeout type. | Emilio Jesus Gallego Arias | |
| We also remove some internal implementation details from the mli file, there due historical reasons. | |||
| 2017-07-21 | PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it. | Maxime Dénès | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | |
| Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads. | |||
| 2014-08-05 | STM: code restructured to reuse task queue for tactics | Enrico Tassi | |
| 2014-07-10 | check_for_interrupt: better (but slower) in threading mode | Enrico Tassi | |
| Experimenting with PIDE I discovered that yield is not sufficient to have a rescheduling, hence the delay. | |||
| 2014-06-21 | Less ocaml warnings. | Hugo Herbelin | |
| 2014-06-08 | Timeout implementation for Windows based on threads. | Pierre-Marie Pédrot | |
| 2014-06-07 | Moving a Thread.yield in check_interrupt. | Pierre-Marie Pédrot | |
| 2014-06-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |