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/

db.mli 2.93 KB
Newer Older
MARCHE Claude's avatar
db  
MARCHE Claude 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 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
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(** Proof database *)

(** {1 data types} *)

(** prover info *)
type prover

val prover_from_id : string -> prover

(** status of an external proof attempt *)
type proof_status =
  | Success (** external proof attempt succeeded *)
  | Timeout (** external proof attempt was interrupted *)
  | Unknown (** external prover answered ``don't know'' or equivalent *)
  | Failure (** external prover call failed *)

type proof_attempt 
type goal
type transf
type theory
type file
type goal_parent =
  | Theory of theory
  | Transf of transf

(** proof_attempt accessors *)
val prover : proof_attempt -> prover
val proof_goal : proof_attempt -> goal
val status : proof_attempt -> proof_status
val proof_obsolete : proof_attempt -> bool
val time : proof_attempt -> float
val edited_as : proof_attempt -> string


(** goal accessors *)
val parent : goal -> goal_parent
val task : goal -> string (* checksum *)
val proved : goal -> bool
val external_proofs: (string, proof_attempt) Hashtbl.t
val transformations : (string, transf) Hashtbl.t

(** transf accessors *)
val parent_goal : transf -> goal
val transf_name : transf -> string
val subgoals : transf -> goal list

(** theory accessors *)        
val theory_name : theory -> string
val goals : theory -> goal list
val verified : theory -> bool

(** file accessors *)
val file_name : file -> string
val theories : file -> theory list

(** {1 The persistent database} *)

val init_base : string -> unit
(** opens or creates the current database, from given file name *)

val files : unit -> file list
(** returns the current set of files *)



(** {1 Updates} *)