Emilio Jesús Gallego Arias

By the way, I'd swear that I witnessed a race condition just now: somehow, after an observe that triggered async checking, a worker produced a spurious error! Interesting!

Thanks for the report @palmskog , note the comment of @kit-ty-kate here too: https://github.com/ocaml/opam-repository/pull/15850#discussion_r380142221 > Apparently opam does not support !pinned (but does pinned): > [ERROR] undefined filter variable in...

The error seems to have evolved in the latest release, we now just get Coq not installed in OPAM's CI due to the package being pinned? https://github.com/ocaml/opam-repository/pull/17070#issuecomment-681732257

It is indeed a big pain, I tried to have `cmdliner` to parse that, but I didn't manage to hack a solution where `cmdliner` would take the arguments in this...

> the second sentence results in one proof goal I think you are "counting" the sentences wrong. IIRC bullets are considered as sentences on their own, thus you will have:...

> I changed the printing format to "X Y" where X is the number of goals and Y is the size of the stack, and "- -" if there is...

As discussed today, the problem here is the ```ocaml let ndoc = { Stm.doc_type = Stm.VoDoc in_file ``` in `sercomp.ml`, in particular `VoDoc` does disable immediate caching of proof states...

@palmskog , should this go into the 8.10 release? I think we can test the goals mode and use the `Vio` type.

> I will experiment with this for a day or so and then we can make the final decision. Sounds good, you already have quite a lot of machinery in...

@palmskog any updates on this? Would postponing for 0.7.1 be a problem for you folks?