Notes on side effects, universes and proof closing - coq/coq GitHub Wiki

In the hope of someday figuring out how to avoid universe double declarations and maybe even simplify close_proof.

NB: this is using https://github.com/coq/coq/pull/10863 otherwise the universe state is even more complicated since we have to consider the seff_univs in the ustate separately

Consider a monomorphic constant with a side effect:

Set Printing Universes.
Lemma foo : Type(*u*).
Proof.
  abstract (exact Type(*v, v < u*)).
  (* abstract declares foo_subproof with u,v |= v < u. u is removed from foo's ustate *)
Qed.
(**
We look at Proof_global.close_proof and Declare.add_constant for foo
(the subproof is always the same and boring as explained above)

##### Defined any mode, or Qed normal mode (coqc, coqtop)

Proof_global.close_proof: we have poly=false, now=true, keep_body_ucst_separate=false
Because there are side effects we are in the allow_deferred=true branch

return ({u},typ),((body,{} |= v < u),eff)
NB: if side_effects didn't put us in allow_deferred=true,
    we would declare no typ univs which is broken in the Qed case

- if Defined:
  Declare.ml calls export_private_constants (declare side effects (u,v |= u < v declared))
  Declare.ml calls add_constant (def entry has no seff)
  Term_typing: locally add typ univs {u} (double declaration!)
  check typ, check body
  Safe_typing: add_field: add typ univs {u} (double declaration!)
  done
- if Qed:
  Declare.ml calls add_constant
  Safe_typing: add_constant
    Term_typing:
      locally add typ univs {u}
      check typ
      handle (inline) side effects -> add side effect univs to body univs
      locally add body univs {u,v} |= v < u (double declaration for u!)
      check body (skipping inlined seff)
      save updated body univs in PrivateMonomorphic
    add_field: add typ univs {u}
    peek on body: it's forced:
      add updated body univs {u,v} |= v < u (double declaration for u!)

##### Qed -async mode (coqide, coqc -async-proofs on)

close_proof with yet-to-do proof: now=false, keep_body_ucst_separate=true
(from stm.ml closse_future_proof in reach `Qed branch)
now=false -> delayed body branch
return ({u},typ),future ((body,{} |= v < u), eff)
Safe_typing add_constant:
  Term_typing:
    locally add typ univs {u}
    check typ
    wait for body
  add_field: add typ univs {u}
  peek on body: Later

whenever the proof finishes: (this is in the worker)
  close_future_proof from stm.ml perform_buildp:
    now=false, keep_body_ucst_separate=true, future is from_val
    now=false so delayed branch of close_proof same as above
  still perform_buildp:
    we do the add_constant round with a forced future -> just like the normal mode

on join (coqide button, coqc -async)
Global.join() joins the futures from the original add_constant

kernel sees the same stuff as normal mode, but delayed body and an extra time in the worker

double check to get early errors, see aeb5daa2efdb2d0f2c75670e11d409f24528c54a

##### Qed vio and vio2vo mode

coqc -quick step:
delayed close_proof and Safe_typing.add_constant as -async mode, but the future will never run
save the proof closure separately in the .vio

vio2vo step:
close_proof from stm.ml check_task_aux with now=true, keep_body_ucst_separate=true
because there are side effects this is the same as the normal mode close_proof
send to kernel (sees the same as normal mode, all forced)
grab body and body univs from opaque table to save in vo
*)

Things to understand:

• what is the 3rd branch of close_proof for (case (poly && not opaque) || (now && not keep_body_ucst_separate && no side effects)), the poly && not opaque part is relatively clear but why is it needed for monomorphics? Maybe related to https://github.com/coq/coq/issues/10890
• why can't we replace the allow_deferred branch with the really delayed branch?

It may be useful to write up what happens when we do exact Type. without abstract ie no side effect case.