forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
stm.ml
2741 lines (2460 loc) · 102 KB
/
stm.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
let prerr_endline s = if false then begin pr_err (s ()) end else ()
let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
open Vernacexpr
open Errors
open Pp
open Names
open Util
open Ppvernac
open Vernac_classifier
module Hooks = struct
let process_error, process_error_hook = Hook.make ()
let interp, interp_hook = Hook.make ()
let with_fail, with_fail_hook = Hook.make ()
let state_computed, state_computed_hook = Hook.make
~default:(fun state_id ~in_cache ->
feedback ~state_id Feedback.Processed) ()
let state_ready, state_ready_hook = Hook.make
~default:(fun state_id -> ()) ()
let forward_feedback, forward_feedback_hook = Hook.make
~default:(function
| { Feedback.id = Feedback.Edit edit_id; route; contents } ->
feedback ~edit_id ~route contents
| { Feedback.id = Feedback.State state_id; route; contents } ->
feedback ~state_id ~route contents) ()
let parse_error, parse_error_hook = Hook.make
~default:(function
| Feedback.Edit edit_id -> fun loc msg ->
feedback ~edit_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))
| Feedback.State state_id -> fun loc msg ->
feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
let execution_error, execution_error_hook = Hook.make
~default:(fun state_id loc msg ->
feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
let unreachable_state, unreachable_state_hook = Hook.make
~default:(fun _ _ -> ()) ()
let tactic_being_run, tactic_being_run_hook = Hook.make
~default:(fun _ -> ()) ()
include Hook
(* enables: Hooks.(call foo args) *)
let call = get
let call_process_error_once =
let processed : unit Exninfo.t = Exninfo.make () in
fun (_, info as ei) ->
match Exninfo.get info processed with
| Some _ -> ei
| None ->
let e, info = call process_error ei in
let info = Exninfo.add info processed () in
e, info
end
(* During interactive use we cache more states so that Undoing is fast *)
let interactive () =
if !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode then `Yes
else `No
let async_proofs_workers_extra_env = ref [||]
type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
let pr_ast { expr } = pr_vernac expr
(* Commands piercing opaque *)
let may_pierce_opaque = function
| { expr = VernacPrint (PrintName _) } -> true
| { expr = VernacExtend (("Extraction",_), _) } -> true
| { expr = VernacExtend (("SeparateExtraction",_), _) } -> true
| { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true
| { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true
| { expr = VernacExtend (("ExtractionConstant",_), _) } -> true
| { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true
| { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
| _ -> false
(* Wrapper for Vernacentries.interp to set the feedback id *)
let vernac_interp ?proof id ?route { verbose; loc; expr } =
let rec internal_command = function
| VernacResetName _ | VernacResetInitial | VernacBack _
| VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
| VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
| VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el
| _ -> false in
if internal_command expr then begin
prerr_endline (fun () -> "ignoring " ^ string_of_ppcmds(pr_vernac expr))
end else begin
set_id_for_feedback ?route (Feedback.State id);
Aux_file.record_in_aux_set_at loc;
prerr_endline (fun () -> "interpreting " ^ string_of_ppcmds(pr_vernac expr));
let a = Lexer.com_state () in
try
Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr));
Lexer.restore_com_state a
with e ->
let e = Errors.push e in
Lexer.restore_com_state a;
iraise Hooks.(call_process_error_once e)
end
(* Wrapper for Vernac.parse_sentence to set the feedback id *)
let vernac_parse ?newtip ?route eid s =
let feedback_id =
if Option.is_empty newtip then Feedback.Edit eid
else Feedback.State (Option.get newtip) in
set_id_for_feedback ?route feedback_id;
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
Flags.with_option Flags.we_are_parsing (fun () ->
try
match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
| None -> raise (Invalid_argument "vernac_parse")
| Some ast -> ast
with e when Errors.noncritical e ->
let (e, info) = Errors.push e in
let loc = Option.default Loc.ghost (Loc.get_loc info) in
Hooks.(call parse_error feedback_id loc (iprint (e, info)));
iraise (e, info))
()
let pr_open_cur_subgoals () =
try Printer.pr_open_subgoals ()
with Proof_global.NoCurrentProof -> str""
let update_global_env () =
if Proof_global.there_are_pending_proofs () then
Proof_global.update_global_env ()
module Vcs_ = Vcs.Make(Stateid)
type future_proof = Proof_global.closed_proof_output Future.computation
type proof_mode = string
type depth = int
type cancel_switch = bool ref
type branch_type =
[ `Master
| `Proof of proof_mode * depth
| `Edit of
proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ]
type cmd_t = {
ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
ceff : bool; (* is a side-effecting command *)
cast : ast;
cids : Id.t list;
cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] }
type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
type qed_t = {
qast : ast;
keep : vernac_qed_type;
mutable fproof : (future_proof * cancel_switch) option;
brname : Vcs_.Branch.t;
brinfo : branch_type Vcs_.branch_info
}
type seff_t = ast option
type alias_t = Stateid.t * ast
type transaction =
| Cmd of cmd_t
| Fork of fork_t
| Qed of qed_t
| Sideff of seff_t
| Alias of alias_t
| Noop
type step =
[ `Cmd of cmd_t
| `Fork of fork_t * Stateid.t option
| `Qed of qed_t * Stateid.t
| `Sideff of [ `Ast of ast * Stateid.t | `Id of Stateid.t ]
| `Alias of alias_t ]
type visit = { step : step; next : Stateid.t }
(* Parts of the system state that are morally part of the proof state *)
let summary_pstate = [ Evarutil.meta_counter_summary_name;
Evarutil.evar_counter_summary_name;
"program-tcc-table" ]
type state = {
system : States.state;
proof : Proof_global.state;
shallow : bool
}
type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
type backup = { mine : branch; others : branch list }
type 'vcs state_info = { (* Make private *)
mutable n_reached : int;
mutable n_goals : int;
mutable state : state option;
mutable vcs_backup : 'vcs option * backup option;
}
let default_info () =
{ n_reached = 0; n_goals = 0; state = None; vcs_backup = None,None }
(* Functions that work on a Vcs with a specific branch type *)
module Vcs_aux : sig
val proof_nesting : (branch_type, 't,'i) Vcs_.t -> int
val find_proof_at_depth :
(branch_type, 't, 'i) Vcs_.t -> int ->
Vcs_.Branch.t * branch_type Vcs_.branch_info
exception Expired
val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit
end = struct (* {{{ *)
let proof_nesting vcs =
List.fold_left max 0
(List.map_filter
(function
| { Vcs_.kind = `Proof (_,n) } -> Some n
| { Vcs_.kind = `Edit _ } -> Some 1
| _ -> None)
(List.map (Vcs_.get_branch vcs) (Vcs_.branches vcs)))
let find_proof_at_depth vcs pl =
try List.find (function
| _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
| _, { Vcs_.kind = `Edit _ } -> anomaly(str"find_proof_at_depth")
| _ -> false)
(List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
with Not_found -> failwith "find_proof_at_depth"
exception Expired
let visit vcs id =
if Stateid.equal id Stateid.initial then
anomaly(str"Visiting the initial state id")
else if Stateid.equal id Stateid.dummy then
anomaly(str"Visiting the dummy state id")
else
try
match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
| [n, Cmd x] -> { step = `Cmd x; next = n }
| [n, Alias x] -> { step = `Alias x; next = n }
| [n, Fork x] -> { step = `Fork (x,None); next = n }
| [n, Fork x; p, Noop] -> { step = `Fork (x,Some p); next = n }
| [p, Noop; n, Fork x] -> { step = `Fork (x,Some p); next = n }
| [n, Qed x; p, Noop]
| [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n }
| [n, Sideff None; p, Noop]
| [p, Noop; n, Sideff None]-> { step = `Sideff (`Id p); next = n }
| [n, Sideff (Some x); p, Noop]
| [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n }
| [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n}
| _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id))
with Not_found -> raise Expired
end (* }}} *)
(*************************** THE DOCUMENT *************************************)
(******************************************************************************)
(* Imperative wrap around VCS to obtain _the_ VCS that is the
* representation of the document Coq is currently processing *)
module VCS : sig
exception Expired
module Branch : (module type of Vcs_.Branch with type t = Vcs_.Branch.t)
type id = Stateid.t
type 'branch_type branch_info = 'branch_type Vcs_.branch_info = {
kind : [> `Master] as 'branch_type;
root : id;
pos : id;
}
type vcs = (branch_type, transaction, vcs state_info) Vcs_.t
val init : id -> unit
val current_branch : unit -> Branch.t
val checkout : Branch.t -> unit
val branches : unit -> Branch.t list
val get_branch : Branch.t -> branch_type branch_info
val get_branch_pos : Branch.t -> id
val new_node : ?id:Stateid.t -> unit -> id
val merge : id -> ours:transaction -> ?into:Branch.t -> Branch.t -> unit
val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit
val delete_branch : Branch.t -> unit
val commit : id -> transaction -> unit
val mk_branch_name : ast -> Branch.t
val edit_branch : Branch.t
val branch : ?root:id -> ?pos:id -> Branch.t -> branch_type -> unit
val reset_branch : Branch.t -> id -> unit
val reachable : id -> Vcs_.NodeSet.t
val cur_tip : unit -> id
val get_info : id -> vcs state_info
val reached : id -> bool -> unit
val goals : id -> int -> unit
val set_state : id -> state -> unit
val get_state : id -> state option
(* cuts from start -> stop, raising Expired if some nodes are not there *)
val slice : start:id -> stop:id -> vcs
val nodes_in_slice : start:id -> stop:id -> Stateid.t list
val create_cluster : id list -> qed:id -> start:id -> unit
val cluster_of : id -> (id * id) option
val delete_cluster_of : id -> unit
val proof_nesting : unit -> int
val checkout_shallowest_proof_branch : unit -> unit
val propagate_sideff : ast option -> unit
val gc : unit -> unit
val visit : id -> visit
val print : ?now:bool -> unit -> unit
val backup : unit -> vcs
val restore : vcs -> unit
end = struct (* {{{ *)
include Vcs_
exception Expired = Vcs_aux.Expired
module StateidSet = Set.Make(Stateid)
open Printf
let print_dag vcs () =
let fname =
"stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
let string_of_transaction = function
| Cmd { cast = t } | Fork (t, _,_,_) ->
(try string_of_ppcmds (pr_ast t) with _ -> "ERR")
| Sideff (Some t) ->
sprintf "Sideff(%s)"
(try string_of_ppcmds (pr_ast t) with _ -> "ERR")
| Sideff None -> "EnvChange"
| Noop -> " "
| Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
| Qed { qast } -> string_of_ppcmds (pr_ast qast) in
let is_green id =
match get_info vcs id with
| Some { state = Some _ } -> true
| _ -> false in
let is_red id =
match get_info vcs id with
| Some s -> Int.equal s.n_reached ~-1
| _ -> false in
let head = current_branch vcs in
let heads =
List.map (fun x -> x, (get_branch vcs x).pos) (branches vcs) in
let graph = dag vcs in
let quote s =
Str.global_replace (Str.regexp "\n") "<BR/>"
(Str.global_replace (Str.regexp "<") "<"
(Str.global_replace (Str.regexp ">") ">"
(Str.global_replace (Str.regexp "\"") """
(Str.global_replace (Str.regexp "&") "&"
(String.sub s 0 (min (String.length s) 20)))))) in
let fname_dot, fname_ps =
let f = "/tmp/" ^ Filename.basename fname in
f ^ ".dot", f ^ ".pdf" in
let node id = "s" ^ Stateid.to_string id in
let edge tr =
sprintf "<<FONT POINT-SIZE=\"12\" FACE=\"sans\">%s</FONT>>"
(quote (string_of_transaction tr)) in
let ids = ref StateidSet.empty in
let clus = Hashtbl.create 13 in
let node_info id =
match get_info vcs id with
| None -> ""
| Some info ->
sprintf "<<FONT POINT-SIZE=\"12\">%s</FONT>" (Stateid.to_string id) ^
sprintf " <FONT POINT-SIZE=\"11\">r:%d g:%d</FONT>>"
info.n_reached info.n_goals in
let color id =
if is_red id then "red" else if is_green id then "green" else "white" in
let nodefmt oc id =
fprintf oc "%s [label=%s,style=filled,fillcolor=%s];\n"
(node id) (node_info id) (color id) in
let add_to_clus_or_ids from cf =
match cf with
| None -> ids := StateidSet.add from !ids; false
| Some c -> Hashtbl.replace clus c
(try let n = Hashtbl.find clus c in from::n
with Not_found -> [from]); true in
let oc = open_out fname_dot in
output_string oc "digraph states {\n";
Dag.iter graph (fun from cf _ l ->
let c1 = add_to_clus_or_ids from cf in
List.iter (fun (dest, trans) ->
let c2 = add_to_clus_or_ids dest (Dag.cluster_of graph dest) in
fprintf oc "%s -> %s [xlabel=%s,labelfloat=%b];\n"
(node from) (node dest) (edge trans) (c1 && c2)) l
);
StateidSet.iter (nodefmt oc) !ids;
Hashtbl.iter (fun c nodes ->
fprintf oc "subgraph cluster_%s {\n" (Dag.Cluster.to_string c);
List.iter (nodefmt oc) nodes;
fprintf oc "color=blue; }\n"
) clus;
List.iteri (fun i (b,id) ->
let shape = if Branch.equal head b then "box3d" else "box" in
fprintf oc "b%d -> %s;\n" i (node id);
fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape
(Branch.to_string b);
) heads;
output_string oc "}\n";
close_out oc;
ignore(Sys.command
("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps))
type vcs = (branch_type, transaction, vcs state_info) t
let vcs : vcs ref = ref (empty Stateid.dummy)
let init id =
vcs := empty id;
vcs := set_info !vcs id (default_info ())
let current_branch () = current_branch !vcs
let checkout head = vcs := checkout !vcs head
let branches () = branches !vcs
let get_branch head = get_branch !vcs head
let get_branch_pos head = (get_branch head).pos
let new_node ?(id=Stateid.fresh ()) () =
assert(Vcs_.get_info !vcs id = None);
vcs := set_info !vcs id (default_info ());
id
let merge id ~ours ?into branch =
vcs := merge !vcs id ~ours ~theirs:Noop ?into branch
let delete_branch branch = vcs := delete_branch !vcs branch
let reset_branch branch id = vcs := reset_branch !vcs branch id
let commit id t = vcs := commit !vcs id t
let rewrite_merge id ~ours ~at branch =
vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
(match x with
| VernacDefinition (_,((_,i),_),_) -> string_of_id i
| VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> string_of_id i
| _ -> "branch")
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
let get_info id =
match get_info !vcs id with
| Some x -> x
| None -> raise Vcs_aux.Expired
let set_state id s =
(get_info id).state <- Some s;
if Flags.async_proofs_is_master () then Hooks.(call state_ready id)
let get_state id = (get_info id).state
let reached id b =
let info = get_info id in
if b then info.n_reached <- info.n_reached + 1
else info.n_reached <- -1
let goals id n = (get_info id).n_goals <- n
let cur_tip () = get_branch_pos (current_branch ())
let proof_nesting () = Vcs_aux.proof_nesting !vcs
let checkout_shallowest_proof_branch () =
if List.mem edit_branch (Vcs_.branches !vcs) then begin
checkout edit_branch;
match get_branch edit_branch with
| { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode
| _ -> assert false
end else
let pl = proof_nesting () in
try
let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
| h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
checkout branch;
prerr_endline (fun () -> "mode:" ^ mode);
Proof_global.activate_proof_mode mode
with Failure _ ->
checkout Branch.master;
Proof_global.disactivate_proof_mode "Classic"
(* copies the transaction on every open branch *)
let propagate_sideff t =
List.iter (fun b ->
checkout b;
let id = new_node () in
merge id ~ours:(Sideff t) ~into:b Branch.master)
(List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
let visit id = Vcs_aux.visit !vcs id
let nodes_in_slice ~start ~stop =
let rec aux id =
if Stateid.equal id start then [] else
match visit id with
| { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n
| { next = n; step = `Alias x } -> (id,Alias x) :: aux n
| { next = n; step = `Sideff (`Ast (x,_)) } ->
(id,Sideff (Some x)) :: aux n
| _ -> anomaly(str("Cannot slice from "^ Stateid.to_string start ^
" to "^Stateid.to_string stop))
in aux stop
let slice ~start ~stop =
let l = nodes_in_slice ~start ~stop in
let copy_info v id =
Vcs_.set_info v id
{ (get_info id) with state = None; vcs_backup = None,None } in
let copy_info_w_state v id =
Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in
let v = Vcs_.empty start in
let v = copy_info v start in
let v = List.fold_right (fun (id,tr) v ->
let v = Vcs_.commit v id tr in
let v = copy_info v id in
v) l v in
(* Stm should have reached the beginning of proof *)
assert (not (Option.is_empty (get_info start).state));
(* We put in the new dag the most recent state known to master *)
let rec fill id =
if (get_info id).state = None then fill (Vcs_aux.visit v id).next
else copy_info_w_state v id in
let v = fill stop in
(* We put in the new dag the first state (since Qed shall run on it,
* see check_task_aux) *)
copy_info_w_state v start
let nodes_in_slice ~start ~stop =
List.rev (List.map fst (nodes_in_slice ~start ~stop))
let create_cluster l ~qed ~start = vcs := create_cluster !vcs l (qed,start)
let cluster_of id = Option.map Dag.Cluster.data (cluster_of !vcs id)
let delete_cluster_of id =
Option.iter (fun x -> vcs := delete_cluster !vcs x) (Vcs_.cluster_of !vcs id)
let gc () =
let old_vcs = !vcs in
let new_vcs, erased_nodes = gc old_vcs in
Vcs_.NodeSet.iter (fun id ->
match (Vcs_aux.visit old_vcs id).step with
| `Qed ({ fproof = Some (_, cancel_switch) }, _)
| `Cmd { cqueue = `TacQueue cancel_switch }
| `Cmd { cqueue = `QueryQueue cancel_switch } ->
cancel_switch := true
| _ -> ())
erased_nodes;
vcs := new_vcs
module NB : sig (* Non blocking Sys.command *)
val command : now:bool -> (unit -> unit) -> unit
end = struct
let m = Mutex.create ()
let c = Condition.create ()
let job = ref None
let worker = ref None
let set_last_job j =
Mutex.lock m;
job := Some j;
Condition.signal c;
Mutex.unlock m
let get_last_job () =
Mutex.lock m;
while Option.is_empty !job do Condition.wait c m; done;
match !job with
| None -> assert false
| Some x -> job := None; Mutex.unlock m; x
let run_command () =
try while true do get_last_job () () done
with e -> () (* No failure *)
let command ~now job =
if now then job ()
else begin
set_last_job job;
if Option.is_empty !worker then
worker := Some (Thread.create run_command ())
end
end
let print ?(now=false) () =
if not !Flags.debug && not now then () else NB.command ~now (print_dag !vcs)
let backup () = !vcs
let restore v = vcs := v
end (* }}} *)
let state_of_id id =
try `Valid (VCS.get_info id).state
with VCS.Expired -> `Expired
(****** A cache: fills in the nodes of the VCS document with their value ******)
module State : sig
(** The function is from unit, so it uses the current state to define
a new one. I.e. one may been to install the right state before
defining a new one.
Warning: an optimization in installed_cached requires that state
modifying functions are always executed using this wrapper. *)
val define :
?safe_id:Stateid.t ->
?redefine:bool -> ?cache:Summary.marshallable ->
?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
val fix_exn_ref : (iexn -> iexn) ref
val install_cached : Stateid.t -> unit
val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn
(* to send states across worker/master *)
type frozen_state
val get_cached : Stateid.t -> frozen_state
val same_env : frozen_state -> frozen_state -> bool
type proof_part
type partial_state =
[ `Full of frozen_state
| `Proof of Stateid.t * proof_part ]
val proof_part_of_frozen : frozen_state -> proof_part
val assign : Stateid.t -> partial_state -> unit
end = struct (* {{{ *)
(* cur_id holds Stateid.dummy in case the last attempt to define a state
* failed, so the global state may contain garbage *)
let cur_id = ref Stateid.dummy
let fix_exn_ref = ref (fun x -> x)
(* helpers *)
let freeze_global_state marshallable =
{ system = States.freeze ~marshallable;
proof = Proof_global.freeze ~marshallable;
shallow = (marshallable = `Shallow) }
let unfreeze_global_state { system; proof } =
States.unfreeze system; Proof_global.unfreeze proof
(* hack to make futures functional *)
let in_t, out_t = Dyn.create "state4future"
let () = Future.set_freeze
(fun () -> in_t (freeze_global_state `No, !cur_id))
(fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
type frozen_state = state
type proof_part =
Proof_global.state * Summary.frozen_bits (* only meta counters *)
type partial_state =
[ `Full of frozen_state
| `Proof of Stateid.t * proof_part ]
let proof_part_of_frozen { proof; system } =
proof,
Summary.project_summary (States.summary_of_state system) summary_pstate
let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable)
let is_cached ?(cache=`No) id =
if Stateid.equal id !cur_id then
try match VCS.get_info id with
| { state = None } when cache = `Yes -> freeze `No id; true
| { state = None } when cache = `Shallow -> freeze `Shallow id; true
| _ -> true
with VCS.Expired -> false
else
try match VCS.get_info id with
| { state = Some _ } -> true
| _ -> false
with VCS.Expired -> false
let install_cached id =
if Stateid.equal id !cur_id then () else (* optimization *)
let s =
match VCS.get_info id with
| { state = Some s } -> s
| _ -> anomaly (str "unfreezing a non existing state") in
unfreeze_global_state s; cur_id := id
let get_cached id =
try match VCS.get_info id with
| { state = Some s } -> s
| _ -> anomaly (str "not a cached state")
with VCS.Expired -> anomaly (str "not a cached state (expired)")
let assign id what =
if VCS.get_state id <> None then () else
try match what with
| `Full s ->
let s =
try
let prev = (VCS.visit id).next in
if is_cached prev
then { s with proof =
Proof_global.copy_terminators
~src:(get_cached prev).proof ~tgt:s.proof }
else s
with VCS.Expired -> s in
VCS.set_state id s
| `Proof(ontop,(pstate,counters)) ->
if is_cached ontop then
let s = get_cached ontop in
let s = { s with proof =
Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
let s = { s with system =
States.replace_summary s.system
(Summary.surgery_summary
(States.summary_of_state s.system)
counters) } in
VCS.set_state id s
with VCS.Expired -> ()
let exn_on id ?valid (e, info) =
match Stateid.get info with
| Some _ -> (e, info)
| None ->
let loc = Option.default Loc.ghost (Loc.get_loc info) in
let (e, info) = Hooks.(call_process_error_once (e, info)) in
Hooks.(call execution_error id loc (iprint (e, info)));
(e, Stateid.add info ?valid id)
let same_env { system = s1 } { system = s2 } =
let s1 = States.summary_of_state s1 in
let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in
let s2 = States.summary_of_state s2 in
let e2 = Summary.project_summary s2 [Global.global_env_summary_name] in
Summary.pointer_equal e1 e2
let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
f id
=
feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id);
let str_id = Stateid.to_string id in
if is_cached id && not redefine then
anomaly (str"defining state "++str str_id++str" twice");
try
prerr_endline (fun () -> "defining "^str_id^" (cache="^
if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
let good_id = match safe_id with None -> !cur_id | Some id -> id in
fix_exn_ref := exn_on id ~valid:good_id;
f ();
fix_exn_ref := (fun x -> x);
if cache = `Yes then freeze `No id
else if cache = `Shallow then freeze `Shallow id;
prerr_endline (fun () -> "setting cur id to "^str_id);
cur_id := id;
if feedback_processed then
Hooks.(call state_computed id ~in_cache:false);
VCS.reached id true;
if Proof_global.there_are_pending_proofs () then
VCS.goals id (Proof_global.get_open_goals ())
with e ->
let (e, info) = Errors.push e in
let good_id = !cur_id in
cur_id := Stateid.dummy;
VCS.reached id false;
Hooks.(call unreachable_state id (e, info));
match Stateid.get info, safe_id with
| None, None -> iraise (exn_on id ~valid:good_id (e, info))
| None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info))
| Some _, None -> iraise (e, info)
| Some (_,at), Some id -> iraise (e, Stateid.add info ~valid:id at)
end (* }}} *)
(****************************** CRUFT *****************************************)
(******************************************************************************)
(* The backtrack module simulates the classic behavior of a linear document *)
module Backtrack : sig
val record : unit -> unit
val backto : Stateid.t -> unit
val back_safe : unit -> unit
(* we could navigate the dag, but this ways easy *)
val branches_of : Stateid.t -> backup
(* To be installed during initialization *)
val undo_vernac_classifier : vernac_expr -> vernac_classification
end = struct (* {{{ *)
let record () =
List.iter (fun current_branch ->
let mine = current_branch, VCS.get_branch current_branch in
let info = VCS.get_info (VCS.get_branch_pos current_branch) in
let others =
CList.map_filter (fun b ->
if Vcs_.Branch.equal b current_branch then None
else Some(b, VCS.get_branch b)) (VCS.branches ()) in
let backup = if fst info.vcs_backup <> None then fst info.vcs_backup
else Some (VCS.backup ()) in
let branches = if snd info.vcs_backup <> None then snd info.vcs_backup
else Some { mine; others } in
info.vcs_backup <- backup, branches)
[VCS.current_branch (); VCS.Branch.master]
let backto oid =
let info = VCS.get_info oid in
match info.vcs_backup with
| None, _ ->
anomaly(str"Backtrack.backto "++str(Stateid.to_string oid)++
str": a state with no vcs_backup")
| Some vcs, _ -> VCS.restore vcs
let branches_of id =
let info = VCS.get_info id in
match info.vcs_backup with
| _, None ->
anomaly(str"Backtrack.branches_of "++str(Stateid.to_string id)++
str": a state with no vcs_backup")
| _, Some x -> x
let rec fold_until f acc id =
let next acc =
if id = Stateid.initial then raise Not_found
else fold_until f acc (VCS.visit id).next in
let info = VCS.get_info id in
match info.vcs_backup with
| None, _ -> next acc
| Some vcs, _ ->
let ids, tactic, undo =
if id = Stateid.initial || id = Stateid.dummy then [],false,0 else
match VCS.visit id with
| { step = `Fork ((_,_,_,l),_) } -> l, false,0
| { step = `Cmd { cids = l; ctac } } -> l, ctac,0
| { step = `Alias (_,{ expr = VernacUndo n}) } -> [], false, n
| _ -> [],false,0 in
match f acc (id, vcs, ids, tactic, undo) with
| `Stop x -> x
| `Cont acc -> next acc
let back_safe () =
let id =
fold_until (fun n (id,_,_,_,_) ->
if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n))
0 (VCS.get_branch_pos (VCS.current_branch ())) in
backto id
let undo_vernac_classifier v =
try
match v with
| VernacResetInitial ->
VtStm (VtBack Stateid.initial, true), VtNow
| VernacResetName (_,name) ->
msg_warning
(str"Reset not implemented for automatically generated constants");
let id = VCS.get_branch_pos (VCS.current_branch ()) in
(try
let oid =
fold_until (fun b (id,_,label,_,_) ->
if b then `Stop id else `Cont (List.mem name label))
false id in
VtStm (VtBack oid, true), VtNow
with Not_found ->
VtStm (VtBack id, true), VtNow)
| VernacBack n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
VtStm (VtBack oid, true), VtNow
| VernacUndo n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,tactic,undo) ->
let value = (if tactic then 1 else 0) - undo in
if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
VtStm (VtBack oid, true), VtLater
| VernacUndoTo _
| VernacRestart as e ->
let m = match e with VernacUndoTo m -> m | _ -> 0 in
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let vcs =
match (VCS.get_info id).vcs_backup with
| None, _ -> anomaly(str"Backtrack: tip with no vcs_backup")
| Some vcs, _ -> vcs in
let cb, _ =
try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs)
with Failure _ -> raise Proof_global.NoCurrentProof in
let n = fold_until (fun n (_,vcs,_,_,_) ->
if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
0 id in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
VtStm (VtBack oid, true), VtLater
| VernacAbortAll ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun () (id,vcs,_,_,_) ->
match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
() id in
VtStm (VtBack oid, true), VtLater
| VernacBacktrack (id,_,_)
| VernacBackTo id ->
VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
| _ -> VtUnknown, VtNow
with
| Not_found ->
msg_warning(str"undo_vernac_classifier: going back to the initial state.");
VtStm (VtBack Stateid.initial, true), VtNow
end (* }}} *)
let hints = ref Aux_file.empty_aux_file
let set_compilation_hints file =
hints := Aux_file.load_aux_file_for file
let get_hint_ctx loc =
let s = Aux_file.get !hints loc "context_used" in
match Str.split (Str.regexp ";") s with
| ids :: _ ->
let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
let ids = List.map (fun id -> Loc.ghost, id) ids in
begin match ids with
| [] -> SsEmpty
| x :: xs ->
List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
end
| _ -> raise Not_found
let get_hint_bp_time proof_name =
try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
with Not_found -> 1.0
let record_pb_time proof_name loc time =
let proof_build_time = Printf.sprintf "%.3f" time in
Aux_file.record_in_aux_at loc "proof_build_time" proof_build_time;
if proof_name <> "" then begin
Aux_file.record_in_aux_at Loc.ghost proof_name proof_build_time;
hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time
end
exception RemoteException of std_ppcmds
let _ = Errors.register_handler (function
| RemoteException ppcmd -> ppcmd
| _ -> raise Unhandled)
(****************************** THE SCHEDULER *********************************)
(******************************************************************************)
module rec ProofTask : sig
type competence = Stateid.t list
type task_build_proof = {
t_exn_info : Stateid.t * Stateid.t;
t_start : Stateid.t;
t_stop : Stateid.t;
t_drop : bool;
t_states : competence;
t_assign : Proof_global.closed_proof_output Future.assignement -> unit;
t_loc : Loc.t;
t_uuid : Future.UUID.t;
t_name : string }
type task =
| BuildProof of task_build_proof
| States of Stateid.t list
type request =
| ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence
| ReqStates of Stateid.t list
include AsyncTaskQueue.Task
with type task := task
and type competence := competence
and type request := request
val build_proof_here :
drop_pt:bool ->
Stateid.t * Stateid.t -> Loc.t -> Stateid.t ->
Proof_global.closed_proof_output Future.computation
(* If set, only tasks overlapping with this list are processed *)
val set_perspective : Stateid.t list -> unit
end = struct (* {{{ *)
let forward_feedback msg = Hooks.(call forward_feedback msg)
type competence = Stateid.t list
type task_build_proof = {
t_exn_info : Stateid.t * Stateid.t;
t_start : Stateid.t;
t_stop : Stateid.t;
t_drop : bool;
t_states : competence;
t_assign : Proof_global.closed_proof_output Future.assignement -> unit;