coq/stm · co/coq

JJason Grossstm: report a lost master connection without matching strerror text

文件	最后提交记录	最后更新时间
asyncTaskQueue.ml	stm: report a lost master connection without matching strerror text Matching the text of system error messages is unreliable: on Windows FormatMessage translates them according to the system UI language, so the guard would not fire on a non-English machine. Instead the worker now lets Sys_error through its own marshal wrappers, which are not used by the master, and treats End_of_file and Sys_error alike in the main loop as the master having gone away.	1 个月前
asyncTaskQueue.mli	Rename coqide -> rocqide	1 年前
dag.ml	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
dag.mli	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
dune	Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode.	4 个月前
partac.ml	Align Evd and UState API names eg Evd.new_quality_variable was equivalent to UState.new_sort_variable, and Evd.new_sort_variable combined new_quality and new_univ (fixed by renaming the UState API to match Evd) also renamed Evd.merge_universe_context -> merge_ustate for clarity	7 个月前
partac.mli	Do not base asyncTaskQueue spawn arguments directly on Sys.argv Instead we generate the needed arguments from the parsed Coqargs and stm args. As workers do not do certain operations like Require and get their state from the parent process's summary this turns out to be very few arguments (unless I made a mistake).	1 年前
proofBlockDelimiter.ml	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
proofBlockDelimiter.mli	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
spawned.ml	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
spawned.mli	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
stm.ml	Reimplement abstract in a purely functional way. This patch replaces the infamous mutable modification of the global safe environment in the abstract tactic by a purely functional mechanism. This changes some of the hidden invariants and makes it a non-trivial change likely to uncover some subtle issues in the implementation. I tried to make it as lenient as possible as a first pass, we will try to sanitize the downstream clients later on. The main change is that an environment alone is not enough to make sense of constants from terms living in the tactic layer. Local constants defined by abstract are not part of the environment but should rather be obtained through the evarmap. Note that this is actually somewhat innocuous API-wise, since the EConstr API has been precisely designed to always require an evarmap around. The only changes are indirect callers to lookup_constant, which must now be given an evarmap. A more subtle change is the precise relation between the global and tactic environments. An explicit design choice is that between vernacular commands, the global environment does contain the abstracted constants. For this to work, we need a two-tiered side-effect tracking. The first tier is provided by the evarmap, which only contains the local constants that have been generated by the current tactic invocation. The second tier is implemented in the Declare mechanism, where we track all private constants defined by the previous tactic calls in the current proof in order to replay them when closing it.	10 个月前
stm.mli	Rename Coq -> Rocq in various comments and doc Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> Co-authored-by: Guillaume Melquiond <guillaume.melquiond@inria.fr>	1 年前
stmargs.ml	Stop catching async exceptions in hacks that catch anomalies Typically the reductionops "Tried to normalize ill-typed term" hack deliberately catches anomalies (including those from CErrors.anomaly) but shouldn't catch async exceptions. Hopefully fixes the non working Fail Timeout in bedrock2, we could also revert #21216 for our own test suite. (debugging tip: apply ~~~diff @@ -32,7 +32,14 @@ let check_for_interrupt () = (* This function assumes it is the only function calling [setitimer] ) let unix_timeout n f x = let open Unix in - let timeout_handler _ = raise Timeout in + let timeout_handler _ = + let info = Exninfo.reify () in + let () = + Exninfo.get_backtrace info \|> Option.iter @@ fun bt -> + Printf.eprintf "timeout at %s\n%!" (Exninfo.backtrace_to_string bt) + in + raise Timeout + in let old_timer = getitimer ITIMER_REAL in ( Here we assume that the existing timer will also interrupt us. *) if old_timer.it_value > 0. && old_timer.it_value <= n then Ok (f x) else ~~~ then run a buggy Timeout with `Set Debug "backtrace"` on until you get the bug, the function which catches the timeout exn should be in the printed backtrace. For instance I had ~~~ Called from Reductionops.infer_conv_gen in file "pretyping/reductionops.ml", line 1324, characters 10-52 ~~~ when trying the Fail Timeout in bedrock2 LeakageSemantics.)	10 个月前
stmargs.mli	Do not base asyncTaskQueue spawn arguments directly on Sys.argv Instead we generate the needed arguments from the parsed Coqargs and stm args. As workers do not do certain operations like Require and get their state from the parent process's summary this turns out to be very few arguments (unless I made a mistake).	1 年前
tQueue.ml	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
tQueue.mli	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
vcs.ml	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
vcs.mli	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
workerPool.ml	Handle most unused-field warnings The warning is locally disabled when the record is meant to be the result of some marshalling. There are a couple cases where I disabled the warning even though the field could probably be deleted, in particular zify (too many cases to want to bother) and some stm stuff with threads (not 100% sure we can delete those fields).	8 个月前
workerPool.mli	Do not base asyncTaskQueue spawn arguments directly on Sys.argv Instead we generate the needed arguments from the parsed Coqargs and stm args. As workers do not do certain operations like Require and get their state from the parent process's summary this turns out to be very few arguments (unless I made a mistake).	1 年前