Pierre-Marie Pédrot (Sep 22 2021 at 12:10): 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.
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.
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.
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.
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.
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.
Enrico Tassi (Sep 22 2021 at 12:14):vernacstate is functional/sync-with-undo
Pierre-Marie Pédrot (Sep 22 2021 at 12:14):yes and no, we do modify state imperatively from there.
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.
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.
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.
this fails because at the level of the Print, the subproof is not properly declared;
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
Enrico Tassi (Sep 22 2021 at 12:17):hum, let me checkout the branch
Pierre-Marie Pédrot (Sep 22 2021 at 12:17):so, somewhere after the Defined is performed.
Pierre-Marie Pédrot (Sep 22 2021 at 12:18):the relevant changes are in vernac/, everything else is kernel-related and pure
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.
Pierre-Marie Pédrot (Sep 22 2021 at 12:21):so the culprit is somehow VernacState.unfreeze_interp_state
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
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.
Pierre-Marie Pédrot (Sep 22 2021 at 12:42)::white_flag:
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)
Pierre-Marie Pédrot (Sep 22 2021 at 12:48):No, because it must be backtracked upon when going back.
Enrico Tassi (Sep 22 2021 at 12:48):No need if you use a weak map
Pierre-Marie Pédrot (Sep 22 2021 at 12:48):That's a hack IMO.
Pierre-Marie Pédrot (Sep 22 2021 at 12:49):We already have leaking issues due to the VM with this design pattern.
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
Pierre-Marie Pédrot (Sep 22 2021 at 12:49):And actually, it won't work.
Pierre-Marie Pédrot (Sep 22 2021 at 12:49):You need to know what to export at the end of the session.
Enrico Tassi (Sep 22 2021 at 12:50):it's in the env (the revstructu of the current library)
Pierre-Marie Pédrot (Sep 22 2021 at 12:50):A weak map could be an overapproximation if backtrack happens.
Enrico Tassi (Sep 22 2021 at 12:50):you collect the gensyms from that, and query the table
Pierre-Marie Pédrot (Sep 22 2021 at 12:50):This looks horrible to me.
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.
Enrico Tassi (Sep 22 2021 at 12:51):eh eh, you are granted permission to dislike ;-)
Enrico Tassi (Sep 22 2021 at 12:51):so let me see the undo thing
Pierre-Marie Pédrot (Sep 22 2021 at 12:51):ah, wait a sec;
Pierre-Marie Pédrot (Sep 22 2021 at 12:51):I think I solved at least part of the problem.
Pierre-Marie Pédrot (Sep 22 2021 at 12:52):I had a suspicious piece of code resetting the opaque table between Qeds
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
Pierre-Marie Pédrot (Sep 22 2021 at 12:53):but removing it makes my bug go away
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)
Enrico Tassi (Sep 22 2021 at 12:54):where is it?
Pierre-Marie Pédrot (Sep 22 2021 at 12:55):in stm.ml line 2268
Pierre-Marie Pédrot (Sep 22 2021 at 12:55):and a bit above
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
Enrico Tassi (Sep 22 2021 at 12:58):that code makes little sense given what you are trying to do
Pierre-Marie Pédrot (Sep 22 2021 at 12:58):that I gather
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
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
Enrico Tassi (Sep 22 2021 at 12:59):well, if the term is opaque they are inlined
Enrico Tassi (Sep 22 2021 at 13:00):so they are in the env
Enrico Tassi (Sep 22 2021 at 13:00):but here you Defined
Pierre-Marie Pédrot (Sep 22 2021 at 13:00):the problem here is specifically with Defined
Pierre-Marie Pédrot (Sep 22 2021 at 13:00):test-suite is running let's see what happens
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 ...
Enrico Tassi (Sep 22 2021 at 13:04):it's neither qed not delayed...
Pierre-Marie Pédrot (Sep 22 2021 at 13:05):the branch does not touch this part of the code though
Pierre-Marie Pédrot (Sep 22 2021 at 13:05):it's already like that in master
Pierre-Marie Pédrot (Sep 22 2021 at 13:09):test-suite still broken but for unrelated reasons
Pierre-Marie Pédrot (Sep 22 2021 at 13:09):"it's a miracle" ©
Pierre-Marie Pédrot (Sep 22 2021 at 13:10):OK, thanks anyways and sorry for bothering you for nothing :/
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.
Pierre-Marie Pédrot (Sep 23 2021 at 10:02):in a nutshell, I am not sure what its specifications are.
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.
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
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.
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.
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.
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
Pierre-Marie Pédrot (Sep 23 2021 at 10:08):what do?
Pierre-Marie Pédrot (Sep 23 2021 at 10:09):cc @Emilio Jesús Gallego Arias as well
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)
Emilio Jesús Gallego Arias (Sep 23 2021 at 10:30):I'd say that joining morally is more like forcing a "lazy"
Emilio Jesús Gallego Arias (Sep 23 2021 at 10:30):so it doesn't introduce a new node
Emilio Jesús Gallego Arias (Sep 23 2021 at 10:30):but updates the state of a node
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
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
Emilio Jesús Gallego Arias (Sep 23 2021 at 10:34):@Gaëtan Gilbert good point, can the work done in join be reused?
Pierre-Marie Pédrot (Sep 23 2021 at 11:12):@Gaëtan Gilbert currently it's neither if I read the code correctly
Pierre-Marie Pédrot (Sep 23 2021 at 11:13):it's an in-place modification that is invisible in the STM
Emilio Jesús Gallego Arias (Sep 23 2021 at 11:18):Indeed @Pierre-Marie Pédrot , IIRC , it is just forcing the futures, right?
Emilio Jesús Gallego Arias (Sep 23 2021 at 11:19):Tho a message is emitted by the kernel for IDEs
Emilio Jesús Gallego Arias (Sep 23 2021 at 11:19):that's how the color changes, correct?
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
Enrico Tassi (Sep 23 2021 at 12:07):I would not add a node to the stm dag to represent this operation, frankly.
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)?
Pierre-Marie Pédrot (Sep 23 2021 at 12:19):yes that's basically the design
Pierre-Marie Pédrot (Sep 23 2021 at 12:19):so you claim we never stored the final constraints anywhere ?
Pierre-Marie Pédrot (Sep 23 2021 at 12:19):this looks weird to me
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)
Enrico Tassi (Sep 23 2021 at 12:24):no, they are in the .vo
Enrico Tassi (Sep 23 2021 at 12:25):if you do .vio -> .vo these constraints are in a dedicated segment
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
Pierre-Marie Pédrot (Sep 23 2021 at 12:26):no, I agree that they are in the vo
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
Enrico Tassi (Sep 23 2021 at 12:26):in CoqIDE, no, the safe_env would be dropped I believe
Enrico Tassi (Sep 23 2021 at 12:27):yes
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
Pierre-Marie Pédrot (Sep 23 2021 at 12:27):even when the proofs are not gray
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)
Pierre-Marie Pédrot (Sep 23 2021 at 12:27):indeed
Pierre-Marie Pédrot (Sep 23 2021 at 12:28):so this confirms my original suspicion then
Pierre-Marie Pédrot (Sep 23 2021 at 12:29):fine then
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
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.
Pierre-Marie Pédrot (Sep 23 2021 at 12:34):yes, but we could still store it into the VCS
Enrico Tassi (Sep 23 2021 at 12:34):not as a node, yes
Pierre-Marie Pédrot (Sep 23 2021 at 12:34):as a write barrier, even if it's not written in the document
Enrico Tassi (Sep 23 2021 at 12:34):ok
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).
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: Nov 29 2023 at 04:01 UTC