Stream: Coq devs & plugin devs

Topic: STM and summary


view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:10):

I'm currently struggling to make https://github.com/ppedrot/coq/tree/move-opaque-out-of-kernel work properly, and to this end I am summoning our local STM gurus.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:11):

For the unaware, this PR moves the computation of delayed proofs outside of the kernel.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:11):

In particular there is now a table in vernac/opaques that is used to store what was before part of the safe env.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:12):

I had to store it in the vernacstate because it does not follow a standard summary behaviour.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:12):

Essentially it's global, i.e. it's never backtracked upon when exiting sections / closing modules.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:13):

Now the problem is that somewhere along the way it gets reset to an old state that is not correct, leading to opaque proofs not being properly stored into the vo file.

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:14):

vernacstate is functional/sync-with-undo

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:14):

yes and no, we do modify state imperatively from there.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:14):

the problem is not so much imperative vs. functional, it's that the STM manipulates the state and I don't know where.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:15):

I've been trying to printf debug the trace of the STM, but this is getting over my head.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:16):

a minimal failing example with my PR:

Definition foo : True.
Proof.
abstract exact I.
Defined.

Print foo_subproof.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:16):

this fails because at the level of the Print, the subproof is not properly declared;

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:17):

yet, it is globally registered in Declare at the same time as the call to export_private_constants

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:17):

hum, let me checkout the branch

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:17):

so, somewhere after the Defined is performed.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:18):

the relevant changes are in vernac/, everything else is kernel-related and pure

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:19):

We now have a global imperative table in vernac/opaques that is kept in sync in the vernacstate in the same way as the other imperative states.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:21):

so the culprit is somehow VernacState.unfreeze_interp_state

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:22):

but I don't understand why it reinstates the correct global env, but not the correct opaque map

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:25):

in particular, in my trace debug on master, summary unfreezing sets the wrong env after Defined but magically the environment becomes correct at some point.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:42):

:white_flag:

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:47):

I'm not sure I follow you idea. To me the opaque_table should not be freezed/unfreezed. Why do you do that? (also, we don't need to send it to workers, so I don't see why it is part of the vernac state.

I think you want a gensym and weak map, and let the GC of ocaml do all the work (if one undoes and makes an opaque proof garbage)

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:48):

No, because it must be backtracked upon when going back.

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:48):

No need if you use a weak map

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:48):

That's a hack IMO.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:49):

We already have leaking issues due to the VM with this design pattern.

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:49):

well, let me check at your code, but IMO a weak map is just the right data structure

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:49):

And actually, it won't work.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:49):

You need to know what to export at the end of the session.

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:50):

it's in the env (the revstructu of the current library)

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:50):

A weak map could be an overapproximation if backtrack happens.

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:50):

you collect the gensyms from that, and query the table

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:50):

This looks horrible to me.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:51):

I want a purely functional API, not yet another pile of mutable state thrown into the mix.

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:51):

eh eh, you are granted permission to dislike ;-)

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:51):

so let me see the undo thing

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:51):

ah, wait a sec;

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:51):

I think I solved at least part of the problem.

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:52):

I had a suspicious piece of code resetting the opaque table between Qeds

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:53):

I am pretty sure I was not the one who wrote this because this is stuff I have no idea about

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:53):

but removing it makes my bug go away

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:53):

(might well be the case it will pop up somewhere else in another guise, let's see)

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:54):

where is it?

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:55):

in stm.ml line 2268

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:55):

and a bit above

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:56):

not that I want to find a culprit, but I think I had a vague recollection of either you or @Emilio Jesús Gallego Arias guiding me to write this snippet

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:58):

that code makes little sense given what you are trying to do

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:58):

that I gather

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:58):

it's unclear what the invariants for Qed are and they might have changed between the first iteration of this PR and now

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 12:59):

looks like it was designed for a system where the private constants are kept inside the env

view this post on Zulip Enrico Tassi (Sep 22 2021 at 12:59):

well, if the term is opaque they are inlined

view this post on Zulip Enrico Tassi (Sep 22 2021 at 13:00):

so they are in the env

view this post on Zulip Enrico Tassi (Sep 22 2021 at 13:00):

but here you Defined

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 13:00):

the problem here is specifically with Defined

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 13:00):

test-suite is running let's see what happens

view this post on Zulip Enrico Tassi (Sep 22 2021 at 13:01):

anyway, something is fishy with that branch. It is the sync one, and we call stm_qed_delay_proof ...

view this post on Zulip Enrico Tassi (Sep 22 2021 at 13:04):

it's neither qed not delayed...

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 13:05):

the branch does not touch this part of the code though

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 13:05):

it's already like that in master

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 13:09):

test-suite still broken but for unrelated reasons

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 13:09):

"it's a miracle" ©

view this post on Zulip Pierre-Marie Pédrot (Sep 22 2021 at 13:10):

