From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 10 Jan 2023 16:59:08 +0000 (+0100)
Subject: auxiliary executables (xoa, matitadep, probe, matex) ported to dune
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef225b816c82d4fad37993f963804e51152f4dac;p=helm.git

auxiliary executables (xoa, matitadep, probe, matex) ported to dune
---

diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile
index b437afb5b..7783a0570 100644
--- a/matita/components/binaries/matex/Makefile
+++ b/matita/components/binaries/matex/Makefile
@@ -1,9 +1,4 @@
 EXEC = matex
-VERSION=0.1.0
-
-REQUIRES = helm-ng_library
-
-include ../Makefile.common
 
 MATEX    = ./$(EXEC).native
 PROBE    = ../probe/probe.native
diff --git a/matita/components/binaries/matex/dune b/matita/components/binaries/matex/dune
new file mode 100644
index 000000000..e49bde67a
--- /dev/null
+++ b/matita/components/binaries/matex/dune
@@ -0,0 +1,12 @@
+(executable
+  (name matex)
+  (public_name matex)
+  (promote (until-clean))
+  (libraries helm_ng_library)
+  (modules_without_implementation)
+  (modules alpha anticipate engine ground options TeXOutput kernel meta TeX matex)
+)
+
+(env
+  (_
+    (flags (:standard -thread -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-29)))) ; -29 for non portable strings
diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 324d114a9..aef518025 100644
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -12,7 +12,7 @@
 module F = Filename
 module L = List
 module P = Printf
-module S = String
+(* module S = String *)
 
 module U = NUri
 module R = NReference
@@ -26,7 +26,7 @@ module K = Kernel
 module T = TeX
 module O = TeXOutput
 module A = Anticipate
