From 52efb4dfb9810bbb749185f24916a43331abc817 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 27 Jun 2017 18:20:51 +0200 Subject: Avoid using unsupported signals under Windows in fake_ide. --- tools/fake_ide.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index c0d2e4d6b5..2718461243 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -293,7 +293,7 @@ let usage () = module Coqide = Spawn.Sync(struct end) let main = - Sys.set_signal Sys.sigpipe + if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in -- cgit v1.2.3 From da2d3108f126b3ff7bface118319bfa43829a895 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 13 Jul 2017 16:50:10 +0200 Subject: In fake_ide, call coqtop.exe instead of coqtop on Win32. --- tools/fake_ide.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 2718461243..258633d29b 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -298,7 +298,8 @@ let main = (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in let coqtop_name, coqtop_args, input_file = match Sys.argv with - | [| _; f |] -> "coqtop", Array.of_list def_args, f + | [| _; f |] -> (if Sys.os_type = "Unix" then "coqtop" else "coqtop.exe"), + Array.of_list def_args, f | [| _; f; ct |] -> let ct = Str.split (Str.regexp " ") ct in List.hd ct, Array.of_list (def_args @ List.tl ct), f -- cgit v1.2.3 From 2065b2abcc4fd42345ab9bfdafd75cf2a5a0889d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Jul 2017 10:51:45 +0200 Subject: coq-makefile: quote using ' to preserve \ (windows paths) --- tools/coq_makefile.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools') diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index c3aedf538e..c76b68dab3 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -118,7 +118,7 @@ let makefile_template = let template = "/tools/CoqMakefile.in" in Coq_config.coqlib ^ template -let quote s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s +let quote s = if String.contains s ' ' then "'" ^ s ^ "'" else s let generate_makefile oc conf_file local_file args project = let s = read_whole_file makefile_template in -- cgit v1.2.3 From 1fd1ca0703811392c890c41a796ed7efdaacca28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Jul 2017 15:02:47 +0200 Subject: coq-makefile: treat coq_makefile as any other coq binary In particular, find it under $(COQBIN) --- tools/CoqMakefile.in | 29 ++++++++++++++++------------- tools/coq_makefile.ml | 1 - 2 files changed, 16 insertions(+), 14 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7d281977af..841ee45711 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -87,6 +87,9 @@ COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" COQMKTOP ?= "$(COQBIN)coqmktop" +COQMKFILE ?= "$(COQBIN)coq_makefile" + +# Timing scripts COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" @@ -437,12 +440,12 @@ beautify: $(BEAUTYFILES) install: install-extra $(HIDE)for f in $(FILESTOINSTALL); do\ - df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ -z "$$df" ]; then\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ echo SKIP "$$f" since it has no logical path;\ else\ - install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ - install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ + install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\ fi;\ done @@ -452,12 +455,12 @@ install-extra:: install-byte: $(HIDE)for f in $(BYTEFILESTOINSTALL); do\ - df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ -z "$$df" ]; then\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ echo SKIP "$$f" since it has no logical path;\ else\ - install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ - install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ + install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\ fi;\ done @@ -482,11 +485,11 @@ install-doc:: html mlihtml uninstall:: @# Extension point $(HIDE)for f in $(FILESTOINSTALL); do \ - df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ - instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`"; \ - rm -f "$$instf";\ - echo RM "$$instf"; \ - rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true; \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" &&\ + (rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true); \ done .PHONY: uninstall diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index c76b68dab3..0e0375c008 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -199,7 +199,6 @@ let generate_conf_coq_config oc args bypass_API = then Coq_config.all_src_dirs else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; - fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); ;; let generate_conf_files oc -- cgit v1.2.3 From ad8bf70ccc61849cfb1ade20ce426ea2ec74aa0e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Jul 2017 18:05:34 +0200 Subject: coq-makefile: strip windows drive letter when DESTDIR is not empty In unix one can concatenate a prefix with an absolute path in order to obtain a valid path. This is not the case on Windows. --- tools/CoqMakefile.in | 44 +++++++++++++++++++++++--------------------- tools/coq_makefile.ml | 7 +++++++ 2 files changed, 30 insertions(+), 21 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 841ee45711..f1e519d038 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -184,10 +184,6 @@ endif PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' -COQLIBINSTALL = $(COQLIB)user-contrib -COQDOCINSTALL = $(DOCDIR)user-contrib -COQTOPINSTALL = $(COQLIB)toploop - ifneq (,$(TIMING)) TIMING_ARG=-time ifeq (after,$(TIMING)) @@ -208,6 +204,12 @@ ifneq "$(DSTROOT)" "" DESTDIR := $(DSTROOT) endif +concat_path = $(if $(1),$(1)/$(subst $(COQMF_WINDRIVE),/,$(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) + # Files ####################################################################### # # We here define a bunch of variables about the files being part of the @@ -444,9 +446,9 @@ install: install-extra if [ "$$?" != "0" -o -z "$$df" ]; then\ echo SKIP "$$f" since it has no logical path;\ else\ - install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ - install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ - echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ fi;\ done install-extra:: @@ -459,24 +461,24 @@ install-byte: if [ "$$?" != "0" -o -z "$$df" ]; then\ echo SKIP "$$f" since it has no logical path;\ else\ - install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ - install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df" &&\ - echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ fi;\ done install-doc:: html mlihtml @# Extension point - $(HIDE)install -d "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" $(HIDE)for i in html/*; do \ - dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ install -m 0644 "$$i" "$$dest";\ echo INSTALL "$$i" "$$dest";\ done $(HIDE)install -d \ - "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" $(HIDE)for i in mlihtml/*; do \ - dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ install -m 0644 "$$i" "$$dest";\ echo INSTALL "$$i" "$$dest";\ done @@ -486,20 +488,20 @@ uninstall:: @# Extension point $(HIDE)for f in $(FILESTOINSTALL); do \ df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ rm -f "$$instf" &&\ echo RM "$$instf" &&\ - (rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true); \ + (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" || true); \ done .PHONY: uninstall uninstall-doc:: @# Extension point - $(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' - $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' - $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE) rmdir "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true .PHONY: uninstall-doc # Cleaning #################################################################### diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 0e0375c008..327f53520c 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -193,12 +193,19 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } = (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)) ;; +let windrive s = + if Coq_config.arch_is_win32 && Str.(string_match (regexp "^[a-zA-Z]:") s 0) + then Str.matched_string s + else s +;; + let generate_conf_coq_config oc args bypass_API = section oc "Coq configuration."; let src_dirs = if bypass_API then Coq_config.all_src_dirs else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; + fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib) ;; let generate_conf_files oc -- cgit v1.2.3 From ecf880d0c50f7be9ab80893ae1fcc6714b3a2309 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 19 Jul 2017 12:55:39 +0200 Subject: fake_ide: do as coqide to find out coqtop path --- tools/fake_ide.ml | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) (limited to 'tools') diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 258633d29b..a9da27ba23 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -297,12 +297,24 @@ let main = (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in - let coqtop_name, coqtop_args, input_file = match Sys.argv with - | [| _; f |] -> (if Sys.os_type = "Unix" then "coqtop" else "coqtop.exe"), - Array.of_list def_args, f + let coqtop_name = (* from ide/ideutils.ml *) + let prog_name = "fake_ide" in + let len_prog_name = String.length prog_name in + let fake_ide_path = Sys.executable_name in + let fake_ide_path_len = String.length fake_ide_path in + let pos = fake_ide_path_len - len_prog_name in + let rex = Str.regexp_string prog_name in + try + let i = Str.search_backward rex fake_ide_path pos in + String.sub fake_ide_path 0 i ^ "coqtop" ^ + String.sub fake_ide_path (i + len_prog_name) + (fake_ide_path_len - i - len_prog_name) + with Not_found -> assert false in + let coqtop_args, input_file = match Sys.argv with + | [| _; f |] -> Array.of_list def_args, f | [| _; f; ct |] -> let ct = Str.split (Str.regexp " ") ct in - List.hd ct, Array.of_list (def_args @ List.tl ct), f + Array.of_list (def_args @ ct), f | _ -> usage () in let inc = if input_file = "-" then stdin else open_in input_file in let coq = -- cgit v1.2.3