Use dune-site to find resources (when installed)

easycrypt.opam

@@ -14,6 +14,22 @@ depends: [
   "zarith" {>= "1.10"}
   "odoc" {with-doc}
 ]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
 opam-version: "2.0"
 
 homepage: "https://www.easycrypt.info/"
@@ -36,8 +52,3 @@ can install AltErgo (package: alt-ergo).
 
 The required steps for configuring the provers are listed on:
   https://github.com/EasyCrypt/easycrypt#configuring-why3"""
-
-build: [
-  ["dune" "subst"]
-  ["dune" "build" "-p" name "-j" jobs "@install"]
-]

easycrypt.opam.template

@@ -20,8 +20,3 @@ can install AltErgo (package: alt-ergo).
 
 The required steps for configuring the provers are listed on:
   https://github.com/EasyCrypt/easycrypt#configuring-why3"""
-
-build: [
-  ["dune" "subst"]
-  ["dune" "build" "-p" name "-j" jobs "@install"]
-]

src/dune

@@ -5,19 +5,23 @@
 
 (include_subdirs unqualified)
 
+(generate_sites_module
+ (module ecDuneSites)
+ (sites easycrypt))
+
 (library 
  (name ecLib)
  (public_name easycrypt.ecLib)
  (modules :standard \ ec)
- (libraries batteries camlp-streams dune-build-info inifiles why3 yojson zarith)
+ (libraries batteries camlp-streams dune-build-info dune-site inifiles why3 yojson zarith)
 )
 
 (executable
  (public_name easycrypt)
  (name ec)
  (modules ec)
  (promote (until-clean))
- (libraries batteries camlp-streams dune-build-info inifiles why3 yojson zarith ecLib))
+ (libraries batteries camlp-streams dune-build-info dune-site inifiles why3 yojson zarith ecLib))
 
 (ocamllex ecLexer)
 

src/ec.ml

@@ -38,6 +38,8 @@ type pconfig = {
 }
 
 let print_config config =
+  let (module Sites) = EcRelocate.sites in
+
   (* Print git-hash *)
   Format.eprintf "git-hash: %s@\n%!" EcVersion.hash;
 
@@ -92,6 +94,9 @@ let print_config config =
       (String.concat ", " (List.map string_of_prover provers))
   end;
 
+  (* Command path *)
+  Format.eprintf "Commands PATH: %s@\n%!" Sites.commands;
+
   (* Print system PATH *)
   Format.eprintf "System PATH:@\n%!";
   List.iter
@@ -105,7 +110,7 @@ let main () =
    * disallows Why3 server to detect external provers completion      *)
   let _ : int list = Unix.sigprocmask Unix.SIG_SETMASK [] in
 
-  let theories = EcRelocate.Sites.theories in
+  let (module Sites) = EcRelocate.sites in
 
   (* Parse command line arguments *)
   let conffile, options =
@@ -190,7 +195,7 @@ let main () =
           | Some root ->
               List.fold_left Filename.concat root ["scripts"; "testing"]
           | None ->
-              EcRelocate.resource ["commands"] in
+              Sites.commands in
         let cmd  = Filename.concat root "runtest" in
         let args =
             [
@@ -219,7 +224,7 @@ let main () =
         let pwd = Sys.getcwd () in
         Sys.chdir (
           List.fold_left Filename.concat
-            (List.hd EcRelocate.Sites.theories)
+            (List.hd Sites.theories)
             (List.init 3 (fun _ -> ".."))
         ); Some pwd
 
@@ -263,7 +268,7 @@ let main () =
       EcCommands.addidir ~namespace:`System (Filename.concat theory "prelude");
       if not ldropts.ldro_boot then
         EcCommands.addidir ~namespace:`System ~recursive:true theory
-    ) theories;
+    ) Sites.theories;
     List.iter (fun (onm, name, isrec) ->
         EcCommands.addidir
           ?namespace:(omap (fun nm -> `Named nm) onm)

src/ecLoader.ml

@@ -51,7 +51,7 @@ let rec addidir ?namespace ?(recursive = false) (idir : string) (ecl : ecloader)
       try Sys.is_directory filename with Sys_error _ -> false
     in
 
-    let dirs = (try EcUtils.Os.listdir idir with Unix.Unix_error _ -> []) in
+    let dirs = (try EcUtils.Os.listdir idir with Unix.Unix_error _ | Sys_error _ -> []) in
     let dirs = List.sort compare (List.filter isdir dirs) in
 
       List.iter (fun filename ->

src/ecRelocate.ml

@@ -1,30 +1,48 @@
+(* -------------------------------------------------------------------- *)
 let myname = Filename.basename Sys.executable_name
 let mydir  = Filename.dirname  Sys.executable_name
 
-let eclocal =
+(* -------------------------------------------------------------------- *)
+let eclocal : bool =
   let rex = EcRegexp.regexp "^ec\\.(?:native|byte|exe)$" in
   EcRegexp.match_ (`C rex) myname
 
-let sourceroot =
+(* -------------------------------------------------------------------- *)
+let sourceroot : string option =
   if eclocal then
     if   Filename.basename mydir = "src"
     then Some (Filename.dirname mydir)
     else Some mydir
   else None
 
-let resource name =
-  match eclocal with
-  | true ->
-      if Filename.basename mydir = "src" then
-        List.fold_left Filename.concat mydir
-          ([Filename.parent_dir_name] @ name)
-      else
-        List.fold_left Filename.concat mydir name
-
-  | false ->
-      List.fold_left Filename.concat mydir
-        ([Filename.parent_dir_name; "lib"; "easycrypt"] @ name)
-
-module Sites = struct
-  let theories = [resource ["theories"]]
+(* -------------------------------------------------------------------- *)
+let local (name : string list) : string =
+  List.fold_left Filename.concat (Option.value ~default:"." sourceroot) name
+
+(* -------------------------------------------------------------------- *)
+module type Sites = sig
+  val commands : string
+  val theories : string list
+end
+
+(* -------------------------------------------------------------------- *)
+module LocalSites() : Sites = struct
+  let commands = local ["scripts"; "testing"]
+  let theories = [local ["theories"]]
 end
+
+(* -------------------------------------------------------------------- *)
+module DuneSites() : Sites = struct
+  let commands =
+    Option.value ~default:"."
+      (EcUtils.List.Exceptionless.hd EcDuneSites.Sites.commands)
+
+  let theories =
+    EcDuneSites.Sites.theories
+end
+
+(* -------------------------------------------------------------------- *)
+let sites : (module Sites) =
+  if   eclocal
+  then (module LocalSites ())
+  else (module DuneSites ())

src/ecRelocate.mli

@@ -1,6 +1,11 @@
+(* -------------------------------------------------------------------- *)
 val sourceroot : string option
-val resource : string list -> string
 
-module Sites : sig
+(* -------------------------------------------------------------------- *)
+module type Sites = sig
+  val commands : string
   val theories : string list
 end
+
+(* -------------------------------------------------------------------- *)
+val sites : (module Sites)