Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

itp_communication.ml 3.65 KB
Newer Older
Sylvain Dailler's avatar
Sylvain Dailler committed
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
(* Information that the IDE may want to have *)
type prover = string
type transformation = string
type strategy = string


type node_ID = int
let root_node : node_ID = 0


type global_information =
    {
     provers         : prover list;
     transformations : transformation list;
     strategies      : strategy list;
     commands        : string list;
     (* hidden_provers       : string list; *)
     (* session_time_limit   : int; *)
     (* session_mem_limit    : int; *)
     (* session_nb_processes : int; *)
     (* session_cntexample   : bool; *)
     (* main_dir             : string *)
    }

type message_notification =
  | Proof_error           of node_ID * string
  | Transf_error          of node_ID * string
  | Strat_error           of node_ID * string
  | Replay_Info           of string
  | Query_Info            of node_ID * string
  | Query_Error           of node_ID * string
  | Help                  of string
  | Information           of string
  | Task_Monitor          of int * int * int
35
  | Parse_Or_Type_Error   of string
36
  | File_Saved            of string
Sylvain Dailler's avatar
Sylvain Dailler committed
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53
  | Error                 of string
  | Open_File_Error       of string

type node_type =
  | NRoot
  | NFile
  | NTheory
  | NTransformation
  | NGoal
  | NProofAttempt

type update_info =
  | Proved of bool
  | Proof_status_change of
      Controller_itp.proof_attempt_status
      * bool   (* obsolete or not *)
      * Call_provers.resource_limit
54
  | Obsolete of bool
Sylvain Dailler's avatar
Sylvain Dailler committed
55 56 57 58 59 60 61 62 63

type notification =
  | New_node     of node_ID * node_ID * node_type * string * bool
  (* Notification of creation of new_node:
     New_node (new_node, parent_node, node_type, name, detached). *)
  | Node_change  of node_ID * update_info
  (* inform that the data of the given node changed *)
  | Remove       of node_ID
  (* the given node was removed *)
64 65 66
  | Next_Unproven_Node_Id of node_ID * node_ID
  (* Next_Unproven_Node_Id (asked_id, next_unproved_id). Returns a node and the
     next unproven node from this node *)
Sylvain Dailler's avatar
Sylvain Dailler committed
67 68 69 70 71 72 73 74 75 76
  | Initialized  of global_information
  (* initial global data *)
  | Saved
  (* the session was saved on disk *)
  | Message      of message_notification
  (* an informative message, can be an error message *)
  | Dead         of string
  (* server exited *)
  | Task         of node_ID * string
  (* the node_ID's task *)
77
  | File_contents of string * string
78
  (* File_contents (filename, contents) *)
Sylvain Dailler's avatar
Sylvain Dailler committed
79 80

type ide_request =
81 82 83 84 85 86 87 88 89 90 91 92
  | Command_req             of node_ID * string
  | Prove_req               of node_ID * prover * Call_provers.resource_limit
  | Transform_req           of node_ID * transformation * string list
  | Strategy_req            of node_ID * strategy
  | Open_session_req        of string
  | Add_file_req            of string
  | Set_max_tasks_req       of int
  | Get_file_contents       of string
  | Get_task                of node_ID
  | Remove_subtree          of node_ID
  | Copy_paste              of node_ID * node_ID
  | Copy_detached           of node_ID
93
  | Save_file_req           of string * string
94
  | Get_first_unproven_node of node_ID
95
  | Mark_obsolete_req       of node_ID
Sylvain Dailler's avatar
Sylvain Dailler committed
96
  | Get_Session_Tree_req
97
  | Clean_req
Sylvain Dailler's avatar
Sylvain Dailler committed
98 99 100 101
  | Save_req
  | Reload_req
  | Replay_req
  | Exit_req
102
  | Interrupt_req
103 104 105 106 107 108

(* Return true if the request modify the session *)
let modify_session (r: ide_request) =
  match r with
  | Command_req _ | Prove_req _ | Transform_req _ | Strategy_req _
  | Add_file_req _ | Remove_subtree _ | Copy_paste _ | Copy_detached _
109
  | Replay_req | Clean_req | Mark_obsolete_req _ -> true
110 111 112 113 114

  | Open_session_req _ | Set_max_tasks_req _ | Get_file_contents _
  | Get_task _ | Save_file_req _ | Get_first_unproven_node _
  | Get_Session_Tree_req | Save_req | Reload_req | Exit_req
  | Interrupt_req -> false