diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_dune.ml | 15 | ||||
| -rw-r--r-- | tools/coqdep.ml | 4 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 2 |
3 files changed, 15 insertions, 6 deletions
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 06ad9e4792..9ecd8f19ce 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -109,6 +109,9 @@ module Aux = struct (* Move to Dirmap.update once we require OCaml >= 4.06.0 *) Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map + let replace_ext ~file ~newext = + Filename.(remove_extension file) ^ newext + end open Aux @@ -163,6 +166,11 @@ let pp_rule fmt targets deps action = "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n" ppl targets pp_deps deps pp_print_string action +let gen_coqc_targets vo = + [ vo.target + ; replace_ext ~file:vo.target ~newext:".glob" + ; "." ^ replace_ext ~file:vo.target ~newext:".aux"] + (* Generate the dune rule: *) let pp_vo_dep dir fmt vo = let depth = List.length dir in @@ -174,12 +182,13 @@ let pp_vo_dep dir fmt vo = (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in (* The source file is also corrected as we will call coqtop from the top dir *) - let source = bpath (dir @ [Filename.(remove_extension vo.target) ^ ".v"]) in + let source = bpath (dir @ [replace_ext ~file:vo.target ~newext:".v"]) in (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) let libflag = "-coqlib %{project_root}" in (* The final build rule *) let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -compile %s))" libflag eflag cflag source in - pp_rule fmt [vo.target] deps action + let all_targets = gen_coqc_targets vo in + pp_rule fmt all_targets deps action let pp_mlg_dep _dir fmt ml = let target = Filename.(remove_extension ml) ^ ".ml" in @@ -192,7 +201,7 @@ let pp_dep dir fmt oo = match oo with let out_install fmt dir ff = let itarget = String.concat "/" dir in - let ff = pmap (function | VO vo -> Some vo.target | _ -> None) ff in + let ff = List.concat @@ pmap (function | VO vo -> Some (gen_coqc_targets vo) | _ -> None) ff in let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n" (pp_list pp_ispec sep) ff diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 226a19678f..4e80caa4cc 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -233,7 +233,7 @@ struct let rem = NSet.fold push next rem in aux rem seen | Some false -> - (** The path we took encountered x -> y but not the one in seen *) + (* The path we took encountered x -> y but not the one in seen *) if through then aux (NMap.add n true rem) (NMap.add n true seen) else aux rem seen | Some true -> aux rem seen @@ -357,7 +357,7 @@ let treat_coq_file chan = | None -> acc | Some file_str -> (canonize file_str, ".v") :: acc else acc - | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *) + | AddLoadPath _ | AddRecLoadPath _ -> acc (* TODO *) in loop acc in diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index db2031c64b..e3dd32fb63 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -132,7 +132,7 @@ let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t) -(** The associated boolean is true if this is a root path. *) +(* The associated boolean is true if this is a root path. *) let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t) let get_prefix p l = |