-module M = Meta
+(* module M = Meta *)
 module N = Alpha
 
 type status = {
@@ -86,7 +86,7 @@ let get_head = function
       end 
    | _               -> None
 
-let proc_sort st is = function
+let proc_sort _st is = function
    | C.Prop             -> T.Macro "PROP" :: is
    | C.Type [`Type, u]  -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
    | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is
@@ -214,7 +214,7 @@ let rec proc_proof st ris t = match t with
       let ris = T.Macro "STEP" :: mk_inferred st t ris in
       let tts = L.rev_map (proc_term st []) rts in
       mk_exit st (T.rev_mk_args tts ris)
-   | C.Match (w, u, v, ts) ->
+   | C.Match (_w, _u, v, ts) ->
       let rts = X.rev_neg_filter (K.not_prop2 st.c) [v] ts in
       let ris = T.Macro "DEST" :: mk_inferred st t ris in
       let tts = L.rev_map (proc_term st []) rts in
@@ -290,13 +290,13 @@ let proc_pair s ss u = function
          O.out_text och (text_t s name t);
       close_out och
 
-let proc_fun ss (r, s, i, u, t) =
+let proc_fun ss (_r, s, _i, u, t) =
    proc_pair s (s :: ss) u (Some t)
 
-let proc_constructor ss (r, s, u) =
+let proc_constructor ss (_r, s, u) =
    proc_pair s (s :: ss) u None
 
-let proc_type ss (r, s, u, cs) =
+let proc_type ss (_r, s, u, cs) =
    proc_pair s (s :: ss) u None;
    L.iter (proc_constructor ss) cs
 
diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml
index 7eebedb7d..3c75b4032 100644
--- a/matita/components/binaries/matex/ground.ml
+++ b/matita/components/binaries/matex/ground.ml
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-module L = List
+(* module L = List *)
 module P = Printf
 module S = String
 
@@ -48,7 +48,7 @@ let rec foldi_left mapi i a = function
    | []       -> a
    | hd :: tl -> foldi_left mapi (succ i) (mapi i a hd) tl
 
-let rec rev_mapi mapi i l =
+let rev_mapi mapi i l =
    let map i a hd = mapi i hd :: a in
    foldi_left map i [] l
 
diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml
index ddd413049..66faa9859 100644
--- a/matita/components/binaries/matex/matex.ml
+++ b/matita/components/binaries/matex/matex.ml
@@ -19,7 +19,7 @@ module L = Librarian
 module X = Ground
 module G = Options
 module E = Engine
-module O = TeXOutput
+(* module O = TeXOutput *)
 module K = Kernel
 
 let help_O = "<dir> Set this output directory"
diff --git a/matita/components/binaries/matitadep/Makefile b/matita/components/binaries/matitadep/Makefile
deleted file mode 100644
index 2fe33e60b..000000000
--- a/matita/components/binaries/matitadep/Makefile
+++ /dev/null
@@ -1,6 +0,0 @@
-EXEC = matitadep
-VERSION=0.1.0
-
-REQUIRES = helm-ng_library
-
-include ../Makefile.common
diff --git a/matita/components/binaries/matitadep/dune b/matita/components/binaries/matitadep/dune
new file mode 100644
index 000000000..8988331ee
--- /dev/null
+++ b/matita/components/binaries/matitadep/dune
@@ -0,0 +1,12 @@
+(executable
+  (name matitadep)
+  (public_name matitadep)
+  (promote (until-clean))
+  (libraries helm_ng_library)
+  (modules_without_implementation)
+  (modules matitadep)
+)
+
+(env
+  (_
+    (flags (:standard -thread -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-29)))) ; -29 for non portable strings
diff --git a/matita/components/binaries/probe/Makefile b/matita/components/binaries/probe/Makefile
deleted file mode 100644
index 24daac41d..000000000
--- a/matita/components/binaries/probe/Makefile
+++ /dev/null
@@ -1,6 +0,0 @@
-EXEC = probe
-VERSION=0.1.0
-
-REQUIRES = helm-ng_library
-
-include ../Makefile.common
diff --git a/matita/components/binaries/probe/dune b/matita/components/binaries/probe/dune
new file mode 100644
index 000000000..19e20a3a5
--- /dev/null
+++ b/matita/components/binaries/probe/dune
@@ -0,0 +1,15 @@
+(ocamllex macLexer)
+
+(executable
+  (name probe)
+  (public_name probe)
+  (promote (until-clean))
+  (libraries helm_ng_library)
+  (modules_without_implementation)
+  (modules macLexer engine error matitaRemove nCicScan matitaList options probe)
+)
+
+(env
+  (_
+    (flags (:standard -thread -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-29)))) ; -29 for non portable strings
+          
diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml
index 95250b26c..e00f0c76c 100644
--- a/matita/components/binaries/probe/matitaList.ml
+++ b/matita/components/binaries/probe/matitaList.ml
@@ -11,7 +11,6 @@
 
 module A = Array
 module F = Filename
-module P = Printf
 module S = String
 module Y = Sys
 
diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml
index 736baafbc..3accc4e71 100644
--- a/matita/components/binaries/probe/nCicScan.ml
+++ b/matita/components/binaries/probe/nCicScan.ml
@@ -39,7 +39,7 @@ let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour)
 
 let add_ind n = O.add_xflavour n `Inductive
 
-let rec set_list c ts cts =
+let set_list c ts cts =
   let map cts t = (c, t) :: cts in
   L.fold_left map cts ts
 
@@ -84,7 +84,7 @@ let rec scan_term st = function
   | (_, C.Sort _)                :: tl -> scan_term (inc st) tl
   | (c, C.Rel i)                 :: tl -> scan_term (scan_lref st c i) tl
   | (_, C.Const p)               :: tl -> scan_term (scan_gref st p) tl
-  | (_, C.Appl [])               :: tl -> X.malformed ()
+  | (_, C.Appl [])               :: _  -> X.malformed ()
   | (c, C.Appl ts)               :: tl ->
     scan_term (add st (pred (L.length ts))) (set_list c ts tl)
   | (c, C.Match (_, t0, t1, ts)) :: tl ->
diff --git a/matita/components/binaries/xoa/Makefile b/matita/components/binaries/xoa/Makefile
deleted file mode 100644
index 1933a2003..000000000
--- a/matita/components/binaries/xoa/Makefile
+++ /dev/null
@@ -1,6 +0,0 @@
-EXEC = xoa
-VERSION=0.2.0
-
-REQUIRES = helm-registry
-
-include ../Makefile.common
diff --git a/matita/components/binaries/xoa/dune b/matita/components/binaries/xoa/dune
new file mode 100644
index 000000000..631bbcb99
--- /dev/null
+++ b/matita/components/binaries/xoa/dune
@@ -0,0 +1,12 @@
+(executable
+  (name xoa)
+  (public_name xoa)
+  (promote (until-clean))
+  (libraries helm_registry)
+  (modules_without_implementation)
+  (modules ast lib ast engine xoa)
+)
+
+(env
+  (_
+    (flags (:standard -thread -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-29)))) ; -29 for non portable strings
diff --git a/matita/components/binaries/xoa/engine.ml b/matita/components/binaries/xoa/engine.ml
index 47770e710..1c5ae3318 100644
--- a/matita/components/binaries/xoa/engine.ml
+++ b/matita/components/binaries/xoa/engine.ml
@@ -52,7 +52,7 @@ let mk_exists ooch noch c v =
    let pre_appl n = P.sprintf "%s %s" (pre n) ele_seq in
    let pre_type   = string_iter " → " pre_appl c in
 
-   let qm n       = "?" in
+   let qm _n      = "?" in
    let qm_set     = string_iter " " qm v in
    let qm_pre     = string_iter " " qm c in
 
@@ -99,7 +99,7 @@ let mk_or ooch noch c =
    let pre_list   = string_iter "," pre c in
    let pre_seq    = string_iter " " pre c in
 
-   let qm n       = "?" in
+   let qm _n      = "?" in
    let qm_pre     = string_iter " " qm c in
 
    let term n     = P.sprintf "term 29 P%u" (c - n) in
@@ -139,7 +139,7 @@ let mk_and ooch noch c =
    let pre_type   = string_iter " → " pre c in
    let pre_seq    = string_iter " " pre c in
 
-   let qm n       = "?" in
+   let qm _n      = "?" in
    let qm_pre     = string_iter " " qm c in
 
    let term n     = P.sprintf "term 34 P%u" (c - n) in
diff --git a/matita/components/binaries/xoa/lib.ml b/matita/components/binaries/xoa/lib.ml
index f2bf31757..9684dc558 100644
--- a/matita/components/binaries/xoa/lib.ml
+++ b/matita/components/binaries/xoa/lib.ml
@@ -14,51 +14,51 @@ module K = Sys
 
 module R = Helm_registry
 
-let template = "matita.ma.templ"
+let template = "../../../matita/matita.ma.templ"
 
 let myself = F.basename Sys.argv.(0)
 
-let get_preamble conf =
-   R.load_from conf;
-   let rt_base_dir = R.get_string "matita.rt_base_dir" in
-   F.concat rt_base_dir template
+let rt_base_dir = F.dirname Sys.argv.(0)
+
+let get_preamble () =
+  F.concat rt_base_dir template
 
 let copy_preamble preamble och =
-   let ich = open_in preamble in
-   let rec read () =
-      Printf.fprintf och "%s\n" (input_line ich); read ()
-   in
-   try read () with End_of_file -> close_in ich
+  let ich = open_in preamble in
+  let rec read () =
+    Printf.fprintf och "%s\n" (input_line ich); read ()
+  in
+  try read () with End_of_file -> close_in ich
 
 let print_header def och =
   let msg = if def then "LOGIC" else "GROUND NOTATION" in
-   let stars = String.make (72 - String.length msg) '*' in
-   Printf.fprintf och "(* %s %s*)\n\n" msg stars
+  let stars = String.make (72 - String.length msg) '*' in
+  Printf.fprintf och "(* %s %s*)\n\n" msg stars
 
 let print_comment och =
-   let msg = Printf.sprintf "NOTE: This file was generated by %s, do not edit" myself in
-   let stars = String.make (72 - String.length msg) '*' in
-   Printf.fprintf och "(* %s %s*)\n\n" msg stars
+  let msg = Printf.sprintf "NOTE: This file was generated by %s, do not edit" myself in
+  let stars = String.make (72 - String.length msg) '*' in
+  Printf.fprintf och "(* %s %s*)\n\n" msg stars
 
 let exists_out name =
-   let path = [
-      R.get_string "xoa.output_dir";
-      name
-   ] in
-   let name = List.fold_left F.concat "" path in
-   K.file_exists (name ^ ".ma")
+  let path = [
+    R.get_string "xoa.output_dir";
+    name
+  ] in
+  let name = List.fold_left F.concat "" path in
+  K.file_exists (name ^ ".ma")
 
 let open_out def preamble name =
-   let path = [
-      R.get_string "xoa.output_dir";
-      name
-   ] in
-   let name = List.fold_left F.concat "" path in
-   let och = open_out (name ^ ".ma") in
-   copy_preamble preamble och;
-   print_header def och;
-   print_comment och;
-   och
+  let path = [
+    R.get_string "xoa.output_dir";
+    name
+  ] in
+  let name = List.fold_left F.concat "" path in
+  let och = open_out (name ^ ".ma") in
+  copy_preamble preamble och;
+  print_header def och;
+  print_comment och;
+  och
 
 let out_include och s =
-   Printf.fprintf och "include \"%s\".\n\n" s
+  Printf.fprintf och "include \"%s\".\n\n" s
diff --git a/matita/components/binaries/xoa/lib.mli b/matita/components/binaries/xoa/lib.mli
index cc66968d3..2cd5fb53f 100644
--- a/matita/components/binaries/xoa/lib.mli
+++ b/matita/components/binaries/xoa/lib.mli
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-val get_preamble: string -> string
+val get_preamble: unit -> string
 
 val exists_out: string -> bool
 
diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml
index 64ce87b17..3d35f1932 100644
--- a/matita/components/binaries/xoa/xoa.ml
+++ b/matita/components/binaries/xoa/xoa.ml
@@ -18,6 +18,9 @@ module E = Engine
 let incremental = ref true
 let separate = ref false
 
+let preamble =
+  L.get_preamble ()
+
 let clear () =
   incremental := true;
   separate := false;
@@ -33,7 +36,7 @@ let unm_and s =
   Scanf.sscanf s "%u" A.mk_and
 
 let process_centralized conf =
-  let preamble = L.get_preamble conf in
+  R.load_from conf;
   if R.has "xoa.objects" && R.has "xoa.notations" then begin
     let ooch = L.open_out true preamble (R.get_string "xoa.objects") in
     let noch = L.open_out false preamble (R.get_string "xoa.notations") in
@@ -71,7 +74,7 @@ let generate (p, o, n) d =
   end
 
 let process_distributed conf =
-  let preamble = L.get_preamble conf in
+  R.load_from conf;
   if R.has "xoa.objects" && R.has "xoa.notations" then begin
     let st = preamble, R.get_string "xoa.objects", R.get_string "xoa.notations" in
     List.iter (generate st) (R.get_list unm_ex "xoa.ex");