OK, thanks anyways and sorry for bothering you for nothing :/

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:02):

I've made some progress since yesterday, and while the first patch in the PR is functional, I am now hitting issues with the join command of the STM.

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:02):

in a nutshell, I am not sure what its specifications are.

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:03):

the last commit of the PR splits the "kernel join" operation into first checking a proof, which produces a certificate (essentially a proof term + constraints + a nonce) and then adding this into the environment.

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:04):

now the STM join needs to be aware of the synchronization between the kernel env and the stm opaque table, but something is amiss

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:06):

when joining, the kernel proof is forced (this is good), it is filled (i.e. constraints are added), but then the STM decides to overwrite the opaque table with the old one.

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:06):

that means that there is a mismatch since the kernel believes the proofs are forced, but the opaque table does not.

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:06):

it actually highlight the dubious spec of the join operation, since it lives "outside" of a state.

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:07):

joining changes the global state, i.e. it should introduce a node in the document, but the STM seems to just forget about that

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:08):

what do?

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:09):

cc @Emilio Jesús Gallego Arias as well

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 10:09):

(I have pushed the latest version on my branch if you guys want to have a look)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 10:30):

I'd say that joining morally is more like forcing a "lazy"

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 10:30):

so it doesn't introduce a new node

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 10:30):

but updates the state of a node

view this post on Zulip Gaëtan Gilbert (Sep 23 2021 at 10:33):

it depends on if you want the univ constraints to be in the env after joining
if no then join is a query
if yes then it does update the state

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 10:33):

how to hack that in the current state of affairs, maybe update the node data type so you can mark a node as joined

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 10:34):

@Gaëtan Gilbert good point, can the work done in join be reused?

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 11:12):

@Gaëtan Gilbert currently it's neither if I read the code correctly

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 11:13):

it's an in-place modification that is invisible in the STM

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 11:18):

Indeed @Pierre-Marie Pédrot , IIRC , it is just forcing the futures, right?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 11:19):

Tho a message is emitted by the kernel for IDEs

view this post on Zulip Emilio Jesús Gallego Arias (Sep 23 2021 at 11:19):

that's how the color changes, correct?

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:06):

One detail about universes is that the safe_env contains a list of lazy constraints (which are part of the thunks of lazy proofs).
IIRC join does forces the proofs, then also forces the list and adds all constraints to the env in order to check they are still satisfiable, but does not produce a new env and store it somewhere. IIRC, it has been a long time.

If you join twice, the thunks are not recomputed, but I think the univ are checkd again

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:07):

I would not add a node to the stm dag to represent this operation, frankly.

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:08):

@Pierre-Marie Pédrot did you touch that list of lazy constraints? Did you move it outside and put a list of ids pointing to the opaque proof (constraints)?

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:19):

yes that's basically the design

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:19):

so you claim we never stored the final constraints anywhere ?

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:19):

this looks weird to me

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:20):

(I've adapted the PR to emulate what was happening before but this looks very wrong)

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:24):

no, they are in the .vo

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:25):

if you do .vio -> .vo these constraints are in a dedicated segment

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:26):

if you do .v -> .vo I think we join (outside the stm, it was in the coqc driver) and then save the library using the global, updated, safe_env

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:26):

no, I agree that they are in the vo

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:26):

I mean that in interactive use we never really get access to the complete env

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:26):

in CoqIDE, no, the safe_env would be dropped I believe

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:27):

yes

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:27):

yeah so except if you mash the "force kernel proofs" button every second you can't be sure you're actually safe

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:27):

even when the proofs are not gray

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:27):

well, if you are at the end of the document and you click it, then you are (until you add one more proof)

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:27):

indeed

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:28):

so this confirms my original suspicion then

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:29):

fine then

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:30):

the new API somehow forces you to realize that something is not fully checked, I guess we could reflect that in the GUI

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:33):

if we had a source format:

theory foo
  imports
body

end

we could put it in the end, but we have no such a thing so...
It is a bit like the checks for modules/sections/proofs which are not closed, there is no natural syntactic element to put the error on.

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:34):

yes, but we could still store it into the VCS

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:34):

not as a node, yes

view this post on Zulip Pierre-Marie Pédrot (Sep 23 2021 at 12:34):

as a write barrier, even if it's not written in the document

view this post on Zulip Enrico Tassi (Sep 23 2021 at 12:34):

ok

view this post on Zulip Hugo Herbelin (Sep 25 2021 at 07:17):

While talking about the STM, does anyone has an explanation or even a solution to the troubling exn_on-related double printing of errors, with the second time sometimes in the wrong environment (see #5479 and a couple of related issues).

view this post on Zulip Emilio Jesús Gallego Arias (Sep 26 2021 at 18:50):

I'm afraid Hugo that fixing that would require a deep reworking of the internals.


Last updated: Oct 21 2021 at 21:03 UTC