package why3find

  1. Overview
  2. Docs

Source file meta.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the why3find.                                    *)
(*                                                                        *)
(*  Copyright (C) 2022-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It 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.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the enclosed LICENSE.md for details.                              *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- META Package Infos                                                 --- *)
(* -------------------------------------------------------------------------- *)

type pkg = {
  name: string ;
  path: string ;
  depends: string list ;
  drivers: string list ;
  extracted: bool ;
}

(* -------------------------------------------------------------------------- *)
(* --- Package Lookup                                                     --- *)
(* -------------------------------------------------------------------------- *)

let path pkg =
  match Global.Sites.packages with
  | local::_ -> Filename.concat local pkg
  | [] -> failwith "Installation site not found"

let find pkg =
  let rec lookup pkg = function
    | [] -> Utils.failwith "Package '%s' not found" pkg
    | d::ds ->
      let path = Filename.concat d pkg in
      if not @@ Sys.file_exists path then lookup pkg ds else
        let meta = Filename.concat path "META.json" in
        if Sys.file_exists meta then
          let open Json in
          let js = of_file meta in
          if jfield "configs" js |> jstringlist <> [] then
            Log.warning "Support for extra config files was removed in \
                         why3find 1.1.0.@ If you need this feature, please \
                         report this at https://git.frama-c.com/pub/why3find/issues.";
          let depends = jfield "depends" js |> jstringlist in
          let drivers = jfield "drivers" js |> jstringlist in
          let extracted = jfield "extracted" js |> jbool in
          { name = pkg ; path ; depends ; drivers ; extracted }
        else
          { name = pkg ; path ; depends = [] ; drivers = [] ;
            extracted = false }
  in lookup pkg Global.Sites.packages

let find_all pkgs =
  let m = Hashtbl.create 32 in
  let pool = ref [] in
  let rec walk pkg =
    if not (Hashtbl.mem m pkg) then
      begin
        Hashtbl.add m pkg () ;
        let m = find pkg in
        List.iter walk m.depends ;
        pool := m :: !pool ;
      end
  in List.iter walk pkgs ; List.rev !pool

let install pkg =
  let meta = Filename.concat pkg.path "META.json" in
  let list xs = `List (List.map (fun s -> `String s) xs) in
  let nonempty (_,js) =
    match js with
    | `Bool b -> b
    | `Null -> false
    | `List [] -> false
    | _  -> true
  in
  Json.to_file meta @@ `Assoc (
    List.filter nonempty [
      "depends", list pkg.depends ;
      "drivers", list pkg.drivers ;
      "extracted", `Bool pkg.extracted ;
    ])

(* -------------------------------------------------------------------------- *)
(* ---                                                                    --- *)
(* -------------------------------------------------------------------------- *)

let shared file =
  let rec lookup = function
    | [] -> Utils.failwith "Resource '%s' not found" file
    | d::ds ->
      let path = Filename.concat d file in
      if Sys.file_exists path then path else
        lookup ds
  in lookup Global.Sites.resources

(* -------------------------------------------------------------------------- *)