Can one implement an `Opaque`

-piercing `unfold`

tactic that does _not_ conflict with async proofs? As @Abhishek Anand pointed out to me recently, that'd let you use `Opaque`

as a less-broken `simpl never`

flag (e.g. one that actually deserves that name).

Today one can write the code below, but those commands break async proofs since they access mutable state. I'm aware of stdpp sealing but it requires `rewrite`

, which is sometimes too slow (and I suspect ssreflect does too).

```
Opaque foo. (* Coq's actual command for the `simpl never` functionality. *)
Lemma ...
Proof.
...
(* The `simpl never` usecase requires an unfolding option. *)
Local Transparent foo. unfold foo. Local Opaque foo.
...
Qed.
```

It just occurred to me that `with_strategy`

might be useful here: https://coq.github.io/doc/V8.13.2/refman/proofs/writing-proofs/rewriting.html#coq:tacn.with_strategy

Opaque doesn't have anything to do with async proofs afaik

@Gaëtan Gilbert global ^W non-proof local commands in proofs block async

since those affect later proofs, the async proof mechanism can't just "skip what's between Proof. and Qed.".

I'm not sure why the async engine can't "pull them out" and pretend it's dealing with

```
Transparent foo. Opaque foo.
Lemma ...
```

but then again, that sounds as hard as inferring a `Proof.`

command when missing (also an open challenge); maybe that's what the document manager is about (no clue?)

non-proof local commands in proofs block async

are you sure? when I do -vos on the following I get no error, which implies async worked

```
Lemma foo : False.
Proof.
Opaque id.
fail.
Qed.
```

the stm has a "replay" mechanism so side-effect commands are done twice (once in the proof, and once out of the proof before sending the term to the kernel IIRC)

so for instance if you do

```
Class XX := xx {}.
Lemma foo : True.
Proof.
Existing Instance xx.
exact I.
Qed.
```

you get the missing locality warning once at Existing Instance and again at Qed

uuh, thanks. I thought I had minimized this a while ago, but I can't reproduce it... and I do have a proof taking too long in vos, but something else might be the cause.

and `coqc -time -vos`

confirms — maybe I should use that to debug _where_ the problem starts:

```
$ coqc -time -vos test.v
Chars 0 - 26 [Set~Nested~Proofs~Allowed.] 0. secs (0.u,0.s)
Chars 0 - 21 [Lemma~foofoo~:~False.] 0.004 secs (0.u,0.002s)
Chars 22 - 28 [Proof.] 0. secs (0.u,0.s)
Chars 31 - 41 [Opaque~id.] 0. secs (0.u,0.s)
Chars 50 - 54 [Qed.] 0. secs (0.u,0.s)
```

Last updated: Jun 18 2024 at 09:02 UTC