Skip to content

Notes on side effects, universes and proof closing

Gaëtan Gilbert edited this page Oct 14, 2019 · 2 revisions

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.

Clone this wiki locally
You can’t perform that action at this time.