Emilio Jesús Gallego Arias comments

Results 1528 comments of


                                            Emilio Jesús Gallego Arias

Add the primitive `catch_system` to the logic monad

Indeed this primitive is quite dangerous and in principle I gotta oppose it: people catching async exceptions will sooner or later do a mess and break the upper layer (that...

Add the primitive `catch_system` to the logic monad

I can see the case for timeout or other resource limits when writing a tactic that calls other tactics, my point that for these kind of limits, it is not...

Add the primitive `catch_system` to the logic monad

How about an API like this one: https://guillaume.munch.name/software/ocaml/memprof-limits/Memprof_limits/Masking/index.html#val-with_resource

Add the primitive `catch_system` to the logic monad

Regarding other points of your comment, they way you are handling the state is very hacky and won't work well in general, even `coqc` doesn't actually execute the file "sequentially"....

Fix artifacts for build:vio by merging build:vio and validate:vio

@coqbot run full CI

Fix artifacts for build:vio by merging build:vio and validate:vio

> Maybe we should just merge the jobs We can just remove `.vio` at all, as we discussed in the call. Given that vio files are quadratic in size, I...

Fix artifacts for build:vio by merging build:vio and validate:vio

I don't understand this issue, letting others take care of it.

Fix artifacts for build:vio by merging build:vio and validate:vio

Note that #18424 is also ready for merge.

[ci] Resurrect CI job for OCaml trunk.

Huhu test suite passed https://gitlab.com/coq/coq/-/jobs/1983005947

[ci] Resurrect CI job for OCaml trunk.

Getting some `SEGV` locally with 5.0.0-rc1 , and moreover I can't reproduce them properly :(