From 565a30614c6df16466f66cac1e517f9202612709 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 17 Feb 2019 01:03:12 +0100 Subject: [azure] [ci] Build on Windows using Dune. We may want to keep the make-based and Dune job, however the make-based setup is tested by the INRIA workers so it may not be needed. In order for some test to run well, we always run in Dune with an absolute path. The easiest way to get a portable absolute path is to use OCaml itself so we introduce a small executable to do that. While we are at it, we do some cleanup of the test-suite `dune` file, in particular we remove useless comments, set `--no-buffer` so results can be seen in real time, and recognize the `NJOBS` variable as we have moved to a Dune version that supports env vars. --- tools/coqdoc/cdglobals.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 0d3fb77551..5dd6cc6c83 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -79,14 +79,17 @@ let use_suffix prefix suffix = (** A weaker analog of the function in Envars *) +let getenv_else s dft = try Sys.getenv s with Not_found -> dft () + let guess_coqlib () = + getenv_else "COQLIB" (fun () -> let file = "theories/Init/Prelude.vo" in let coqbin = normalize_path (Filename.dirname Sys.executable_name) in let prefix = Filename.dirname coqbin in let coqlib = use_suffix prefix Coq_config.coqlibsuffix in if Sys.file_exists (coqlib / file) then coqlib else if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file) - then Coq_config.coqlib else prefix + then Coq_config.coqlib else prefix) let header_trailer = ref true let header_file = ref "" -- cgit v1.2.3 From d6f88819f5279e94d33e0e15f6be1e368210af08 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 17 Feb 2019 17:51:05 +0100 Subject: [paths] Try to be more portable on Win32 Absolute paths follow different separator rules so "c:\foo/bar" may not work on `mingw`. We try to improve this situation using OCaml's `Filename.dir_sep/concat` --- tools/CoqMakefile.in | 8 ++++---- tools/coq_makefile.ml | 20 ++++++++++---------- 2 files changed, 14 insertions(+), 14 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f8f10b34ae..bd9d8c9221 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -187,7 +187,7 @@ COQDOCLIBS?=$(COQLIBS_NOML) COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) COQMAKEFILE_VERSION:=@COQ_VERSION@ -COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) @@ -216,9 +216,9 @@ endif concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2)) -COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib) -COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib) -COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) +COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib) +COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib) +COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop) # Files ####################################################################### # diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4f01a6bd87..68281d6481 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -123,9 +123,10 @@ let read_whole_file s = let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s let generate_makefile oc conf_file local_file args project = + let coqlib = Envars.coqlib () in let makefile_template = - let template = "/tools/CoqMakefile.in" in - Envars.coqlib () ^ template in + let template = Filename.concat "tools" "CoqMakefile.in" in + Filename.concat coqlib template in let s = read_whole_file makefile_template in let s = List.fold_left (* We use global_substitute to avoid running into backslash issues due to \1 etc. *) @@ -260,7 +261,7 @@ let generate_conf_doc oc { defs; q_includes; r_includes } = eprintf "Warning: in %s\n" destination; destination end else "$(INSTALLDEFAULTROOT)" - else String.concat "/" gcd in + else String.concat Filename.dir_sep gcd in Printf.fprintf oc "COQMF_INSTALLCOQDOCROOT = %s\n" (quote root) let generate_conf_defs oc { defs; extra_args } = @@ -343,15 +344,13 @@ let chop_prefix p f = let len_f = String.length f in String.sub f len_p (len_f - len_p) -let clean_path p = - Str.global_replace (Str.regexp_string "//") "/" p - let destination_of { ml_includes; q_includes; r_includes; } file = let file_dir = CUnix.canonical_path_name (Filename.dirname file) in let includes = q_includes @ r_includes in let mk_destination logic canonical_path = - clean_path (physical_dir_of_logical_dir logic ^ "/" ^ - chop_prefix canonical_path file_dir ^ "/") in + Filename.concat + (physical_dir_of_logical_dir logic) + (chop_prefix canonical_path file_dir) in let candidates = CList.map_filter (fun {thing={ canonical_path }, logic} -> if is_prefix canonical_path file_dir then @@ -368,8 +367,9 @@ let destination_of { ml_includes; q_includes; r_includes; } file = with | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} -> let destination = - clean_path (physical_dir_of_logical_dir logic ^ "/" ^ - chop_prefix p file_dir ^ "/") in + Filename.concat + (physical_dir_of_logical_dir logic) + (chop_prefix p file_dir) in Printf.printf "%s" (quote destination) | _ -> () (* skip *) | exception Not_found -> () (* skip *) -- cgit v1.2.3