From b755869a7fdb34dcf7dacc9d5fd93c768d71d751 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Mar 2020 02:26:43 -0400 Subject: [proof] Split delayed and regular proof closing functions, part II We make the types of the delayed / non-delayed declaration path different, as the latter is just creating futures that are forced right away. TTBOMK the new code should behave identically w.r.t. old one, modulo the equation `Future.(force (from_val x)) = x`. There are some questions as what the code is doing, but in this PR I've opted to keep the code 100% faithful to the original one, unless I did a mistake. --- stm/stm.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 62556d38ff..ba8eba0eed 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1668,7 +1668,7 @@ end = struct (* {{{ *) (* The original terminator, a hook, has not been saved in the .vio*) let proof, _info = - PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in + PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in let info = Lemmas.Info.make () in @@ -2518,9 +2518,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent | VtKeepAxiom -> assert false in - Some(PG_compat.close_proof ~opaque - ~keep_body_ucst_separate:false - (State.exn_on id ~valid:eop)) in + try Some (PG_compat.close_proof ~opaque ~keep_body_ucst_separate:false) + with exn -> + let iexn = Exninfo.capture exn in + Exninfo.iraise (State.exn_on id ~valid:eop iexn) + in if keep <> VtKeep VtKeepAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in -- cgit v1.2.3 From e9c05828bba7ceb696a5c17457b8e0826bbd94f1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Mar 2020 02:45:47 -0400 Subject: [proof] Split return_proof in partial and regular versions. This is a small refactoring as these two functions behave very differently and the invariants are quite different, in fact regular `return_proof` should not be exported but be part of close proof, but there is small use in the STM still. --- stm/stm.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index ba8eba0eed..c1156b9afe 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1501,7 +1501,7 @@ end = struct (* {{{ *) let wall_clock2 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); - let p = PG_compat.return_proof ~allow_partial:drop_pt () in + let p = if drop_pt then PG_compat.return_partial_proof () else PG_compat.return_proof () in if drop_pt then feedback ~id Complete; p) @@ -1661,7 +1661,7 @@ end = struct (* {{{ *) try Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop; if drop then - let _proof = PG_compat.return_proof ~allow_partial:true () in + let _proof = PG_compat.return_partial_proof () in `OK_ADMITTED else begin let opaque = Proof_global.Opaque in -- cgit v1.2.3 From 0eadf776ba78dcfdcab842f38f5de871ed337376 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Mar 2020 17:04:16 -0400 Subject: [proof] [stm] Force `opaque` in `close_future_proof` Following an observation by Enrico Tassi, we remove the `opaque` parameter from `close_future_proof`, it should never be called with transparent constants. We will enforce this thru typing at the proof layer soon. --- stm/stm.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index c1156b9afe..5b88ee3d68 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1522,15 +1522,15 @@ end = struct (* {{{ *) let st = State.freeze () in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> - let opaque = Proof_global.Opaque in (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; let pobject, _info = - PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in + PG_compat.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let st = Vernacstate.freeze_interp_state ~marshallable:false in + let opaque = Proof_global.Opaque in stm_qed_delay_proof ~st ~id:stop ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in ignore(Future.join checked_proof); @@ -2479,13 +2479,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ~drop_pt exn_info block_stop, ref false in qed.fproof <- Some (Some fp, cancel); - let opaque = match keep' with - | VtKeepAxiom | VtKeepOpaque -> - Proof_global.Opaque (* Admitted -> Opaque should be OK. *) - | VtKeepDefined -> Proof_global.Transparent + let () = match keep' with + | VtKeepAxiom | VtKeepOpaque -> () + | VtKeepDefined -> + CErrors.anomaly (Pp.str "Cannot delegate transparent proofs, this is a bug in the STM.") in let proof, info = - PG_compat.close_future_proof ~opaque ~feedback_id:id fp in + PG_compat.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state ~marshallable:false in -- cgit v1.2.3